Reintroduce transport

diff --git a/Exp.cf b/Exp.cf
index 83d9a9951f492586457622134d124a5911160939..8d8c8410d39687850cc2dc2f2f6009754484b5ca 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -32,6 +32,7 @@ AppFormula.   Exp2 ::= Exp2 "@" Formula ;
 App.          Exp2 ::= Exp2 Exp3 ;
 IdP.          Exp3 ::= "IdP" Exp4 Exp4 Exp4 ;
 Comp.         Exp3 ::= "comp" Exp4 Exp4 System ;
+Trans.        Exp3 ::= "transport" Exp4 Exp4 ;
 Fill.         Exp3 ::= "fill" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "glue" Exp4 System ;
 GlueElem.     Exp3 ::= "glueElem" Exp4 System ;

diff --git a/Resolver.hs b/Resolver.hs
index 68fbb8e83b79bc096c77403803e651358a7d025a..46cdde1ea4840c528e1eaa8c67ad848790fb05c7 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -202,9 +202,10 @@ resolveExp e = case e of
         CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs
                               <*> mapM resolveFormula phis
       _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi
-  IdP x y z     -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
+  IdP a u v     -> CTT.IdP <$> resolveExp a <*> resolveExp u <*> resolveExp v
   Comp u v ts   -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
   Fill u v ts   -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+  Trans u v     -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> pure Map.empty
   Glue u ts     -> CTT.Glue <$> resolveExp u <*> resolveSystem ts
   GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
   -- GlueLine phi psi u ->

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 705e3ff3d91b40f4eaf3772539dfa7fcb1f352d3..0fa5b97c0fdf77ac1e2b91ad6e76e83e5fa06024 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -15,6 +15,7 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
        (p : (x : A) -> Id (B x) (f x) (g x)) :
        Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i
 
+-- Transport can be defined using comp
 trans (A B : U) (p : Id U A B) (a : A) : B = comp p a []
 
 -- subst can be defined using trans:
@@ -22,7 +23,7 @@ substTrans (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
   trans (P a) (P b) (mapOnPath A U P a b p) e
 
 subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
-  comp (mapOnPath A U P a b p) e []
+  transport (mapOnPath A U P a b p) e
 
 -- substRefl (A : U) (P : A -> U) (a : A) (e : P a) :
 --   Id (P a) (subst A P a a (refl A a) e) e = refl (P a) e