Index of the slides:

DTT: the exchange rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 DTT: the “unpack” rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 DTT: structural rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 DTT: type rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 DTT: alternate rules for strong sum . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6 DTT: Alternate rules for strong equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Adjunction diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Conversions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Comprehension categories with unit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 Comprehension categories with unit: a bijection . . . . . . . . . . . . . . . . . . . . . . . .11 Comprehension categories with unit: big bijection . . . . . . . . . . . . . . . . . . . . . . 12 Comprehension categories with unit: three rules . . . . . . . . . . . . . . . . . . . . . . . .13 Interpreting ΠI and ΠE in a CCompC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Interpreting ΣI in a CCompC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Interpreting ΣE^{+} in a CCompC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .16 The “unpack” rule (2) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Rules for DTT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 DTT: the exchange rule In Jacobs (10.1) the exchange rule for DTT is stated like this:

{Γ, x : σ, y : τ, Δ ⊢ M : ρ \atop Γ, y : τ, x : σ, Δ ⊢ M : ρ}

with a side-condition: “x is not free in τ”.

Let’s translate this:

{a⃗:A⃗, b:Ba⃗, c:Ca⃗, d⃗:D⃗_{a⃗bc} ⊢ e_{a⃗bcd⃗}:E_{a⃗bcd⃗} \atop a⃗:A⃗, c:Ca⃗, b:Ba⃗, d⃗:D⃗_{a⃗bc} ⊢ e_{a⃗bcd⃗}:E_{a⃗bcd⃗}}

Note that if we had used c : C_{a⃗b} instead of c : Ca⃗ the bottom judgment would have made no sense.

Let’s make this shorter. We can hide the annotations that indicate dependencies, the types, and the “vector” marks:

{a⃗:A⃗, b:B, c:C, d⃗:D⃗ ⊢ e:E \atop a⃗:A⃗, c:C, b:B, d⃗:D⃗ ⊢ e:E} {a⃗, b, c, d⃗ ⊢ e \atop a⃗, c, b, d⃗ ⊢ e}  {a, b, c, d ⊢ e \atop a, c, b, d ⊢ e}

It is this last form that we will use.

Exercise: rewrite the first translation with

(a⃗:A⃗) := (a_{1}:A_{1}[ ], …, a_{n}:A_{n}[a_{1}, ..., a_{n−1}])
(d⃗:D⃗_{a⃗bc}) := (d_{1}:D_{1}[a_{1}, ..., a_{n}, b, c], …,

d_{m}:D_{m}[a_{1}, ..., a_{n}, b, c, d_{1}, ..., d_{m−1}])

and check that the rule becomes unbearably big.

DTT: the “unpack” rule In Jacobs (10.1, but after 10.1.2) the strong sum-elimination rule is stated as this:

Γ, z : Σx : σ.τ ⊢ ρ : Type Γ, x : σ, y : τ ⊢ Q : ρ[⟨x, y⟩/z]
Γ, z : Σx : σ.τ ⊢ (unpack z as ⟨x, y⟩ in Q) : ρ

(strong)

In an “unpack” term like

unpack P as ⟨x, y⟩ in Q

the “unpack” binds two variables in Q, x and y, at the same time, and sets their values to the components of the (dependent) pair P.

In the presence of π and π′ we can define:

(unpack P as ⟨x, y⟩ in Q) := Q[x := πP, y := π′P].

Let’s change the “unpack” notation one step at a time:

unpack P as ⟨x, y⟩ in Q
⇒ unpack P =: x, y in Q
⇒ Q[x, y := P]

Now let’s rewrite the rule:

Γ, z : Σx : σ.τ ⊢ ρ : Type Γ, x : σ, y : τ ⊢ Q : ρ[z := ⟨x, y⟩]
Γ, z : Σx : σ.τ ⊢ Q[x, y := z] : ρ

\begin{matrix}a⃗:A⃗, p:(Σb:B.C) ⊢ D:Type & a⃗:A⃗, b:B, c:C ⊢ d:D[p := ⟨b, c⟩] \\ a⃗:A⃗, p:(Σb:B.C) ⊢ d[b, c := p]:D \end{matrix}

\begin{matrix}a⃗:A⃗, (b, c):(Σb:B.C) ⊢ D:Type & a⃗:A⃗, b:B, c:C ⊢ d:D[(b, c) := ⟨b, c⟩] \\ a⃗:A⃗, (b, c):(Σb:B.C) ⊢ d[b, c := (b, c)]:D \end{matrix}

\begin{matrix}a⃗, (b, c) ⊢ D & a⃗, b, c ⊢ d \\ a⃗, (b, c) ⊢ d[b, c := (b, c)] \end{matrix}

