From 9c8123c53fdabcf66d3db7feb4ab192f4b45ce7d Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 20 Oct 2016 17:47:04 -0400 Subject: [PATCH] a lot of comments --- examples/discor.ctt | 1 + examples/groupoidTrunc.ctt | 1 + examples/hedberg.ctt | 1 + examples/helix.ctt | 1 + examples/hnat.ctt | 1 + examples/idtypes.ctt | 2 ++ examples/int.ctt | 2 ++ 7 files changed, 9 insertions(+) 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) -- 2.34.1