PRESHEAF TYPE THEORIES

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

BIBLIOGRAPHY

[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 [8]. Alexis LAOUAR. A presheaf model of dependent type theory

VIDEO

The companion video for [1] source.