\begin{matrix}a, (b, c) ⊢ D & a, b, c ⊢ d \\ a, (b, c) ⊢ d[b, c := (b, c)] \end{matrix} ΣE^{+}

\begin{matrix}a, (b, c) ⊢ D & a, b, c ⊢ d \\ a, (b, c) ⊢ d \end{matrix} ΣE^{+}

We will use the two last forms.

DTT: structural rules These ones are used very often:

Variable:  {a ⊢ B \atop a, b ⊢ b} v
Substitution: \begin{matrix}a ⊢ b & a, b, c ⊢ D \\ a, c ⊢ D \end{matrix} s \begin{matrix}a ⊢ b & a, b, c ⊢ d \\ a, c ⊢ d \end{matrix} s
Weakeking:  \begin{matrix}a ⊢ B & a ⊢ C \\ a, b ⊢ C \end{matrix} w  \begin{matrix}a ⊢ B & a ⊢ c \\ a, b ⊢ c \end{matrix} w

These ones not so much:

Conversion: \begin{aligned}a ⊢ b & a ⊢ B = B′ \\ & a ⊢ b′ \end{aligned} conv
Contraction:  {a, b, b′, c ⊢ D \atop a, b, c ⊢ D} contr  {a, b, b′, c ⊢ d \atop a, b, c ⊢ d} contr
Exchange:  {a, b, c, d ⊢ E \atop a, c, b, d ⊢ E} exch  {a, b, c, d ⊢ e \atop a, c, b, d ⊢ e} exch

Note: “Variable” is called “Projection” at [Jacobs].

DTT: type rules We have four different type-formers: singleton, (dependent) products, (dependent) sums, and equality. For each one of them we have a type-building rule, an introduction rule, and elimination rules.

There are several options for elimination rules for dependent sums and equality.

In a system with “weak sums” the rule is ΣE^{−}. In a system with “strong sums” the rule is ΣE^{+}, or, equivalently, π + π′.

In a system with “weak equality” the rule is EqE^{−}. In a system with “strong equality” the rule is EqE^{+}, or, equivalently, ee+ur (“externalization of equality” plus “uniqueness of reflexivity”).

Singleton:  ⊢ 1 1  ⊢ ∗ 1I  {a ⊢ ∗′ \atop a ⊢ ∗′ = ∗} 1E

Products:  {a, b ⊢ C \atop a ⊢ Πb : B.C} Π  {a, b ⊢ c \atop a ⊢ b↦c} ΠI  \begin{aligned}a ⊢ b & a ⊢ b↦c \\ & a ⊢ c \end{aligned} ΠE

Sums:  {a, b ⊢ C \atop a ⊢ Σb : B.C} Σ  \begin{matrix}a ⊢ B & a, b ⊢ C \\ a, b, c ⊢ (b, c) \end{matrix} ΣI  (See below)

Equality: {a ⊢ B \atop a, b, b′ ⊢ W[b = b′]} Eq {a ⊢ B \atop a, b ⊢ (b = b)} EqI  (See below)

\begin{matrix}a ⊢ D & a, b, c ⊢ d \\ a, (b, c) ⊢ d \end{matrix} ΣE^{−}  \begin{matrix}a, b, b′, c ⊢ D & a, b, c ⊢ d \\ a, b, b′, (b = b′), c ⊢ d \end{matrix} ^{EqE^{−}}

\begin{matrix}a, (b, c) ⊢ D & a, b, c ⊢ d \\ a, (b, c) ⊢ d \end{matrix} ΣE^{+}  \begin{matrix}a, b, b′, (b = b′) ⊢ C & a, b ⊢ c \\ a, b, b′, (b = b′) ⊢ c \end{matrix} ^{EqE^{+}}

{a ⊢ b, c \atop a ⊢ b} π  {a ⊢ b, c \atop a ⊢ c} π′  {a ⊢ (b = b′) \atop a ⊢ b = b′} ee {a ⊢ (b = b)′ \atop a ⊢ (b = b)′ = (b = b)} ur

DTT: alternate rules for strong sum Jacobs, 10.1.3 (i): The rules π and π′ can be defined from ΣE^{+}:

{a ⊢ (b, c) \atop a ⊢ b} π := \begin{aligned}a ⊢ (b, c) & \begin{matrix}\begin{matrix}{a, b ⊢ C \atop a ⊢ Σb.C} Σ & a ⊢ B \\ a, (b, c) ⊢ B \end{matrix} w & \begin{matrix}a, b ⊢ C & {a ⊢ B \atop a, b ⊢ b} v \\ a, b, c ⊢ b \end{matrix} ; w \\ a, (b, c) ⊢ b \end{matrix} ; ΣE^{+} \\ & a ⊢ b \end{aligned} ; s

