From: Simon Huber <hubsim@gmail.com>
Date: Fri, 5 Jun 2015 14:18:22 +0000 (+0200)
Subject: Throw out transport
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9affc9f4029e54da4108550b71d72b12977d8074;p=cubicaltt.git

Throw out transport
---

diff --git a/Exp.cf b/Exp.cf
index 718647d..b0f9470 100644
--- a/Exp.cf
+++ b/Exp.cf
@@ -31,7 +31,6 @@ Sigma.        Exp1 ::= [PTele] "*" Exp1 ;
 AppFormula.   Exp2 ::= Exp2 "@" Formula ;
 App.          Exp2 ::= Exp2 Exp3 ;
 IdP.          Exp3 ::= "IdP" Exp4 Exp4 Exp4 ;
-Trans.        Exp3 ::= "transport" Exp4 Exp4 ;
 Comp.         Exp3 ::= "comp" Exp4 Exp4 System ;
 Fill.         Exp3 ::= "fill" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "glue" Exp4 System ;
diff --git a/Resolver.hs b/Resolver.hs
index 734d5c9..c693737 100644
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -202,7 +202,6 @@ resolveExp e = case e of
         CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs
                               <*> mapM resolveFormula phis
       _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi
-  Trans x y   -> CTT.Comp <$> resolveExp x <*> resolveExp y <*> pure Map.empty
   IdP x y z   -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
   Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
   Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 20f37da..09e8884 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -15,14 +15,14 @@ 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
 
-trans (A B : U) (p : Id U A B) (a : A) : B = genComp p a []
+trans (A B : U) (p : Id U A B) (a : A) : B = comp p a []
 
 -- subst can be defined using trans:
 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 =
-  transport (mapOnPath A U P a b p) e
+  comp (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