This article requires as prerequisites an article about the formalization of the category theory and topos theory: Formal Set Topos. Presheaf model of type theory could be seen as generalization of the notion of Kripke model.

$$\def\mapright#1{\xrightarrow{{#1}}} \def\mapdown#1{\Big\downarrow\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagl#1{\vcenter{\searrow}\rlap{\raise2pt{\scriptstyle{#1}}}} \def\mapdiagr#1{\vcenter{\swarrow}\rlap{\raise2pt{\scriptstyle{#1}}}} $$


Definition (Presheaf over $C$). A presheaf over a category $C$ is a functor from $C^{op}$ to the category of $\mathrm{Set}$. We denote $\mathrm{Ob}_C$ as $I,J,K$ and $\mathrm{Hom}_C$ as $f,g$, identity morphisms $1_I : I \rightarrow I$, composition $f\ g : K \rightarrow I$ for $g : K \rightarrow J$, $f : I \rightarrow J$. This means a presheaf $\mathrm{PSh}_C$ is given by a family of sets $C_I$ and restriction maps $u \mapsto u\ f$, $C_I \rightarrow C_J$ for $f:J \rightarrow I$ satisfying the laws $u\ 1_I = u$ and $(u\ f)\ g=u\ (f\ g)$ for $g:K \rightarrow J$. The family of sets $C_I$ is called right action.

By the nature of the rescription maps we could classify presheaves: i) if the restriction map forms a boundary operator (degeneracy map) $\sigma : u_{n} \mapsto v_{n-1}$, such that $\sigma \sigma = 0$ then this is cohomology presheaf; ii) if the restriction map is a process action $\pi : s_{n} \mapsto s_{n+1}$ then this is process presheaf; iii) if the restriction map actually restricts the domain the such presheaf is called topological (default meaning).

Definition (Yoneda presheaf $\mathrm{Yo}_X$). Any object $X$ of base category $C$ defines a presheaf $\mathrm{Yo}_X$ represented by $X$. This presheaf $\mathrm{Yo}_X$ assigns to each object $I$ in $C$ the set of arrows $I \rightarrow X$. Given anarrow $f:J \rightarrow I$ composition with f maps an arrow $I \rightarrow X$ to an arrow $J \rightarrow X$. In other words $\mathrm{Yo}_X(J)$ then a set of maps $I \rightarrow J$ and the restriction maps defined by composition.

Definition (Seive). A sieve $S$ on $I$ is a set of maps with codomain $I$ such that $f g: K \rightarrow I$ is in $S$ whenever $f : J \rightarrow I$ is in $S$ and $g : K \rightarrow J$.

Definition (Subpresheaf $\Omega(I)$). Subpresheaf of a presheaf A is a map $A \rightarrow \Omega_d(I)$, which for each $I$ selects a subset of $A(I)$ of shape $I$ defined by polyhedron A. $\Omega_d(I)$ is a presheaf where $\Omega_d(I)$ is a set of decidable seives, so that we can decide if $f: I \rightarrow J$ is a member of $S$.


Definition (Type). A type is interpreted as a presheaf $A$, a family of sets $A_I$ with restriction maps $u \mapsto u\ f, A_I \rightarrow A_J$ for $f: J\rightarrow I$. A dependent type B on A is interpreted by a presheaf on category of elements of $A$: the objects are pairs $(I,u)$ with $u : A_I$ and morphisms $f: (J,v) \rightarrow (I,u)$ are maps $f : J \rightarrow$ such that $v = u\ f$. A dependent type B is thus given by a family of sets $B(I,u)$ and restriction maps $B(I,u) \rightarrow B(J,u\ f)$.

We think of $A$ as a type and $B$ as a family of presheves $B(x)$ varying $x:A$. The operation $\Pi(x:A)B(x)$ generalizes the semantics of implication in a Kripke model.

Defintion (Pi). An element $w:[\Pi(x:A)B(x)](I)$ is a family of functions $w_f : \Pi(u:A(J))B(J,u)$ for $f : J \rightarrow I$ such that $(w_f u)g=w_{f\ g}(u\ g)$ when $u:A(J)$ and $g:K\rightarrow J$.

Defintion (Sigma). The set $\Sigma(x:A)B(x)$ is the set of pairs $(u,v)$ when $u:A(I),v:B(I,u)$ and restriction map $(u,v)\ f=(u\ f,v\ f)$.


Definition (Simplicial Types). The simplicial type is defined as a presheaf on category of finite linear posets $[n]$ and monotone maps. Let's write a presheaf as $\mathrm{X}: \Delta^{op} \rightarrow \mathrm{Set}$. In a sense that this is a category on a shapes, the notion of subpolyhedras is then represented by subpresheaves.

Definition ($\mathrm{sSet}$). The category of simplicial types denoted $\mathrm{sSet}$.


Definition (Cubical Presheaf $\mathbb{I}$). The identity types modeled with another presheaf, the presheaf on Lawvere category of distributive lattices (theory of de Morgan algebras) denoted with $\Box$ — $\mathbb{I} : \Box^{op} \rightarrow \mathrm{Set}$.