{a ⊢ (b, c) \atop a ⊢ c} π′ := \begin{aligned}a ⊢ (b, c) & \begin{matrix}\begin{matrix}{a, b ⊢ C \atop a, (b, c) ⊢ b} & a, b ⊢ C \\ a, (b, c) ⊢ C \end{matrix} s & {a, b ⊢ C \atop a, b, c ⊢ c} v \\ a, (b, c) ⊢ c \end{matrix} ; ΣE^{+} \\ & a ⊢ c \end{aligned} ; s

The rule ΣE^{+} can be defined from π and π′:

\begin{matrix}\begin{matrix}a, (b, c) ⊢ D & a, b, c ⊢ d \\ a, (b, c) ⊢ d \end{matrix} & ΣE^{+} \\ := \begin{aligned}{a, b ⊢ C \atop a, (b, c) ⊢ c} π′ & \begin{matrix}{a, b ⊢ C \atop a, (b, c) ⊢ b} π & \begin{matrix}{a, b ⊢ C \atop a ⊢ Σb.C} Σ & a, b, c ⊢ d \\ a, (b, c), b, c ⊢ d \end{matrix} w \\ a, (b, c), c ⊢ d \end{matrix} ; s \\ & a, (b, c) ⊢ d \end{aligned} ; s \end{matrix}

DTT: Alternate rules for strong equality The ΣE^{+} rule is equivalent to the two rules ee and ur, that say that from “witnesses of equality” we can prove external equality - i.e., that some terms are equal. This equivalence ΣE^{+} ⟺ (ee, ur) is of a different nature from the ones that we have seen before - this one uses β/ϵ/:= and lives intrinsically in the (P+T) structure - it cannot be restricted to the T-part (i.e., to the syntactical world).

a, b, b′, e ⊢ b
=^{η} b[b′ := b, e := r] with b = b′ via e
= b′[b′ := b, e := r] with b = b′ via e
=^{η} b′
a, b, b′, e ⊢ e
=^{η} e[b′ := b, e := r] with b = b′ via e
= r[b′ := b, e := r] with b = b′ via e
=^{η} r

Adjunction diagrams

[figure: (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}(b=b′), c \\ a, b, b′ \end{matrix}); (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}(b=b′), c \\ a, b, b′ \end{matrix}); co□; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a, b, b′ \end{matrix})}; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a, b, b′ \end{matrix})}; □; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}d \\ a, b \end{matrix})}; a,b;c⊢d; (\begin{matrix}(b=b′), c \\ a, b, b′ \end{matrix}); _{(\begin{matrix}d \\ a, b, b′ \end{matrix})}; a,b,b′;e,c⊢d[b = b′ via e]; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}d \\ a, b \end{matrix})}; a,b;c⊢d[b′:=b,e:=r]; (\begin{matrix}(b=b′), c \\ a, b, b′ \end{matrix}); _{(\begin{matrix}d \\ a, b, b′ \end{matrix})}; a,b,b′;e,c⊢d; a, b; a, b, b′; (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}b, c \\ a \end{matrix}); (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}b, c \\ a \end{matrix}); co□; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; □; _{(\begin{matrix}e \\ a, b \end{matrix})}; _{(\begin{matrix}b↦e \\ a \end{matrix})}; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}d \\ a, b \end{matrix})}; a,b;c⊢d; (\begin{matrix}b, c \\ a \end{matrix}); _{(\begin{matrix}d \\ a \end{matrix})}; a;p⊢d[b,c:=p]; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}d \\ a, b \end{matrix})}; a,b;c⊢d[p:=⟨b,c⟩]; (\begin{matrix}b, c \\ a \end{matrix}); _{(\begin{matrix}d \\ a \end{matrix})}; a;p⊢d; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}e \\ a, b \end{matrix})}; a,b;d⊢fb; _{(\begin{matrix}d \\ a \end{matrix})}; _{(\begin{matrix}b↦e \\ a \end{matrix})}; a;d⊢f; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}e \\ a, b \end{matrix})}; a,b;d⊢e; _{(\begin{matrix}d \\ a \end{matrix})}; _{(\begin{matrix}b↦e \\ a \end{matrix})}; a;d⊢λb.e; a, b; a]

