----------------------------------------------------------------------
-- This Agda code is designed to accompany the paper "Axioms for
-- Modelling Cubical Type Theory in a Topos". It is currently a work
-- in progress and still includes postulates/holes in certain places.
-- It also needs some tidying up and possibily reorganisation.
--
-- The idea for getting an impredicative universe of propositions Ω
-- comes from Martin Escardo, more details can be found at:
--
--          http://www.cs.bham.ac.uk/~mhe/impredicativity/          
----------------------------------------------------------------------

module root where

----------------------------------------------------------------------
-- Introducing basics (e.g. equality, products etc)
----------------------------------------------------------------------
open import prelude

----------------------------------------------------------------------
-- Impredicative universe of propositions and logic
----------------------------------------------------------------------
open import impredicative 

----------------------------------------------------------------------
-- The interval I
----------------------------------------------------------------------
open import interval

----------------------------------------------------------------------
-- Cofibrant propositions
----------------------------------------------------------------------
open import cof

----------------------------------------------------------------------
-- Fibrations
----------------------------------------------------------------------
open import fibrations

----------------------------------------------------------------------
-- Type formers: products, functions, path and identity types
----------------------------------------------------------------------
open import Data.products
open import Data.functions
open import Data.paths
open import Data.id

----------------------------------------------------------------------
-- Equivalences, quasi-inverss, contractiability, extendability etc
----------------------------------------------------------------------
open import equivs

----------------------------------------------------------------------
-- The glueing construction
----------------------------------------------------------------------
open import glueing

----------------------------------------------------------------------
-- Towards univalence 
----------------------------------------------------------------------
open import univalence.core
open import univalence.inverses


----------------------------------------------------------------------
-- Still to do (just a standard result from the HoTT book left):
--
--  - Explicitly defining qinv2equiv
--      Section: equivs
--      Current progress can be seen in: scratchpad.agda
--
----------------------------------------------------------------------