Skip to content
forked from HoTT/HoTT-Agda

Development of homotopy type theory in Agda

Notifications You must be signed in to change notification settings

sattlerc/HoTT-Agda

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 

Repository files navigation

This code base contains the accompanying code to the article

  "Higher Homotopies in a Hierarchy of Univalent Universes"

and all of its dependencies. It has been verified to typecheck
with Agda release 2.4.2.


Contents
========

The subdirectory 'Universe' contains our Agda developments implementing
the contents of the above article. The code is extensively documented,
we hope it to be self-explanatory. The reader is invited to start with
the entry point 'Universe/index.agda', which establishes correspondence
of sections of the article with individual modules and lemmata and theorems
of the article and definitions inside the modules.

The subdirectory 'lib' contains a slightly modified portion of
the HoTT community's Agda library. For readability and verifiability,
we decided to include only those parts that are required to typecheck
the actual code implementing the development of the article.

The only notable uses of a postulate occur in 'lib/Univalence' for
the Univalence Axiom and in 'lib/types/Truncation' to emulate a higher
inductive type, the n-truncation, in Agda using Dan Licata's "trick"
of a partially private definition (note that Agda does not currently
support higher inductive types natively).
This file is important at the very end of our development when we
want to compare our "internal" notions of connectedness to the
standard one derived from truncations in the theory.


How to typecheck
================

The Agda API for universe levels recently changed, introducing breakage for
code written for versions below 2.4. We decided to port our code to version 2.4
because of the simultaneous introduction of the semantically justified
implementation of the --without-K flag by Jesper Cockx.

The code has specifically been verified to typecheck under Agda 2.4.2.
Regressions related to Agda Issue 1214 cause Agda 2.4.0.* to fail
termination checking.

The entry point 'Universe/index.agda' imports all of the files of our
developments. It is hence enough to run 'agda Universe/index.agda'
within the working directory this README file is residing in. The flag
"--without-K" required to make Agda compatible with homotopy type theory
is given in the header of each individual file, so it is not necessary
to pass as a command line parameter. Execution of the above command should
result in a final output line "Finished Universe.index" with no errors,
unresolved meta-variables, or outstanding termination checks.


Correspondence to the article text
==================================

Formalization of proofs necessitates strict modularity if one wants to avoid
the hidden complexities implicit in formalizing hand-written arguments.
This introduces a software engineering perspective into the enterprise.
For this reason, the organization of the code is slightly different from
that of the article, in which e.g. one may freely allude to arguments from proofs
of previous lemmata without giving these facts an external representation.

The file 'Universe/index.agda' establishes a basic correspondence of sections
of the article with modules of the codebase. In addition to this overview,
it also mentions which definitions, lemmata, corollaries, and theorems
may be found in which file. Individual such references are additionally
given at the corresponding places inside each module.

Let us elaborate on a few differences between the type theory implemented
by Agda and HoTT.

The first difference concerns the presence of eta-rules for record types,
i.e. for the Sigma-type-former within Agda. While this enables shorter code
on a number of occasions, we believe this difference to be minor and not
relevant to this formalization. 

Secondly, Agda implements universe polymorphism by giving the user access
to an internal type of universe indices, e.g. enabling internal inductive
arguments over the universe hierarchy. No such thing is possible in HoTT.
We exploit this feature to give a polymorphic proof of our main theorems,
which in the article are always indexed over some external natural constant n.
To produce a 'proper' type derivation in HoTT, one would recursively
instantiate the code for each universe in the hierarchy, eliminating the
internal universe index variables in the process.

Relatedly, universes in Agda are not cumulative (and ordering relations
on universe indices are not specifiable), in contrast to the theory of our
reference, the HoTT book. This introduces a number of technical deviations,
which are properly explained at the appropriate places, most notably
the first one, explaining the explicit usage of equivalences
instead of equalities for some aspects of section 5:
  * Universe/Hierachy.agda, line 8
  * Universe/Trunc/Basic.agda, line 40
  * Universe/Trunc/Universal.agda, line 80
  * Universe/Trunc/Connection.agda, line 36

A real difference between the development of the article and the codebase
is the choice of proving a slightly weaker variant of Lemma 5.8
that nevertheless turns out to be sufficient.
Instead of giving an explicit description of a non-trivial inhabitant
of a certain loop space, we merely prove it non-contractible.
It is certainly possible to follow the exact strategy as the article here,
but we have found that this makes for a particularly present formal
induction step, with no other change further on.

Finally, a minor difference is the definition of the fibered version of
the loop space operator, where we choose an equivalent representation.
This is explained in situ:
  * Universe/Utility/Pointed.agda, line 222


Copyright and Licensing
=======================

The HoTT community's Agda library, residing in the 'lib' subdirectory, is free
software distributed under the terms of the MIT License (see 'lib/LICENSE').

Our own development, residing in the 'Universe' subdirectory, is free software
distributed under the terms of the MIT License (see 'Universe/LICENSE').

About

Development of homotopy type theory in Agda

Resources

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Agda 100.0%