[figure: (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}b, c \\ a \end{matrix}); (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}b, c \\ a \end{matrix}); co□; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; □; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}d \\ a, b \end{matrix})}; a,b;c⊢d; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}d \\ a, b \end{matrix})}; a,b;c⊢d[b,c:=p][p:=⟨b,c⟩]; (\begin{matrix}b, c \\ a \end{matrix}); _{(\begin{matrix}d \\ a \end{matrix})}; a;p⊢d[b,c:=p]; (\begin{matrix}b, c \\ a \end{matrix}); _{(\begin{matrix}d \\ a \end{matrix})}; a;p⊢d[b,c:=p]; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}b, c \\ a \end{matrix})}; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}b, c \\ a \end{matrix})}; co□; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; _{(\begin{matrix}d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; □; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a, b \end{matrix})}; a,b;c⊢d[p:=⟨b,c⟩]; _{(\begin{matrix}b, c \\ a \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; a;p⊢d[p:=⟨b,c⟩][b,c:=p]; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a, b \end{matrix})}; a,b;c⊢d[p:=⟨b,c⟩]; _{(\begin{matrix}b, c \\ a \end{matrix})}; _{(\begin{matrix}d \\ a \end{matrix})}; a;p⊢d]

Conversions Conventions: β-conversions first, then η-conversions. Underlined names are terms. \underline{(b=b)} is the reflexivity term.

(λb.\underline{c})\underline{b} = \underline{c}[\underline{b} =: b]
λb.\underline{f}b = \underline{f}
unpack ⟨\underline{b}, \underline{c}⟩ as ⟨b, c⟩ in \underline{d} = \underline{d}[\underline{b} =: b, \underline{c} =: c]
unpack \underline{(b, c)} as ⟨b, c⟩ in \underline{d}[⟨b, c⟩ =: (b, c)] = \underline{d}[\underline{(b, c)} =: (b, c)]
\underline{d} with b = b via \underline{(b=b)} = \underline{d}
\underline{d}[b =: b′, \underline{(b=b)} =: (b=b)′] with b′ = b via (b=b)′ = \underline{d}

a ⊢ f =^{β} λb.fb
a, b ⊢ e =^{η} (λb.e)b
a, b, c ⊢ d = d[b, c := ⟨b, c⟩]
a, p ⊢ d = d[p := ⟨b, c⟩][b, c := p]
a, b, c ⊢ d = d[with b = b via r]
a, b, b′, e, c ⊢ d = d[b′ := b, e := r][with b′ = b via e]
Γ, x : σ, x′ : σ, Δ ⊢ ρ : Type Γ, x : σ, Δ[x/x′] ⊢ Q : ρ[x/x′]

Γ, x : σ, x′ : σ, z : Eq_{σ}(x, x′), Δ ⊢ (Q with x′ = x via z) : ρ

(weak)

\begin{matrix}a, b, b′, c ⊢ D & a, b, c[b =: b′] ⊢ d : D[b =: b′] \\ a, b, b′, (b = b′), c ⊢ (d with b′ = b via (b = b′)) : D \end{matrix} (weak)

Comprehension categories with unit Jacobs, 10.4.7 (p.616): A fibration p : 𝔼 → 𝔹 with a terminal object functor 1 : 𝔹 → 𝔼 (where we know by lemma 1.8.8 that p ⊣ 1 and that η_{I} = id) is comprehension category with unit if 1 has a right adjoint. We call this right adjoint {−}.

[figure: (\begin{matrix}b \\ a \end{matrix}); (\begin{matrix}∗ \\ c \end{matrix}); (\begin{matrix}∗ \\ c \end{matrix}); (\begin{matrix}e \\ d \end{matrix}); (\begin{matrix}b \\ a \end{matrix}); a; p; (\begin{matrix}∗ \\ c \end{matrix}); c; 1; (\begin{matrix}e \\ d \end{matrix}); d, e; \{−\}; a; c; c; d, e]

Jacobs, 10.4.7 (p.616): Definition of the functor 𝔼 → 𝔹^{→}: its action on objects is X↦pε_{X}.

[figure: 1\{X\}; X; ε_{X}; \{X\}; \{X\}; id; \{X\}; pX; pε_{X}; 1\{X\}; \{X\}; X; \{X\}; X; pX; (\begin{matrix}∗ \\ d, e \end{matrix}); (\begin{matrix}e \\ d \end{matrix}); d, e; d, e; d, e; d; (\begin{matrix}∗ \\ d, e \end{matrix}); d, e; (\begin{matrix}e \\ d \end{matrix}); d, e; (\begin{matrix}e \\ d \end{matrix}); d]

The functor 𝔼 → 𝔹^{→} is a comprehension category, i.e., it takes cartesian morphisms to pullback squares. We want to check that the image of a cartesian morphism is a pullback. Given two maps i↦a and i↦c, d such that a↦c is well-defined, we need to construct a mediating map i↦a, b.

