Groupoid and Path-Object Models of Intensional Type Theory

Proof. The product of two categories is a category, and an arrow $(p,q)$ is invertible as soon as both components are, with inverse $(p^{-1},q^{-1})$. For the exponential, a natural transformation $\alpha$ between functors into a groupoid is invertible: each component ${\alpha }_{\gamma }$ has an inverse in $\mathrm{\Delta }$, and the family $({\alpha }_{\gamma }^{-1})$ is natural because inverting the naturality square of $\alpha$ at $p$ gives the naturality square of ${\alpha }^{-1}$ at $p$. The adjunction is the usual currying of functors, which restricts to groupoids because every construction involved preserves invertibility. ◻

Proof. Composition of functors is strictly associative and unital, and both clauses of definition 152.6 are defined by composition on objects and on arrows. The two equations for $M$ hold because they are the corresponding equations for the underlying assignments, and the functoriality conditions are preserved: if $M(p^{\prime }\circ p)=M(p^{\prime })\circ (p^{\prime }\cdot M(p))$ holds in $\mathrm{\Gamma }$, applying $F$ to arrows gives the same equation in $\mathrm{\Delta }$. ◻

Proof. Associativity: both bracketings of $(p^{″},q^{″})\circ (p^{\prime },q^{\prime })\circ (p,q)$ have first component $p^{″}\circ p^{\prime }\circ p$ and second component $q^{″}\circ (p^{″}\cdot q^{\prime })\circ (p^{″}{p}^{\prime }\cdot q)$, using functoriality of $A$ to identify $p^{″}\cdot (p^{\prime }\cdot q)$ with $(p^{″}\circ p^{\prime })\cdot q$. Units are immediate from $A(\mathsf{id})=\mathsf{id}$. Inverses: composing $(p,q)$ with the displayed inverse gives first component ${\mathsf{id}}_{\gamma }$ and second component $(p^{-1}\cdot q^{-1})\circ (p^{-1}\cdot q)=p^{-1}\cdot (q^{-1}\circ q)=\mathsf{id}$, and symmetrically on the other side. For ${\mathbf{q}}_A$: its arrow component at $(p,q)$ must be an arrow $(p,q)\cdot {\mathbf{q}}_A(\gamma ,a)\to {\mathbf{q}}_A({\gamma }^{\prime },a^{\prime })$ in $A[{\mathbf{p}}_A]({\gamma }^{\prime },a^{\prime })=A({\gamma }^{\prime })$, that is $p\cdot a\to a^{\prime }$, and $q$ is such an arrow. The two dependent-object equations are the identity and composition clauses just verified. ◻

Proof. Functoriality of $⟨F,M⟩$ is the pair of the functoriality of $F$ and the two dependent-object equations of $M$: for composable $q,q^{\prime }$ in $\mathrm{\Delta }$, The two equations hold by construction. Uniqueness: an object of $\mathrm{\Gamma }.A$ is a pair and an arrow is a pair, so a functor $H$ into it is determined by ${\mathbf{p}}_A\circ H$ and by ${\mathbf{q}}_A[H]$, which are exactly the two components. The category laws for $\mathbf{Gpd}$ and strict functoriality of reindexing are lemma 152.7. ◻

Proof. Well-typedness: for $s:a_1\to a_2$ in $A(\gamma )$ the composite $q_2\circ (p\cdot s)\circ q_1^{-1}$ goes $a_1^{\prime }\to p\cdot a_1\to p\cdot a_2\to a_2^{\prime }$, an arrow of $A({\gamma }^{\prime })$. Identity: at $(\mathsf{id},\mathsf{id},\mathsf{id})$ the formula returns $s$. Composition: applying $(p^{\prime },q_1^{\prime },q_2^{\prime })$ after $(p,q_1,q_2)$ gives $$q_2^{\prime }\circ (p^{\prime }\cdot (q_2\circ (p\cdot s)\circ q_1^{-1}))\circ q_1^{\prime -1}=(q_2^{\prime }\circ (p^{\prime }\cdot q_2))\circ ((p^{\prime }\circ p)\cdot s)\circ (q_1^{\prime }\circ (p^{\prime }\cdot q_1){)}^{-1},$$ which is the formula for the composite arrow of ${\mathrm{\Gamma }}_A$ computed in construction 152.8. Since the values are discrete, a dependent object of $I_A[\mathsf{diag}]$ is an assignment of an arrow $a\to a$ for each $(\gamma ,a)$ subject to the equation $I_A(p,q,q)(r_A(\gamma ,a))=r_A({\gamma }^{\prime },a^{\prime })$; and indeed $q\circ (p\cdot {\mathsf{id}}_a)\circ q^{-1}={\mathsf{id}}_{a^{\prime }}$. ◻

