Throw out transport

diff --git a/Exp.cf b/Exp.cf
index 718647da36c408c81d88061091f4884f74fa4d8a..b0f94700081559ff0ab032fadcf78cc5f9419e07 100644 (file)
--- 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 734d5c945a1825b46a7512be0b85b095d154cf65..c6937374d7873c24831d5da9bc12de93e29c8ba7 100644 (file)
--- 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 20f37da892a832a34b3934df33fb41245b6c7fea..09e88848d6aafe0f958182ac2e4621c0db7de4de 100644 (file)
--- 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