[figure: 1I; \{1I\}; 1I; I; X; \{X\}; X; pX; 1I; I; 1\{Y \}; \{Y \}; Y; \{Y \}; Y; pY; \{1I\}; I; π_{1I}; \{1I\}; I; η_{I}; \{1I\}; \{X\}; \{g\}; I; \{X\}; g^{∨}; 1I; X; g; I; pX; u; \{X\}; pX; π_{X}; X; Y; f; \{X\}; \{Y \}; \{f\}; pX; pY; pf; 1I; 1\{Y \}; 1v; 1\{Y \}; Y; ε_{Y}; I; \{Y \}; v; \{Y \}; \{Y \}; id; \{Y \}; pY; π_{Y}; (\begin{matrix}∗ \\ i \end{matrix}); i; (\begin{matrix}∗ \\ i \end{matrix}); i, ∗; _{(\begin{matrix}b \\ a \end{matrix})}; a, b; _{(\begin{matrix}b \\ a \end{matrix})}; a; _{(\begin{matrix}∗ \\ i \end{matrix})}; i; _{(\begin{matrix}∗ \\ c, d \end{matrix})}; c, d; _{(\begin{matrix}d \\ c \end{matrix})}; c, d; _{(\begin{matrix}d \\ c \end{matrix})}; c; (\begin{matrix}∗ \\ i \end{matrix}); _{(\begin{matrix}b \\ a \end{matrix})}; i, ∗; i; i, ∗; a, b; i; a, b; i; a; _{(\begin{matrix}b \\ a \end{matrix})}; _{(\begin{matrix}d \\ c \end{matrix})}; □; a, b; a; a, b; c, d; a; c; _{(\begin{matrix}∗ \\ i \end{matrix})}; _{(\begin{matrix}∗ \\ c, d \end{matrix})}; _{(\begin{matrix}∗ \\ c, d \end{matrix})}; _{(\begin{matrix}d \\ c \end{matrix})}; i; c, d; c, d; c, d; c, d; c]

Comprehension categories with unit: a bijection Jacobs, 10.4.9 (i): In a CCw1, pack a morphism u : I → J in the base category, and an object Y over J. Then the vertical morphisms 1I → u^{∗}Y are in bijection with morphisms from u to π_{Y} in 𝔹/J.

[figure: 1I; u^{∗}Y; 1I; I; 1I; Y; u^{∗}Y; I; u^{∗}Y; Y; □; u^{∗}Y; Y; I; I; id; I; \{Y \}; I; J; u; Y; \{Y \}; Y; J; \{Y \}; J; π_{Y}; (\begin{matrix}∗ \\ a, b \end{matrix}); (\begin{matrix}c \\ a, b \end{matrix}); (\begin{matrix}∗ \\ a, b \end{matrix}); a, b; (\begin{matrix}∗ \\ a, b \end{matrix}); _{(\begin{matrix}c \\ a \end{matrix})}; (\begin{matrix}c \\ a, b \end{matrix}); a, b; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}c \\ a \end{matrix})}; □; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}c \\ a \end{matrix})}; a, b; a, b; a, b; a, c; a, b; a; _{(\begin{matrix}c \\ a \end{matrix})}; a, c; _{(\begin{matrix}c \\ a \end{matrix})}; a; a, c; a]

Comprehension categories with unit: big bijection Jacobs, 10.4.9 (ii):

[figure: 1L; (Qu^{∗}A)^{∗}1I; (Qu^{∗}A)^{∗}1I; 1I; 1L; u^{′∗}X; (Qu^{∗}A)^{∗}1I; u^{′∗}X; 1I; ∏_{u^{∗}A} u^{′∗}X; 1I; u^{∗} ∏_{A} X; u^{′∗}X; ∏_{u^{∗}A} u^{′∗}X; ∏_{u^{∗}A} u^{′∗}X; u^{∗} ∏_{A} X; u^{′∗}X; X; u^{∗} ∏_{A} X; ∏_{A} X; X; ∏_{A} X; u^{∗}A; A; L; I; Qu^{∗}A; L; J; u′=QA^{∗}u; I; K; u; J; K; QA; L; {X}; {X}; J; π_{X}; I; {∏_{A} X}; {∏_{A} X}; K; π_{∏_{A} X}]

a, c; b ⊢ d a; b ⊢ c↦d

