Skip to content

Latest commit

 

History

History
40 lines (33 loc) · 1.88 KB

README.md

File metadata and controls

40 lines (33 loc) · 1.88 KB
Raw

Agda code for "For Induction-Induction, Induction is Enough"

Installation

This folder has been tested with Agda 2.6.0.1. Newer Agda versions likely work as well. An Agda standard library is also needed. Instructions how to set up the standard library can be found here, the library itself can be downloaded from here.

Formalization

We construct a morphism from the syntax of the type theory of signatures to an arbitrary model, and prove its uniqueness.

Files in the order of dependency with a short description:

  1. EqLib.agda: definitions and lemmas taking from the HoTT library (removing the univalence axiom).
  2. Lib.agda: some useful lemmas, some of them requiring UIP
  3. Syntax.agda: syntax of the theory of signatures
  4. Model.agda: definition of models
  5. SyntaxIsModel.agda: syntax as a model
  6. ModelRew.agda: postulated model with rewrite rules
  7. Relation.agda: definition of the relation between the syntax and the postulated model
  8. RelationWeakening.agda: stability of the relation under weakening
  9. RelationSubstitution.agda: stability of the relation under substitution
  10. RelationInhabit.agda: construction of a related semantic counterpart for each part of the syntax
  11. ModelMorphism.agda: definition of model morphisms
  12. ModelMorphismRew.agda: postulated model morphism from the syntax to the postulated model
  13. SyntaxIsInitial.agda: construction of a morphism from the syntax to the postulated model, and proof that the postulated morphism is pointwise equal to it.