----------------------------------------------------------------------
-- 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/          
----------------------------------------------------------------------

{-# OPTIONS --rewriting #-}
module cof where 

open import prelude
open import impredicative
open import interval

infixr 4 _∨_
infix  5 _↗_
infix  6 _∙_

----------------------------------------------------------------------
-- Cofibrant propositions
----------------------------------------------------------------------
postulate
 cof   : Ω  Ω
 cofO  : (i : Int)  prf (cof (i  O))
 cofI  : (i : Int)  prf (cof (i  I))
 cofor : (P Q : Ω)  prf (cof P  cof Q  cof(P or Q))
 cof&  : (P Q : Ω)  prf (cof P  (P  cof Q)  cof(P & Q)) 
 
Cof : Set
Cof =  P  Ω  cof P 

[_] : Cof  Set
[ φ ] = prf (fst φ)

cofFalse : Cof
fst cofFalse = 
snd cofFalse = subst (prf  cof) (propext O≠I ∅-elim) (cofI O)

cofTrue : Cof
fst cofTrue = 
snd cofTrue = subst (prf  cof) (propext  _  tt)  _  refl)) (cofO O)

_≈O : (i : Int)  Cof
fst (i ≈O) = i  O
snd (i ≈O) = cofO i

_≈I : (i : Int)  Cof
fst (i ≈I) = i  I
snd (i ≈I) = cofI i

_≈OI_ : (i : Int)(e : OI)  Cof
fst (i ≈OI e) = i   e 
snd (i ≈OI e) with e
... | O' = cofO i
... | I' = cofI i

_∨_ : Cof  Cof  Cof
(P , u)  (Q , v) = ((P or Q) , cofor P Q u v)

cofEq : {P Q : Cof}  fst P  fst Q  P  Q
cofEq {P , cofP} {.P , cofP'} refl = cong (_,_ P) (equ (cof P) cofP cofP' )

----------------------------------------------------------------------
-- Cofibrant-partial function classifier
----------------------------------------------------------------------
 : Set  Set
 A = Σ φ  Cof , ([ φ ]  A)

_↗_ : {A : Set}   A  A  Ω
(φ , f)  x = All u  [ φ ] , f u  x

----------------------------------------------------------------------
-- Dependently typed paths
----------------------------------------------------------------------
Π : (Int  Set)  Set
Π A = (i : Int)  A i

Π′ :
  {A B : Int  Set}
   ---------------------------------
  ((i : Int)  A i  B i)  Π A  Π B
Π′ F p i = F i (p i)

_∙_ :
  {A : Int  Set}
   -------------------------
  (Π A)  (i : Int)  (A i)
(φ , f)  i = (φ , λ u  f u i)