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.

INTRO

(Presheaf over ).
A presheaf over a category is a functor
from to the category of .
We denote as and as ,
identity morphisms ,
composition for , .
This means a presheaf is given by a family of sets
and restriction maps , for
satisfying the laws and for
. The family of sets 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)
, such that
then this is cohomology presheaf; ii) if the restriction map is a process action
then this is process presheaf;
iii) if the restriction map actually restricts the domain the such presheaf is
called topological (default meaning).

(Yoneda presheaf ).
Any object of base category defines a
presheaf represented by .
This presheaf assigns to each object in
the set of arrows . Given anarrow
composition with f maps an arrow to an arrow .
In other words
then a set of maps and the restriction maps defined by composition.

(Seive).
A sieve on is a set of maps with codomain such that
is in whenever is in and .

(Subpresheaf ).
Subpresheaf of a presheaf A is a map , which
for each selects a subset of of shape defined by polyhedron A.
is a presheaf where is a set of decidable seives,
so that we can decide if is a member of .

DEPENDENT TYPES

(Type).
A type is interpreted as a presheaf , a family of sets with restriction maps
for . A dependent type
B on A is interpreted by a presheaf on category of elements of : the objects
are pairs with and morphisms are
maps such that . A dependent type B is thus given
by a family of sets and restriction maps .

We think of as a type and as a family of presheves varying .
The operation generalizes the semantics of
implication in a Kripke model.

(Pi). An element is a family
of functions for such
that when and .

(Sigma). The set is the set
of pairs when and restriction map .

SIMPLICIAL TYPES

(Simplicial Types).
The simplicial type is defined as a presheaf on category of
finite linear posets and monotone maps. Let's write a presheaf
as . In a sense that this
is a category on a shapes, the notion of subpolyhedras is then
represented by subpresheaves.

().
The category of simplicial types denoted .

CUBICAL TYPES

(Cubical Presheaf ).
The identity types modeled with another presheaf, the presheaf on Lawvere
category of distributive lattices (theory of de Morgan algebras) denoted
with .

. The presheaf :
i) has to distinct global elements and (B);
ii) (I) has a decidable equality for each (B);
iii) is tiny so the path functor has right adjoint (B).;
iv) has meet and join (connections, B).

NOTE: In the simplicial model B condition is underivable.

(Cofibrations Subpresheaf ).
The subpresheaf corresponds to a map
so that can
be seen internally as the subpresheaf of propositions in
satisfying the property (which
reads ‘ is cofibrant’). In other words
classified cofibrant maps.

:
i) cofibrant maps should contain isomorphisms and be closed under composition (A);
ii) is closed under disjunction:
(A).

. This properties defined how we can mix the
contexts of depedent types and cubical types:
i) wedge (C);
ii) cofibrations (C).

NOTE: B could be replaced with strengthened
C.

:
i) — free monoidal category on interval ;
ii) — free monoidal category on interval with connections and ;
iii) — free symmetric monoidal category on interval;
iv) — free cartesian category on interval;
v) — free cartesian category on distributive lattice.

NOTE: the cartesian cube category is the opposite of
the category of finite, strictly bipointed sets: .

Theorem (Awodey).
The category of cubical types (presheaves on ) is the
classifying topos of strictly bipointed objects . Geometric
realisation preserves finite products.

SIMPLIFICATION

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.2.2.2.1) 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.2.2.2.1) a (star g a M.2.2.2.1))
* ((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