From: Anders Mörtberg Date: Fri, 21 Oct 2016 19:57:42 +0000 (-0400) Subject: doc X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=b3ec37c1c740f101551656538920853e5df48a39;p=cubicaltt.git doc --- diff --git a/examples/README.md b/examples/README.md index b5b282c..9c110d8 100644 --- a/examples/README.md +++ b/examples/README.md @@ -4,97 +4,101 @@ Cubical Type Theory: examples This folder contains a lot of examples implemented using cubicaltt. The files contain: -* *binnat.ctt* - Binary natural numbers and isomorphism to unary - numbers. Example of data and program refinement by - doing a proof for unary numbers by computation with - binary numbers. +* **binnat.ctt** - Binary natural numbers and isomorphism to unary + numbers. Example of data and program refinement by + 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. -* 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** - Hedberg's 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 + isomorphism 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.