Proof. An arrow of ${\mathrm{\Gamma }}_A.I_A$ over $(p,q_1,q_2)$ is a pair whose second component is an arrow in the discrete groupoid $I_A({\gamma }^{\prime },a_1^{\prime },a_2^{\prime })$, hence exists exactly when $I_A(p,q_1,q_2)(s)=s^{\prime }$. With $p=\mathsf{id}$, $q_1={\mathsf{id}}_{a_1}$, $q_2=s$ and source datum ${\mathsf{id}}_{a_1}$ the condition reads $s\circ {\mathsf{id}}_{a_1}\circ {\mathsf{id}}_{a_1}^{-1}=s$, which holds. At $s={\mathsf{id}}_a$ the arrow is $(\mathsf{id},\mathsf{id},\mathsf{id},\star )$, the identity. ◻

Proof. The object part is well typed by lemma 152.13: the element $d(\gamma ,a_1)$ lies in $C(\gamma ,a_1,a_1,{\mathsf{id}}_{a_1})$, and transporting it along $f(u)$ lands in $C(u)$.

For the arrow part write $u=(\gamma ,a_1,a_2,s)$ and $u^{\prime }=({\gamma }^{\prime },a_1^{\prime },a_2^{\prime },s^{\prime })$, so that $q_i:p\cdot a_i\to a_i^{\prime }$ and, because the second components of arrows of ${\mathrm{\Gamma }}_A.I_A$ exist only when the discrete condition holds, $$q_2\circ (p\cdot s)=s^{\prime }\circ q_1.$$ Since $d$ is a dependent object and $(p,q_1):(\gamma ,a_1)\to ({\gamma }^{\prime },a_1^{\prime })$ is an arrow of $\mathrm{\Gamma }.A$, $$d(p,q_1):(p,q_1,q_1,\star )\cdot d(\gamma ,a_1)\to d({\gamma }^{\prime },a_1^{\prime }).$$ Applying $f(u^{\prime })\cdot -$ and using functoriality of $C$ gives an arrow $$(f(u^{\prime })\circ (p,q_1,q_1,\star ))\cdot d(\gamma ,a_1)\to f(u^{\prime })\cdot d({\gamma }^{\prime },a_1^{\prime })=\mathsf{J}(C,d)(u^{\prime }).$$ It remains to identify the source. Composing in ${\mathrm{\Gamma }}_A.I_A$, $$f(u^{\prime })\circ (p,q_1,q_1,\star )=(\mathsf{id},{\mathsf{id}}_{a_1^{\prime }},s^{\prime },\star )\circ (p,q_1,q_1,\star )=(p,q_1,s^{\prime }\circ q_1,\star ),$$ while $$h\circ f(u)=(p,q_1,q_2,\star )\circ (\mathsf{id},{\mathsf{id}}_{a_1},s,\star )=(p,q_1,q_2\circ (p\cdot s),\star ).$$ By (152.1) the two agree, so the source is $(h\circ f(u))\cdot d(\gamma ,a_1)=h\cdot \mathsf{J}(C,d)(u)$, which is what a dependent object requires. The two functoriality equations for $\mathsf{J}(C,d)$ follow from those of $d$ and of $C$ by the same computation.

Computation: at $u=(\gamma ,a,a,{\mathsf{id}}_a)$ the arrow $f(u)$ is the identity by lemma 152.13, so $\mathsf{J}(C,d)(u)=d(\gamma ,a)$; and at an arrow $(p,q,q,\star )$ the same lemma gives $\mathsf{J}(C,d)(p,q,q,\star )=f({\gamma }^{\prime },a^{\prime },a^{\prime },\mathsf{id})\cdot d(p,q)=d(p,q)$. Hence $\mathsf{J}(C,d)[\mathsf{refl}]=d$ as dependent objects. ◻

Proof. By definition 152.11 the fibre $I_{A_0}(\ast ,\ast )$ is the discrete groupoid on ${\mathrm{hom}}_{A_0}(\ast ,\ast )=\{\mathsf{id},g\}$, a two-element set. A dependent object $u$ of the displayed $\mathrm{\Pi }$-type would in particular supply, at the objects $x=y=\ast$, $p=g$, $q=\mathsf{id}$, an object of $$I_{I_{A_0}}(\ast ,\ast ,g,\mathsf{id})=\mathrm{\Delta }({\mathrm{hom}}_{I_{A_0}(\ast ,\ast )}(g,\mathsf{id})).$$ The groupoid $I_{A_0}(\ast ,\ast )$ is discrete and $g\ne \mathsf{id}$, so that hom-set is empty and the required object does not exist. Underivability follows from soundness of the interpretation (theorem 54.28 applied to $\mathcal{G}$): a derivation would produce such a dependent object. ◻

