From: Anders Mörtberg Date: Thu, 20 Oct 2016 21:47:04 +0000 (-0400) Subject: a lot of comments X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9c8123c53fdabcf66d3db7feb4ab192f4b45ce7d;p=cubicaltt.git a lot of comments --- diff --git a/examples/discor.ctt b/examples/discor.ctt index 5b39f91..068a46d 100644 --- a/examples/discor.ctt +++ b/examples/discor.ctt @@ -1,3 +1,4 @@ +-- or A B is discrete if A and B are module discor where import prelude diff --git a/examples/groupoidTrunc.ctt b/examples/groupoidTrunc.ctt index e3149bf..827e4dd 100644 --- a/examples/groupoidTrunc.ctt +++ b/examples/groupoidTrunc.ctt @@ -1,3 +1,4 @@ +-- The groupoid truncation as a HIT module groupoidTrunc where import equiv diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt index 9a57b92..e438e62 100644 --- a/examples/hedberg.ctt +++ b/examples/hedberg.ctt @@ -1,3 +1,4 @@ +-- Hedbergs lemma: a type with decidable equality is a set module hedberg where import prelude diff --git a/examples/helix.ctt b/examples/helix.ctt index 5e0e4be..31b3875 100644 --- a/examples/helix.ctt +++ b/examples/helix.ctt @@ -1,3 +1,4 @@ +-- The loop space of the circle is equal to Z module helix where import circle diff --git a/examples/hnat.ctt b/examples/hnat.ctt index 723de51..2834ed5 100644 --- a/examples/hnat.ctt +++ b/examples/hnat.ctt @@ -1,3 +1,4 @@ +-- Non-standard natural numbers as a HIT without any path constructor module hnat where import nat diff --git a/examples/idtypes.ctt b/examples/idtypes.ctt index d0705dd..d2bb65e 100644 --- a/examples/idtypes.ctt +++ b/examples/idtypes.ctt @@ -1,3 +1,5 @@ +-- Identity types (variation of Path types with definitional equality +-- for J). Including a proof univalence expressed only using Id. module idtypes where import sigma diff --git a/examples/int.ctt b/examples/int.ctt index 1bd6891..391db88 100644 --- a/examples/int.ctt +++ b/examples/int.ctt @@ -61,4 +61,6 @@ sucPathZ : Path U Z Z = isoPath Z Z sucZ predZ sucpredZ predsucZ testOneZ : Z = transport sucPathZ zeroZ testNOneZ : Z = transport ( sucPathZ @ - i) zeroZ + + ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)