Skip to content
Branch: master
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
Makefile
README.md Remove one more instance of "graduate lemma" Sep 7, 2017
algstruct.ctt Added definitions of algebraic structures in algstruct.ctt, a constru… Jan 2, 2017
binnat.ctt A small simplification on binnat.ctt Sep 17, 2017
bool.ctt
brunerie.ctt copy over brunerie.ctt from hcomptrans branch. some computations are … Apr 19, 2018
category.ctt rename gradLemma to isoToEquiv Aug 11, 2017
circle.ctt add 5th winding number Apr 19, 2018
collection.ctt rename Id to Path Jul 7, 2016
constcubes.ctt
control.ctt plug functor to recursion schemes Nov 6, 2017
csystem.ctt
demo.ctt
discor.ctt a lot of comments Oct 20, 2016
equiv.ctt Clean up isoToEquiv proof with Anders. Apr 9, 2018
grothendieck.ctt Added definitions of algebraic structures in algstruct.ctt, a constru… Jan 2, 2017
groupoidTrunc.ctt a lot of comments Oct 20, 2016
hedberg.ctt
helix.ctt comments Oct 21, 2016
hnat.ctt
hz.ctt
idtypes.ctt
injective.ctt comments Oct 21, 2016
int.ctt
integer.ctt
interval.ctt
lambek.ctt plug functor to recursion schemes Nov 6, 2017
list.ctt comments Oct 21, 2016
nat.ctt
opposite.ctt swap direction of equality to match order in comment Dec 25, 2016
ordinal.ctt comments Oct 21, 2016
pi.ctt
pointedMaps.ctt
prelude.ctt add an alternative proof of J Feb 23, 2018
propTrunc.ctt
retract.ctt
setquot.ctt
sigma.ctt comments Oct 21, 2016
subset.ctt rename gradLemma to isoToEquiv Aug 11, 2017
summary.ctt
susp.ctt comments Oct 21, 2016
torsor.ctt
torus.ctt
univalence.ctt fix indentation in univalenceAlt Apr 25, 2018
univprop.ctt Uncommented slow function. Jan 3, 2017

README.md

Cubical Type Theory: examples

This folder contains a lot of examples implemented using cubicaltt. The files contain:

  • algstruct.ctt - Defines some standard algebraic structures and properties.

  • 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.

  • 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.

  • csystem.ctt - Definition of C-systems and universe categories. Construction of a C-system from a universe category.

  • demo.ctt - Demo of the system.

  • discor.ctt - or A B is discrete if A and B are.

  • equiv.ctt - Definition of equivalences and various results on these, including "isoToEquiv".

  • grothendieck.ctt - This file contains a constuction of the Grothendieck group and a proof of its universal property.

  • groupoidTrunc.ctt - The groupoid truncation as a HIT.

  • 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.

  • 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

  • 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.

  • 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

  • interval.ctt - The interval as a HIT. Proof of function extensionality from it.

  • list.ctt - Lists. Various basic lemmas in "cubical style".

  • nat.ctt - Natural numbers. Various basic lemmas in "cubical style".

  • ordinal.ctt - Ordinals.

  • opposite.ctt - Opposite category and a proof that C^op^op = C definitionally.

  • 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).

  • propTrunc.ctt - Propositional truncation as a HIT. (WARNING: not working correctly)

  • retract.ctt - Definition of retract and section.

  • setquot.ctt - Formalization of impredicative set quotients á la Voevodsky.

  • sigma.ctt - Various results about sigma types.

  • 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.

  • 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.

  • torus.ctt - Proof that Torus = S1 * S1.

  • univalence.ctt - Proofs of the univalence axiom.

  • univprop.ctt - Defines natural transformations, universal arrows, and adjunctions. Also contains a proof that a family of universal arrows gives rise to an adjunction. This is then used to prove that the Grothendieck homomorphism is left adjoint to the forgetful functor.

You can’t perform that action at this time.