Call the index set of X IX. Call the partition into empty parts indexed by S 0S. We have 0 ⊣ I ⊣ D ⊣ ⊔ ⊣ T.
None of the our three adjunction strings can be extended further. Let’s apply the construction that gave us histories at the other 5 ends. Niceness is implicit. - The right construction of TS->X is the terminal S->S’ with a TS’->X: The image of ⊔(TS->X). - The left construction of X->0S is the initial S’->S with a X->0S’: The image of I(X->0S). - The left construction of B->FX is the initial X’->X with a B->FX’: The image of ∨(B->FX). - The right construction of Δ1•->S is the terminal •->• with a Δ1•->S: The image of Δ•(Δ1•->S). - The left construction of S->Δ∅• is absurd, but can still be written as the image of Δ•(S->Δ∅•). - The history of ∨B->X is the terminal B->B’ with a ∨B’->X: Breaks the pattern! F(∨B->X) does not have the information to determine the history.
In fact, ⊔T, I0, ∨F, Δ•Δ1 and Δ•Δ∅ are all identity, only F∨ isn’t.
Call the index set of X IX. Call the partition into empty parts indexed by S 0S. We have 0 ⊣ I ⊣ D ⊣ ⊔ ⊣ T.
None of the our three adjunction strings can be extended further. Let’s apply the construction that gave us histories at the other 5 ends. Niceness is implicit.
- The right construction of TS->X is the terminal S->S’ with a TS’->X: The image of ⊔(TS->X).
- The left construction of X->0S is the initial S’->S with a X->0S’: The image of I(X->0S).
- The left construction of B->FX is the initial X’->X with a B->FX’: The image of ∨(B->FX).
- The right construction of Δ1•->S is the terminal •->• with a Δ1•->S: The image of Δ•(Δ1•->S).
- The left construction of S->Δ∅• is absurd, but can still be written as the image of Δ•(S->Δ∅•).
- The history of ∨B->X is the terminal B->B’ with a ∨B’->X: Breaks the pattern! F(∨B->X) does not have the information to determine the history.
In fact, ⊔T, I0, ∨F, Δ•Δ1 and Δ•Δ∅ are all identity, only F∨ isn’t.