module cwf where {- Here is a short informal description of categorical semantics of dependent type theory given by Peter Dybjer. The code is by Thierry Coquand ported to cubical by 5HT. http://www.cse.chalmers.se/~peterd/papers/Ise2008.pdf Another good intro to LCCC was a 80-514 course at CMU: http://math.cmu.edu/~cnewstea/talks/20170301.pdf Definition (Fam). The Fam is the category of families of sets where objects are dependent function spaces (x:A)->B(x) and morphisms with domain Pi(A,B) and codomain Pi(A',B') are pairs of functions A',g(x:A):B(x)->B'(f(x))>. Definition (Derivability). Ctx|-A = (c:Ctx) -> A(c). Definition (Comprehension). Ctx;A = (c:Ctx) * A(c). Statement. Comprehension is not assoc. G;A;B =/= G;B;A Definition (Context).The C is context category where objects are contexts and morphisms are substitutions. Terminal object G=0 in C is called empty context. Context comprehension operation G;A = (x:G)*A(x) and its eliminators: p:G;A |- G, q: G;A |- A(p) such that universal property holds: for any D:ob(C), morphism g:D->G, and term a:D->A there is a unique morphism s=:D->G;A such that p.s=g and q(s)=a. Statement. Subst is assoc. g(g(G,x,a),y,b) = g(g(G,y,b),x,a) Definition (CwF-object). A CwF-object is a Sigma(C,C->Fam) of context category C with contexts as objects and substitutions as morphisms and functor T:C->Fam where object part is a map from a context G of C to famility of sets of terms G |- A and morphism part is a map from substitution g:D->G to a pair of functions which perform substitutions of g in terms and types respectively. Definition (CwF-morphism). Let (C,T):ob(C) where T:C->Fam. A CwF-morphism m: (C,T)->(C',T') is a pair C',s:T->T'(F)> where F is a functor and s is a natural transformation. Definition (Category of Types). Let we have CwF with (C,T) objects and (C,T)->(C',T') mophisms. For a given context G in Ob(C) we can construct a Type(G) -- the category of types in context G with set of types in contexts as objects as and functions f:G;A->B(p) as morphisms. Definition (Local Cartesian Closed Category). LCCC(C) = Sigma(C,(A:ob C)->CCC(C/A)). [1]. Alexandre Buisse, Peter Dybjer. The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories -- an Intuitionistic Perspective. [2]. Martin Hofmann, Thomas Streicher. The groupoid interpretation of type theory. [3]. Pierre Clairambault. From Categories with Families to Locally Cartesian Closed Categories. [4]. Andreas Abel, Thierry Coquand, Peter Dybjer. On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. [5]. R.A.G. Seely. Locally cartesian closed categories and type theory. [6]. Pierre-Louis Curien, Richard Garner, Martin Hofmann. Revisiting the categorical interpretation of dependent type theory. [7]. Simon Castellan. Dependent type theory as the initial category with families. [8]. Peter Dybjer. Internal Type Theory. -} import cat import fun import nat import list import bool import maybe {- The type checker based on Categories with Families (CwF) model. The contexts modeled as lists of initial objects of internal language. Here is example of two contexts and substitution between them. Ctx: Vec Exp 3 = [ A:U, B:A->U, Pi(A,B) ] Ctx: Vec Exp 5 = [ A:U, B:A->U, Pi(A,B), Sigma(A,B), A->A ] Subst: Vec Exp 2 = [ Sigma (Var 1) (Var 2), Pi (Var 1) (Var 1) ] -} data Exp = Star (_: nat) | Var (_: nat) | Pi (_ _: Exp) | Lam (_: Exp) | App (_ _: Exp) Ty: U = Exp Ctx: U = list Ty Subst: U = list Exp seq (start: nat): list Exp = cons (Var start) (seq (succ start)) mutual p: Subst = seq one q: Exp = Var zero ide: Subst = seq zero cmp: Subst -> Subst -> Subst = split nil -> \(ts: Subst) -> nil cons x xs -> \(ts: Subst) -> cons (sub ts x) (cmp xs ts) lift (ts: Subst): Subst = cons q (cmp ts p) unwrap: maybe Exp -> Exp = split { nothing -> q ; just x -> x } shift (t: Exp) (i: nat): Exp = sub (seq i) t isCo: Ctx -> bool = split nil -> true cons x xs -> and (isCo xs) (isTy xs x) isU (c:Ctx)(a b:Exp): Exp -> bool = split Star i -> (and (isTm c (Star i) a) (isTm (cons a c) (Star i) b)) Var i -> false Pi a b -> false Lam x -> false App a b -> false isPi (c:Ctx)(e:Exp): Exp -> bool = split Star i -> false Var i -> false Pi a b -> isTm (cons a c) b e Lam x -> false App a b -> false isTy (c:Ctx): Ty -> bool = split Star i -> true Var i -> isTm c (Star zero) (Var i) Pi a b -> and (isTy c a) (isTy (cons a c) b) Lam x -> isTm c (Star zero) (Lam x) App a b -> isTm c (Star zero) (App a b) isTm (c:Ctx)(e:Exp): Ty -> bool = split Star i -> false Var i -> false Pi a b -> isU c a b e Lam x -> isPi c x e App a b -> false app (s: Exp): Exp -> Exp = split Star i -> App (Star i) s Var i -> App (Var i) s Pi a b -> App (Pi a b) s Lam x -> sub (cons s ide) x App a b -> App (App a b) s sub (ts: Subst): Exp -> Exp = split Star i -> Star i Var i -> unwrap (nth Exp i ts) Pi a b -> Pi (sub ts a) (sub (lift ts) b) Lam x -> Lam (sub (lift ts) x) App s t -> app (sub ts t) (sub ts s) inferTy (c: Ctx): Exp -> maybe Ty = split Star i -> just (Star i) Var i -> just (shift (unwrap (nth Exp i c)) (succ i)) Pi a b -> just (Star one) -- implement Lam x -> just (Star zero) -- implement App s t -> just (Star zero) -- implement Fam: precategory = undefined isContext (C: precategory): U = undefined isTerminal (C: precategory): U = undefined isComprehension(C: precategory)(T: catfunctor C Fam): U = undefined CwF: U = (C: precategory) * (T: catfunctor C Fam) * (context: isContext C) * (terminal: isTerminal C) * (pullback: isComprehension C T) * unit