[figure: (\begin{matrix}∗ \\ a, b, c \end{matrix}); (\begin{matrix}∗ \\ a, b, c \end{matrix}); (\begin{matrix}∗ \\ a, b, c \end{matrix}); (\begin{matrix}∗ \\ a, b \end{matrix}); (\begin{matrix}∗ \\ a, b, c \end{matrix}); _{(\begin{matrix}d \\ a, b, c \end{matrix})}; a,b,c⊢d; (\begin{matrix}∗ \\ a, b, c \end{matrix}); _{(\begin{matrix}d \\ a, b, c \end{matrix})}; (\begin{matrix}∗ \\ a, b \end{matrix}); _{(\begin{matrix}c↦d \\ a, b \end{matrix})}; (\begin{matrix}∗ \\ a, b \end{matrix}); _{(\begin{matrix}c↦d \\ a, b \end{matrix})}; a,b⊢c↦d; _{(\begin{matrix}d \\ a, b, c \end{matrix})}; _{(\begin{matrix}c↦d \\ a, b \end{matrix})}; _{(\begin{matrix}c↦d \\ a, b \end{matrix})}; _{(\begin{matrix}c↦d \\ a, b \end{matrix})}; _{(\begin{matrix}d \\ a, b, c \end{matrix})}; _{(\begin{matrix}d \\ a, c \end{matrix})}; _{(\begin{matrix}c↦d \\ a, b \end{matrix})}; _{(\begin{matrix}c↦d \\ a \end{matrix})}; _{(\begin{matrix}d \\ a, c \end{matrix})}; _{(\begin{matrix}c↦d \\ a \end{matrix})}; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}c \\ a \end{matrix})}; a, b, c; a, b; a, b, c; a, c; a, b; a; a, c; a; a, b, c; a, c, d; a, c, d; a, c; a, b; a, (c↦d); a, (c↦d); a]

Comprehension categories with unit: three rules Jacobs, 10.3.3: The categorical interpretation of the rules for dependent sums:

{a, b ⊢ C \atop a; b, c ⊢ (b, c)} ΣI  [figure: (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}b, c \\ a \end{matrix})}; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}b, c \\ a \end{matrix})}; co□; (\begin{matrix}c \\ a, b \end{matrix}); a, b, c; (\begin{matrix}c \\ a, b \end{matrix}); a, b; _{(\begin{matrix}b, c \\ a \end{matrix})}; a, (b, c); _{(\begin{matrix}b, c \\ a \end{matrix})}; a; a, b, c; a, b; a, b, c; a, (b, c); a, b; a; a, (b, c); a]

\begin{matrix}a, (b, c) ⊢ D & a, b, c ⊢ d \\ a, (b, c) ⊢ d \end{matrix} ΣE^{+}  [figure: a, b, c, d; a, b, c; a, b, c, d; a, b, c; a, b, c, d; a, (b, c), d; a, b, c; a, (b, c); a, (b, c), d; a, (b, c); a, (b, c), d; a, (b, c)]

\begin{matrix}a ⊢ D & a, b, c ⊢ d \\ a, (b, c) ⊢ d \end{matrix} ΣE^{−}  [figure: a, b, c; a, b, c; a, b, c; a, b, c, d; a, b, c; a, (b, c), d; a, b, c, d; a, (b, c), d; a, (b, c), d; a, d; a, b, c, d; a, b, c; a, (b, c), d; a, (b, c); a, d; a; a, b, c; a, (b, c); a, (b, c); a]

(Oops, the diagram for ΣE^{−} is wrong)

Interpreting ΠI and ΠE in a CCompC (Jacobs, 10.5.3)

[figure: 1\{X\}; 1I; 1\{X\}; Y; f; 1I; ∏_{X} Y; λ_{X}f; Y; ∏_{X} Y; X; \{X\}; X; I; \{X\}; I; π_{X}; (\begin{matrix}∗ \\ a, b \end{matrix}); (\begin{matrix}∗ \\ a \end{matrix}); (\begin{matrix}∗ \\ a, b \end{matrix}); _{(\begin{matrix}c \\ a, b \end{matrix})}; a,b⊢c; (\begin{matrix}∗ \\ a \end{matrix}); _{(\begin{matrix}b↦c \\ a \end{matrix})}; a⊢(b↦c); _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}b↦c \\ a \end{matrix})}; _{(\begin{matrix}b \\ a \end{matrix})}; a, b; _{(\begin{matrix}b \\ a \end{matrix})}; a; a, b; a]

[figure: 1I; π_{X}^{∗}1I; π_{X}^{∗}1I; 1I; 1I; h^{∨∗}Y; gh; π_{X}^{∗}1I; Y; g^{∧}; 1I; Π_{X}Y; g; h^{∨∗}Y; Y; Y; Π_{X}Y; 1I; X; h; 1I; I; X; \{X\}; X; I; I; \{X\}; h^{∨}; \{X\}; I; π_{X}; (\begin{matrix}∗ \\ a \end{matrix}); (\begin{matrix}∗ \\ a, b \end{matrix}); (\begin{matrix}∗ \\ a, b \end{matrix}); (\begin{matrix}∗ \\ a \end{matrix}); (\begin{matrix}∗ \\ a \end{matrix}); _{(\begin{matrix}c \\ a \end{matrix})}; a⊢c; (\begin{matrix}∗ \\ a, b \end{matrix}); _{(\begin{matrix}c \\ a, b \end{matrix})}; (\begin{matrix}∗ \\ a \end{matrix}); _{(\begin{matrix}b↦c \\ a \end{matrix})}; a⊢(b↦c); _{(\begin{matrix}c \\ a \end{matrix})}; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}b↦c \\ a \end{matrix})}; _{(\begin{matrix}∗ \\ a \end{matrix})}; _{(\begin{matrix}b \\ a \end{matrix})}; a⊢b; _{(\begin{matrix}∗ \\ a \end{matrix})}; a; _{(\begin{matrix}b \\ a \end{matrix})}; a, b; _{(\begin{matrix}b \\ a \end{matrix})}; a; a; a, b; a, b; a]

