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-04-26 11:22 3.3K 
[TXT]agda-flat.prelude.html2018-01-20 09:34 12K 
[TXT]agda-flat.tiny.html2018-04-26 11:00 68K 
[TXT]agda.cchm.html2018-04-26 11:00 9.5K 
[TXT]agda.cctt.html2018-04-26 11:00 11K 
[TXT]agda.exp-path.html2018-04-26 11:00 14K 
[TXT]agda.fibration.html2018-04-26 11:00 67K 
[TXT]agda.postulates.html2018-01-20 09:34 12K 
[TXT]agda.prelude.html2018-01-20 09:34 107K 
[DIR]code/2018-04-26 11:22 -  
[TXT]proposition-6-2.html2018-04-26 11:00 126K 
[TXT]theorem-3-1.html2018-04-26 11:22 56K 
[TXT]theorem-5-2-relative.html2018-04-26 11:22 193K 
[TXT]theorem-5-2.html2018-04-26 11:22 178K 

Proofs of Theorems 3.1, 5.2 and Proposition 6.2 from 

Dan R. Licata, Ian Orton, Andrew M. Pitts and Bas Spitters, 
"Internal Universes in Models of Homotopy Type Theory"

in Proceedings of the 3rd International Conference on Formal
Structures for Computation and Deduction (FSCD 2018), Leibniz
International Proceedings in Informatics (LIPIcs), Vol. 108,
pp. 23:1-28:, 2018.

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

Installation instructions for agda-flat are in ~/code/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

-- A version  of Theorem 5.2 relativized to an arbitrary universe
open import theorem-5-2-relative

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