From: Anders Date: Fri, 27 Mar 2015 16:53:07 +0000 (+0100) Subject: Examples X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d130265253b40a7c15a63eca74fc83e5c752c215;p=cubicaltt.git Examples --- diff --git a/examples/integer.ctt b/examples/integer.ctt index 2f08c7b..e8b6ba9 100644 --- a/examples/integer.ctt +++ b/examples/integer.ctt @@ -37,3 +37,6 @@ predsucZ : (n : Z) -> Id Z (predZ (sucZ n)) n = split suc n -> refl Z (negZ (suc n)) sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ + +sucIdZ2 : Id U Z Z = compId U Z Z Z sucIdZ sucIdZ +test : Z = predZ (transport sucIdZ2 zeroZ) \ No newline at end of file diff --git a/examples/prelude.ctt b/examples/prelude.ctt index c3bd9f6..1566339 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -49,11 +49,12 @@ isoId (A B : U) (f : A -> B) (g : B -> A) glue B [ (i = 0) -> (A,f,g,s,t) ] -- u --- a0 ----- a1 --- | | --- r0 | | r1 --- | | --- b0 ----- b1 +-- a0 -----> a1 +-- | | +-- r0 | | r1 +-- | | +-- V V +-- b0 -----> b1 -- v Square (A : U) (a0 a1 : A) (u : Id A a0 a1)