In the top left vertex of the diagram for ΠE we have omitted an iso to keep the diagram shorter: 1I ≅ h^{∨∗}π_{X}^{∗}1I.

Interpreting ΣI in a CCompC (Jacobs, 10.5.3)

[figure: 1I; f^{∨∗}X; g; 1I; Σ_{X}Y; ⟨f,g⟩; f^{∨∗}X; Y; Y; Σ_{X}Y; f^{∨∗}X; Σ_{X}Y; Y; π_{X}^{∗}Σ_{X}Y; Σ_{X}Y; Σ_{X}Y; id; Σ_{X}Y; π_{X}^{∗}Σ_{X}Y; π_{X}^{∗}Σ_{X}Y; Σ_{X}Y; 1I; X; f; 1I; I; X; \{X\}; X; I; I; \{X\}; f^{∨}; \{X\}; I; π_{X}; (\begin{matrix}∗ \\ a \end{matrix}); _{(\begin{matrix}c \\ a \end{matrix})}; a⊢c; (\begin{matrix}∗ \\ a \end{matrix}); _{(\begin{matrix}b, c \\ a \end{matrix})}; a⊢(b,c); _{(\begin{matrix}c \\ a \end{matrix})}; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}b, c \\ a \end{matrix})}; _{(\begin{matrix}c \\ a \end{matrix})}; _{(\begin{matrix}b, c \\ a \end{matrix})}; _{(\begin{matrix}c \\ a, b \end{matrix})}; _{(\begin{matrix}b, c \\ a, b \end{matrix})}; _{(\begin{matrix}b, c \\ a \end{matrix})}; _{(\begin{matrix}b, c \\ a \end{matrix})}; _{(\begin{matrix}b, c \\ a \end{matrix})}; _{(\begin{matrix}b, c \\ a, b \end{matrix})}; _{(\begin{matrix}b, c \\ a, b \end{matrix})}; _{(\begin{matrix}b, c \\ a \end{matrix})}; _{(\begin{matrix}∗ \\ a \end{matrix})}; _{(\begin{matrix}b \\ a \end{matrix})}; a⊢b; _{(\begin{matrix}∗ \\ a \end{matrix})}; a; _{(\begin{matrix}b \\ a \end{matrix})}; a, b; _{(\begin{matrix}b \\ a \end{matrix})}; a; a; a, b; a, b; a]

Interpreting ΣE^{+} in a CCompC (Jacobs, 10.5.3)

[figure: (\begin{matrix}∗ \\ a, b, c \end{matrix}); (\begin{matrix}d \\ a, b, c \end{matrix}); a,b,c⊢d; (\begin{matrix}∗ \\ a, b, c \end{matrix}); a, b, c; (\begin{matrix}d \\ a, b, c \end{matrix}); a, b, c, d; (\begin{matrix}d \\ a, b, c \end{matrix}); a, b, c; (\begin{matrix}c \\ a, b \end{matrix}); a, b, c; (\begin{matrix}c \\ a, b \end{matrix}); a, b; (\begin{matrix}b \\ a \end{matrix}); a, b; (\begin{matrix}b \\ a \end{matrix}); a; a, b, c; a, b, c, d; a, b, c, d; a, b, c; a, b, c; a, b; a, b; a; _{(\begin{matrix}∗ \\ a, (b, c) \end{matrix})}; _{(\begin{matrix}d \\ a, (b, c) \end{matrix})}; a,(b,c)⊢d; _{(\begin{matrix}∗ \\ a, (b, c) \end{matrix})}; a, (b, c); _{(\begin{matrix}d \\ a, (b, c) \end{matrix})}; a, (b, c), d; _{(\begin{matrix}d \\ a, (b, c) \end{matrix})}; a, (b, c); _{(\begin{matrix}b, c \\ a \end{matrix})}; a, (b, c); _{(\begin{matrix}b, c \\ a \end{matrix})}; a; a, (b, c); a, (b, c), d; a, (b, c), d; a, (b, c); a, (b, c); a; a, b, c; a, (b, c); a, b, c, d; a, (b, c), d; a, b, c; a, (b, c); a, b; a; (\begin{matrix}∗ \\ a, b, c \end{matrix}); _{(\begin{matrix}∗ \\ a, (b, c) \end{matrix})}; (\begin{matrix}∗ \\ a, b, c \end{matrix}); _{(\begin{matrix}∗ \\ a, (b, c) \end{matrix})}; □; (\begin{matrix}d \\ a, b, c \end{matrix}); _{(\begin{matrix}d \\ a, (b, c) \end{matrix})}; (\begin{matrix}d \\ a, b, c \end{matrix}); _{(\begin{matrix}d \\ a, (b, c) \end{matrix})}; □; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}b, c \\ a \end{matrix})}; (\begin{matrix}c \\ a, b \end{matrix}); _{(\begin{matrix}b, c \\ a \end{matrix})}; co□]

