From: Anders <mortberg@chalmers.se>
Date: Thu, 18 Jun 2015 13:37:17 +0000 (+0200)
Subject: Reintroduce transport
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=ae85ca4c9118630219ebc3f76b20992b9d3f8463;p=cubicaltt.git

Reintroduce transport
---

diff --git a/Exp.cf b/Exp.cf
index 83d9a99..8d8c841 100644
--- 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 68fbb8e..46cdde1 100644
--- 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 705e3ff..0fa5b97 100644
--- 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