Index of /~amp12/agda/internal-universes

[ICO]NameLast modifiedSizeDescription

[PARENTDIR]Parent Directory  -  
[TXT]Agda.Builtin.Equality.html2018-01-07 17:50 4.6K 
[TXT]Agda.Builtin.Unit.html2018-01-07 17:50 2.5K 
[TXT]Agda.Primitive.html2018-01-07 17:50 11K 
[TXT]Agda.css2018-01-07 17:50 1.2K 
[TXT]README.html2018-01-21 09:15 2.7K 
[TXT]agda-flat.prelude.html2018-01-20 09:34 12K 
[TXT]agda-flat.tiny.html2018-01-20 09:34 57K 
[TXT]agda.cchm.html2018-01-20 09:34 9.2K 
[TXT]agda.cctt.html2018-01-20 09:34 11K 
[TXT]agda.fibration.html2018-01-20 09:34 47K 
[TXT]agda.postulates.html2018-01-20 09:34 12K 
[TXT]agda.prelude.html2018-01-20 09:34 107K 
[DIR]code/2018-01-21 19:34 -  
[TXT]proposition-6-2.html2018-01-20 09:34 121K 
[TXT]theorem-3-1.html2018-01-20 09:34 55K 
[TXT]theorem-5-2.html2018-01-20 09:34 127K 

README
{- 
Proofs of Theorems 3.1, 5.2 and Proposition 6.2 from Dan Licata, Ian
Orton, Andrew M. Pitts and Bas Spitters, "Universes in Models of
Homotopy Type Theory".

The proofs are carried out in agda-flat, an extension of Agda by
Andrea Vezzosi which implements the local type theory described in the
paper.

Installation instructions for agda-flat are at
<http://www.cl.cam.ac.uk/~amp12/agda/internal-universes/agda-flat/install.txt>
-}

{-# OPTIONS --without-K #-}

module README where

-- Proof of Theorem 3.1
open import theorem-3-1

-- Proof of Theorem 5.2
open import theorem-5-2

-- Proof of Proposition 6.2
open import proposition-6-2