[figure: 1\{Y \}; κ^{∗}Z; h; 1\{Y \}; \{Y \}; κ^{∗}Z; \{κ^{∗}Z\}; κ^{∗}Z; \{Y \}; Y; \{Y \}; Y; \{X\}; X; \{X\}; X; I; \{Y \}; \{κ^{∗}Z\}; h^{∨}; \{κ^{∗}Z\}; \{Y \}; π_{κ^{∗}Z}; \{Y \}; \{X\}; π_{Y}; \{X\}; I; π_{X}; 1\{∐_{X} Y \}; Z; (κ^{−1};\overline{h})^{∧}; 1\{∐_{X} Y \}; \{∐_{X} Y \}; Z; \{Z\}; Z; \{∐_{X} Y \}; ∐_{X} Y; \{∐_{X} Y \}; ∐_{X} Y; I; \{∐_{X} Y \}; \{Z\}; κ^{−1};\overline{h}; \{Z\}; \{∐_{X} Y \}; π_{Z}; \{∐_{X} Y \}; I; π_{\{∐_{X} Y \}}; \{Y \}; \{∐_{X} Y \}; κ; \{κ^{∗}Z\}; \{Z\}; \{Y \}; \{∐_{X} Y \}; κ; \{X\}; I; π_{X}; 1\{Y \}; 1\{∐_{X} Y \}; 1\{Y \}; 1\{∐_{X} Y \}; 1κ; κ^{∗}Z; Z; κ^{∗}Z; Z; □; Y; ∐_{X} Y; Y; ∐_{X} Y; co□]

The “unpack” rule (2) In 10.1.2 Jacobs defines (for P : σ × τ):

πP =^{def} unpack P as ⟨x, y⟩ in x
π′P =^{def} unpack P as ⟨x, y⟩ in y

i.e.,

\begin{aligned}πP & := & x[x, y := P] \\ π′P & := & y[x, y := P] \end{aligned}

Rules for DTT

                a|-b  a|-B=B'
Conversion:     -------------
                    a|-b'
                 a|-B
Projection:     ------
                a,b|-b
                a,b,b',c|-D       a,b,b',c|-d
Contraction:    -----------       -----------
                 a,b,c|-D          a,b,c|-d
                a|-b  a,b,c|-D    a|-b  a,b,c|-d
Substitution:   --------------    --------------
                    a,c|-D           a,c|-d
                a|-B  a|-C        a|-B  a|-c
Weakening:      ----------        ----------
                  a,b|-C            a,b|-c
                a,b,c,d|-E        a,b,c,d|-e
Exchange:       ----------        ----------
                a,c,b,d|-E        a,c,b,d|-e
                Type:             Intro:          Elim:
                                                   a|-*'
Singleton:       ---               ---           -------
                 |-1               |-*           a|-*'=*
               a,b|-C             a,b|-c      a|-b  a|-b|->c
DepProds:     ---------          --------     --------------
              a|-Πb:B.C          a|-b|->c         a|-c
               a,b|-C          a|-B  a,b|-C
DepSums:      ---------        ------------     (see below)
              a|-Σb:B.C        a,b,c|-(b,c)
                a|-B               a|-B
Equality:   ---------------     ----------      (see below)
            a,b,b'|-W[b=b']     a,b|-(b=b)
Elimination rules:
                 DepSums:                  Equality:
              a|-D  a,b,c|-d          a,b,b',c|-D  a,b,c|-d
Weak:         --------------          ---------------------
                a,(b,c)|-d              a,b,b',(b=b'),c|-d
            a,(b,c)|-D  a,b,c|-d     a,b,b',(b=b')|-C  a,b|-c
Strong:     --------------------     ------------------------
                 a,(b,c)|-d             a,b,b',(b=b')|-c
             a|-b,c    a|-b,c       a|-(b=b')      a|-(b=b)'
AltStrong:   ------    ------       ---------   ---------------
              a|-b      a|-c         a|-b=b'    a|-(b=b)'=(b=b)