From: Anders Mörtberg Date: Fri, 21 Oct 2016 19:53:51 +0000 (-0400) Subject: doc X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a18af0399b00e41c580dd3137949bd018c06bdda;p=cubicaltt.git doc --- diff --git a/examples/README.md b/examples/README.md index 5b3a567..b5b282c 100644 --- a/examples/README.md +++ b/examples/README.md @@ -9,91 +9,92 @@ cubicaltt. The files contain: doing a proof for unary numbers by computation with binary numbers. -bool.ctt - Booleans. Proof that bool = bool by negation and various - other simple examples. +* **bool.ctt** - Booleans. Proof that bool = bool by negation and + various other simple examples. -category.ctt - Categories. Structure identity principle. Pullbacks. +* category.ctt - Categories. Structure identity principle. Pullbacks. -circle.ctt - The circle as a HIT. Computation of winding numbers. +* circle.ctt - The circle as a HIT. Computation of winding numbers. -collection.ctt - This file proves that the collection of all - sets is a groupoid. +* collection.ctt - This file proves that the collection of all sets is + a groupoid. -csystem.ctt - Definition of C-systems and universe - categories. Construction of a C-system from a universe - category. +* csystem.ctt - Definition of C-systems and universe + categories. Construction of a C-system from a universe + category. -demo.ctt - Demo of the system. +* demo.ctt - Demo of the system. -discor.ctt - or A B is discrete if A and B are. +* discor.ctt - or A B is discrete if A and B are. -equiv.ctt - Definition of equivalences and various results on these, - including the "graduate lemma". +* equiv.ctt - Definition of equivalences and various results on these, + including the "graduate lemma". -groupoidTrunc.ctt - The groupoid truncation as a HIT. +* groupoidTrunc.ctt - The groupoid truncation as a HIT. -hedberg.ctt - Hedbergs lemma: a type with decidable equality is a set. +* hedberg.ctt - Hedbergs lemma: a type with decidable equality is a + set. -helix.ctt - The loop space of the circle is equal to Z. +* helix.ctt - The loop space of the circle is equal to Z. -hnat.ctt - Non-standard natural numbers as a HIT without any path - constructor. +* hnat.ctt - Non-standard natural numbers as a HIT without any path + constructor. -hz.ctt - Z defined as a (impredicative set) quotient of nat * nat +* hz.ctt - Z defined as a (impredicative set) quotient of nat * nat -idtypes.ctt - Identity types (variation of Path types with - definitional equality for J). Including a proof - univalence expressed only using Id. +* idtypes.ctt - Identity types (variation of Path types with + definitional equality for J). Including a proof + univalence expressed only using Id. -injective.ctt - Two definitions of injectivity and proof that they are - equal. +* injective.ctt - Two definitions of injectivity and proof that they + are equal. -int.ctt - The integers as nat + nat with proof that suc is an iso - giving a non-trivial path from Z to Z. +* int.ctt - The integers as nat + nat with proof that suc is an iso + giving a non-trivial path from Z to Z. -integer.ctt - The integers as a HIT (identifying +0 with -0). Proof - that this representation is isomorphic to the one in - int.ctt +* integer.ctt - The integers as a HIT (identifying +0 with -0). Proof + that this representation is isomorphic to the one in + int.ctt -interval.ctt - The interval as a HIT. Proof of function extensionality - from it. +* interval.ctt - The interval as a HIT. Proof of function + extensionality from it. -list.ctt - Lists. Various basic lemmas in "cubical style". +* list.ctt - Lists. Various basic lemmas in "cubical style". -nat.ctt - Natural numbers. Various basic lemmas in "cubical style". +* nat.ctt - Natural numbers. Various basic lemmas in "cubical style". -ordinal.ctt - Ordinals. +* ordinal.ctt - Ordinals. -pi.ctt - Characterization of equality in pi types. +* pi.ctt - Characterization of equality in pi types. -prelude.ctt - The prelude. Definition of Path types and basic - operations on them (refl, mapOnPath, - funExt...). Definition of prop, set and groupoid. Some - basic data types (empty, unit, or, and). +* prelude.ctt - The prelude. Definition of Path types and basic + operations on them (refl, mapOnPath, + funExt...). Definition of prop, set and groupoid. Some + basic data types (empty, unit, or, and). -propTrunc.ctt - Propositional truncation as a HIT. (WARNING: not - working correctly) +* propTrunc.ctt - Propositional truncation as a HIT. (WARNING: not + working correctly) -retract.ctt - Definition of retract and section. +* retract.ctt - Definition of retract and section. -setquot.ctt - Formalization of impredicative set quotients á la - Voevodsky. +* setquot.ctt - Formalization of impredicative set quotients á la + Voevodsky. -sigma.ctt - Various results about sigma types. +* sigma.ctt - Various results about sigma types. -subset.ctt - Two definitions of a subset and a proof that they are - equal. +* subset.ctt - Two definitions of a subset and a proof that they are + equal. -summary.ctt - Summary of where to find the results and examples from - the cubical type theory paper. +* summary.ctt - Summary of where to find the results and examples from + the cubical type theory paper. -susp.ctt - Suspension. Definition of the circle as the suspension of - bool and a proof that this is equal to the standard HIT - representation of the circle. +* susp.ctt - Suspension. Definition of the circle as the suspension of + bool and a proof that this is equal to the standard HIT + representation of the circle. -torsor.ctt - Torsors. Proof that S1 is equal to BZ, the classifying - space of Z. +* torsor.ctt - Torsors. Proof that S1 is equal to BZ, the classifying + space of Z. -torus.ctt - Proof that Torus = S1 * S1. +* torus.ctt - Proof that Torus = S1 * S1. -univalence.ctt - Proofs of the univalence axiom. +* univalence.ctt - Proofs of the univalence axiom.