Properties of $\mathbb{I}$. The presheaf $\mathbb{I}$: i) has to distinct global elements $0$ and $1$ (B$_1$); ii) $\mathbb{I}$(I) has a decidable equality for each $I$ (B$_2$); iii) $\mathbb{I}$ is tiny so the path functor $X \mapsto X^\mathbb{I}$ has right adjoint (B$_3$).; iv) $\mathbb{I}$ has meet and join (connections).

NOTE: In the simplicial model B$_3$ condition is underivable.

Definition (Cofibrations Subpresheaf $\mathbb{F}$). The subpresheaf $\mathbb{F}$ corresponds to a map $\mathrm{Cofib} : \Omega \rightarrow \Omega$ so that $\mathbb{F}$ can be seen internally as the subpresheaf of propositions $\varphi$ in $\mathbb{F}$ satisfying the property $\mathrm{Cofib}\ (\varphi)$ (which reads ``$\varphi$ is cofibrant''). In other words $\mathbb{F}$ classified cofibrant maps.

Properties of $\mathbb{F}$: i) cofibrant maps should contain isomorphisms and be closed under composition (A$_1$); ii) $\mathbb{F}$ is closed under disjunction: $\mathrm{Cofib}\ (\varphi_2) \rightarrow \mathrm{Cofib}\ (\varphi_1) \rightarrow \mathrm{Cofib}\ (\varphi_1 \wedge \varphi_2)$ (A$_2$).

Mixing Properties. This properties defined how we can mix the contexts of depedent types and cubical types: i) wedge $\forall\ (i: \mathbb{I})\ \mathrm{Cofib}\ (i=0) \wedge \mathrm{Cofib}\ (i=1)$ (C$_1$); ii) cofibrations $\forall\ (i: \mathbb{I})\ \mathrm{Cofib}\ (\phi) \rightarrow \mathrm{Cofib}\ (\forall(i: \mathbb{I})\ \phi))$ (C$_2$).

NOTE: B$_4$ could be replaced with strengthened C$_1$ — $\forall\ (i:\mathbb{I})\ \mathrm{Cofib}\ (i = j)$.

Cubical Flavors: i) $\Box_m$ — free monoidal category on interval $1 \rightarrow I \leftarrow 1$; ii) $\Box_{mc}$ — free monoidal category on interval with connections $\vee$ and $\wedge$; iii) $\Box_s$ — free symmetric monoidal category on interval; iv) $\Box_c$ — free cartesian category on interval; v) $\Box_d$ — free cartesian category on distributive lattice.

NOTE: the cartesian cube category $\Box_c$ is the opposite of the category $\mathbb{B}$ of finite, strictly bipointed sets: $\Box_c =_{def} \mathbb{B}^{op}$.

Theorem (Awodey). The $\mathrm{cSet}$ category of cubical types (presheaves on $\Box$) is the classifying topos of strictly bipointed objects $(X,a,b,a \neq b)$. Geometric realisation $\mathrm{cSet} \rightarrow \mathrm{Top}$ preserves finite products.


What if we take not a category as the underlying objects for sheaves but monoidal structure just to simplify the model?

isPSh (G: U) (M: monoid): U = (c: G -> M.1.1 -> G) * (left: (g: G) -> Path G (c g M. g) * ((g: G) (t r: M.1.1) -> Path G (c (c g t) r) (c g (M.2.1 t r))) PSh (M: monoid): U = (G: U) * (isPSh G M) NatPSh (M: monoid) (D G: PSh M): U = (sigma: D.1 -> G.1) * ((s: D.1)(t: M.1.1) -> Path G.1 (G.2.1 (sigma s) t) (sigma (D.2.1 s t)))
isType (M: monoid) (G: PSh M) (A: G.1 -> U): U = (star: (g: G.1) -> A g -> (t: M.1.1) -> A (G.2.1 g t)) * (coe1: (g: G.1) (t: M.1.1) -> Path U (A g) (A (G.2.1 g t))) * (coe2: (g: G.1) (t r: M.1.1) -> Path U (A(G.2.1(G.2.1 g t)r))(A(G.2.1 g(M.2.1 t r)))) * (left: (g: G.1) (a: A g) -> PathP (coe1 g M. a (star g a M. * ((g:G.1)(a:A g) (t r: M.1.1) -> PathP (coe2 g t r) (star (G.2.1 g t) (star g a t) r) (star g a (M.2.1 t r)))
Ctx: monoid -> U = PSh Type (M: monoid) (G: PSh M): U = (A: G.1 -> U) * isType M G A Substitution: (M: monoid) -> Ctx M -> Ctx M -> U = NatPSh


[1]. Thierry Coquand. A Survey of Constructive Presheaf Models of Univalence. [2]. Mark Bickford. Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. [3]. Chuangjie Xu. A Continuous Computational Interpretation of Type Theories. [4]. Thierry Coquand, Bassel Mannaa, Fabian Ruch. Stack Semantics of Type Theory. [5]. Ian Orton, Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. [6]. Thierry Coquand, Simon Huber, Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory [7]. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom


The companion video for [1] source.