Proof. $C$ is a family: an arrow $(q,\star ):(a,p)\to (a^{\prime },p^{\prime })$ of $\mathrm{\Theta }$ exists exactly when $q\circ p\circ q^{-1}=p^{\prime }$, and in a groupoid this forces $p={\mathsf{id}}_a$ if and only if $p^{\prime }={\mathsf{id}}_{a^{\prime }}$; so the two fibres are simultaneously empty or singletons and the identity assignment is functorial. The object $d$ exists because $C(a,{\mathsf{id}}_a)$ is a singleton. Finally $C(\ast ,g)$ is empty, since $g\ne \mathsf{id}$, so no dependent object of $C$ exists.

For the last claim, suppose $\mathcal{G}$ carried an operation $\mathsf{K}$ sending $C$ and $d$ as above to an element of $\mathrm{Tm}(\mathrm{\Theta },C)$; the previous paragraph shows that set is empty. ◻

Proof. The displayed descriptions are definition 152.11 applied to the $\mathrm{\Sigma }$-structure of definition 54.33 and to the fibre. Take $A:=\mathrm{B}(\mathbb{Z}/2\mathbb{Z})$ with $a=\ast$, and $B$ the family with $B(\ast ):=\mathrm{\Delta }(\{b,b^{\prime }\})$ and $B(g)$ the swap. Then $(g,{\mathsf{id}}_{b^{\prime }})$ is an element of the first set, because $g\cdot b=b^{\prime }$. The second set is the hom-set from $b$ to $b^{\prime }$ in a discrete groupoid with $b\ne b^{\prime }$, which is empty. ◻

Proof. Immediate from definition 152.11: the identity family of a type is its family of hom-sets, and the hom-sets of $\mathbf{Gpd}(\mathcal{V})$ are by definition 152.21 the sets of isomorphisms. For the refutation take $X=Y=\mathrm{\Delta }(\{0,1\})$. Its isomorphisms are the two bijections of a two-element set, so $I_{\mathcal{U}}(X,X)$ is the discrete groupoid on a set with two elements; the argument of theorem 152.17, applied to the identity and the swap in place of $\mathsf{id}$ and $g$, shows that $\mathsf{UIP}(\mathcal{U})$ has no dependent object. ◻

Proof. The $\mathrm{\Pi }$-structure of definition 54.33 takes $\mathrm{\Pi }(A,B)(\gamma )$ to be the groupoid of sections of the restricted family with vertical natural transformations as arrows. Applying definition 152.11 to that groupoid gives the stated fibre. A term of $\prod _{a:A}{\mathsf{Id}}_B(fa,f^{\prime }a)$ is precisely a family of arrows $f(\gamma )(a)\to f^{\prime }(\gamma )(a)$ whose dependent-object equation is the naturality condition, so it is exactly an element of the fibre. ◻

Proof. Stability. Given a pullback of $e$ along $f$, an object of the pullback is a pair $(a,x)$ with $f(a)=e(x)$, and an arrow out of it in the base lifts by lifting its $e$-component and pairing.

$(s,t)$ is an isofibration. An object of $X^{\mathbb{I}}$ is an arrow $w:x_1\to x_2$ of $X$; an arrow of $X^{\mathbb{I}}$ is a commuting square. Given $w$ and arrows $u_1:x_1\to y_1$, $u_2:x_2\to y_2$ in $X$, the arrow $w^{\prime }:=u_2\circ w\circ u_1^{-1}$ is an object of $X^{\mathbb{I}}$ and $(u_1,u_2)$ is an arrow $w\to w^{\prime }$ over $(u_1,u_2)$; this is the required lift, and it is exactly the reindexing formula of definition 152.11.

Lifting against $r$. Let $e:E\to B$ be an isofibration and let a square be given with $r$ on the left: that is, a functor $k:X\to E$, a functor $\ell :PX\to B$ with $\ell \circ r=e\circ k$. For an object $w:x_1\to x_2$ of $PX$ the arrow $\ell (\mathsf{id},w):\ell (r{x}_1)\to \ell (w)$ of $B$ has source $e(k(x_1))$; lift it to an arrow ${\xi }_w:k(x_1)\to z_w$ of $E$ and put $m(w):=z_w$. Choosing the lift to be the identity when $w$ is an identity arrow makes $m\circ r=k$ on the nose, and the arrow part of $m$ is determined by conjugating the chosen lifts, exactly as in the proof of theorem 152.14. Then $e\circ m=\ell$ because $e$ was applied to the chosen lifts. ◻

Proof. By construction 152.8 an object of $(A\times A).I_A$ is a triple $(a_1,a_2,s)$ with $s:a_1\to a_2$, and an arrow is a pair $(q_1,q_2)$ with $q_2\circ s\circ q_1^{-1}=s^{\prime }$. An object of $A^{\mathbb{I}}$ is an arrow of $A$ and an arrow is a commuting square, which is the same condition. The assignment $(a_1,a_2,s)\mapsto s$ is a functor with an evident inverse, commutes with the projections to $A\times A$, and carries $r_A$ to $r$. ◻