From: Simon Huber 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 = \(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