----------------------------------------------------------------------
-- 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 Data.id where

open import prelude
open import impredicative
open import interval
open import cof
open import fibrations
open import Data.paths
open import Data.products

----------------------------------------------------------------------
-- Id types
----------------------------------------------------------------------
Id : {Γ : Set}(A : Γ  Set)  Σ x  Γ , A x × A x  Set
Id {Γ} A = Σ' (Path A) Prf where
  Prf : Σ (Σ Γ  x  A x × A x)) (Path A)  Set
  Prf ((x , (a , a')) , p) =  φ  Cof  fst φ  (All i  Int , fst p i  a) 

IdExt :
  {Γ : Set}
  {A : Γ  Set}
  {x : Γ}
  {a a' : A x}
  {id id' : Id A (x , (a , a'))}
   ------------
  (fst (fst id)  fst (fst id'))  (fst (fst (snd id)))  fst (fst (snd id'))  id  id'
IdExt {Γ} {A} {x} {a} {a'} {(p , u)} refl refl =
  let pathEq = (PathExt refl) in Σext pathEq (PrfExt pathEq refl) where
    Prf : Σ (Σ Γ  x  A x × A x)) (Path A)  Set
    Prf ((x , (a , a')) , p) =  φ  Cof  fst φ  (All i  Int , fst p i  a) 
    PrfExt : {p p' : a ~ a'}(eq : p  p'){u : Prf ((x , (a , a')) , p)}{v : Prf ((x , (a , a')) , p')}
       fst (fst u)  fst (fst v)  subst ((λ p  Prf ((x , a , a') , p))) eq u  v
    PrfExt {p} {_} {refl} {((φ , _) , _)} refl =
      Σext (Σext refl (eq (cof φ))) (eq (φ  all Int  i  fst p i  a)))

existsCof : (φ : Cof)(f : [ φ ]   Ω)  ((u : [ φ ])  prf (cof (f u)))  prf (cof (exists [ φ ] f))
existsCof φ f fCof = subst (prf  cof) eqProps' cofφ&exists where
  imp : prf (fst φ  cof (exists [ φ ] f))
  imp u = subst (prf  cof) eqProps (fCof u) where
    eqProps : f u  exists [ φ ] f
    eqProps = propext  v   (u , v) )  v  ∥∥-elim body  _ _  eq (f u)) v) where
      body : Σ (prf (fst φ))  v₁  prf (f v₁))  prf (f u)
      body (u' , fu') = subst (prf  f) (eq (fst φ)) fu'
      
  eqProps' : (fst φ & exists [ φ ] f)  exists [ φ ] f
  eqProps' = propext snd  u  (∥∥-rec (fst φ) fst u , u))
  
  cofφ&exists : prf (cof (fst φ & exists [ φ ] f))
  cofφ&exists = cof& (fst φ) (exists [ φ ] f) (snd φ) imp
  

FibId : {Γ : Set}{A : Γ  Set}  Fib A  Fib (Id A)
FibId {Γ} {A} α = FibΣ {B = Prf} (FibPath {A = A} α) β where
  Γ' : Set
  Γ' = Σ (Σ Γ  x  A x × A x)) (Path A)
  
  Prf : Γ'  Set
  Prf ((x , (a , a')) , p) =  φ  Cof  fst φ  (All i  Int , fst p i  a) 
  
  prfExt : {x : Γ}{a a' : A x}{p : a ~ a'}{pr pr' : Prf ((x , (a , a')) , p)}  fst (fst pr)  fst (fst pr')  pr  pr'
  prfExt {x} {a} {a'} {p} {((φ , _) , _)} {_} refl = Σext (Σext refl (eq (cof φ))) (eq (φ  (All i  Int , fst p i  a)))
  
  β : Fib Prf
  β e p φ f φ' = ψ where
    ψ :  ψ  (Prf (p  ! e ))  (φ , f)   ! e   ψ 
    fst (fst ψ) = (exists [ φ ] fI , existsCof φ fI  u  snd (fst (f u  ! e )))) where
      fI : [ φ ]  Ω
      fI u = fst (fst (f u  ! e ))
    snd (fst ψ) ex i = ex goal proof where
      goal : Ω
      goal = fst (snd (p  ! e )) i  fst (snd (fst (p  ! e )))
      proof : Σ [ φ ]  u  prf (fst (fst (f u  ! e ))))  prf (goal)
      proof (u , v) = snd (f u  ! e ) v i
    snd ψ u = prfExt {p = snd (p  ! e )} (propext  v   u , v ) backwards) where
      backwards : prf (fst (fst (fst ψ)))  prf (fst (fst (f u  ! e )))
      backwards v = ∥∥-rec (fst (fst (f u  ! e )))  pair  subst  v  [ fst (f v  ! e ) ]) (eq (fst φ )) (snd pair)) v


reflId : {Γ : Set}(A : Γ  Set){x : Γ}(a : A x)  Id A (x , (a , a))
reflId {Γ} A {x} a = (reflPath {A = A} a , (cofTrue ,  tt i  refl)))


private
 triple :
  {Γ : Set}
  (A : Γ  Set)
  {x : Γ}
  {a : A x}
  (B : Σ a'  (A x) , Id A (x , (a , a'))  Set)
  (a' : A x)
  (e : Id A (x , (a , a')))
  (b : B (a' , e))
   Σ a'  (A x) , Σ e  (Id A (x , (a , a'))) , B (a' , e)
 triple _ _ a' e b = (a' , e , b)

private
 tripleExt :
  {Γ : Set}
  (A : Γ  Set)
  {x : Γ}
  {a₀ : A x}
  (B : Σ a'  (A x) , Id A (x , (a₀ , a'))  Set)
  {a a' : A x}
  {e  : Id A (x , (a₀ , a))}
  {e' : Id A (x , (a₀ , a'))}
  {b  : B (a , e)}
  {b' : B (a' , e')}
  (_ : a  a')
  (_ : fst (fst e)  fst (fst e'))
  (_ : fst (fst (snd e))   fst (fst (snd e')))
  (eqB : (p : (a , e)  (a' , e'))  subst B p b  b')
  -----------------
   triple A B a e b  triple A B a' e' b'
 tripleExt A {x} {a₀} B {a} .{a} {e} {e'} {b} {b'} refl p q eqB =
   Σext refl (Σext (IdExt {A = A} p q) (trans step₂ step₁)) where
     substLemma : (e' : Id A (x , (a₀ , a)))(p : e  e')
        subst  e  B (a , e)) p b  subst B (Σext refl p) b
     substLemma _ refl = refl
     step₁ : subst  e₁  B (a , e₁)) (IdExt {A = A} p q) b  subst B (Σext refl (IdExt {A = A} p q)) b
     step₁ = substLemma e' (IdExt {A = A} p q)
     step₂ : subst B (Σext refl (IdExt {A = A} p q)) b  b'
     step₂ = eqB ((Σext refl (IdExt {A = A} p q)))

private
 Jinternal :
  {Γ : Set}
  {A : Γ  Set}
  {x : Γ}
  {a : A x}
  (B : Σ a'  (A x) , Id A (x , (a , a'))  Set)
  (β : Fib B)
  (a' : A x)
  (e : Id A (x , (a , a')))
   -------------
  (b : B (a , reflId A a))   b'  B(a' , e)  fst (fst (snd e))  (triple A B a' e b')  (triple A B a (reflId A a) b) 
 Jinternal {Γ} {A} {x} {a} B β a' (p , φ , pRefl) b = (bI' , atRefl) where
  q : (i : Int)  Id A (x , (a , fst p i))
  fst (fst (q i)) j = fst p (min i j)
  fst (snd (fst (q i))) = fst (snd p)
  snd (snd (fst (q i))) = refl
  fst (snd (q i)) = φ  i ≈O
  snd (snd (q i)) u j = or-elim-eq  _  fst p (min i j)) a  {l}  pRefl l (min i j))  {r}  right i r) u where
    right : (i : Int)  (i  O)  fst p (min i j)  a
    right .O refl = fst (snd p)

  substEq : {x : Γ}{a a' : A x}(equal : a  a')(goal : Id A (x , (a , a')))
     fst (fst (reflId A a))  fst (fst goal)
     [ fst (snd goal) ]
     subst  a''  Id A (x , a , a'')) equal (reflId A a)  goal
  substEq refl goal equal u = IdExt {A = A} equal (propext  _  u)  _  tt))

  coePath : (i : Int)(equal : (j : Int)  a  fst p (min i j))(u : [ φ  i ≈O ])
     (a , reflId A a)  (fst p i , q i)
  coePath i equal u = Σext (equal I) (substEq (equal I) (q i) (funext equal) u)

  coeB : (i : Int)(equal : (j : Int)  a  fst p (min i j))(u : [ φ  i ≈O ])
     B (a , reflId A a)  B (fst p i , q i)
  coeB i equal u b = subst B (coePath i equal u) b
    
  f : [ φ ]  Π (B   i  fst p i , q i))
  f u i = coeB i  j  symm (pRefl u (min i j)))  inl u  b
    
  b' : B (fst p O , q O)
  b' = coeB O  _  a≡pO)  inr refl  b where
    a≡pO : a  fst p O
    a≡pO = symm (fst (snd p))
    
  congSubst : {A : Set}{a a' : A}(B : A  Set)(p q : a  a')(b b' : B a)  b  b'  subst B p b  subst B q b'
  congSubst B refl refl b .b refl = refl

  extends : prf ((φ , f)  O  b')
  extends u = congSubst B eq₁ eq₂ b b refl where
    eq₁ : (a , reflId A a)  (fst p O , q O)
    eq₁ = coePath O  j  symm (pRefl u O))  inl u 
    eq₂ : (a , reflId A a)  (fst p O , q O)
    eq₂ = coePath O  _  symm (fst (snd p)))  inr refl 

  bI : B (fst p I , q I)
  bI = fst (β O'  i  (fst p i , q i)) φ f (b' , extends))

  pI≡a : fst p I  a'
  pI≡a = snd (snd p)

  substEq' : {a' a'' : A x}(equal : a'  a'')(id : Id A (x , (a , a')))(id' : Id A (x , (a , a'')))
     fst (fst id)  fst (fst id')
     fst (fst (snd id))  fst (fst (snd id'))
     subst  a''  Id A (x , a , a'')) equal id  id'
  substEq' refl id id' eq₁ eq₂  = IdExt {A = A} eq₁ eq₂

  qI≡p : subst  a'  Id A (x , (a , a'))) pI≡a (q I)  (p , φ , pRefl)
  qI≡p = substEq' pI≡a (q I) (p , φ , pRefl) refl eqProps where
    eqProps : fst (φ  I ≈O)  fst φ
    eqProps = propext
       u  u (fst φ) (λ{ (inl u)  u ; (inr I≡O)  ∅-elim (O≠I (symm I≡O)) }))
       u   inl u )

  bI' : B (a' , p , φ , pRefl)
  bI' = subst B (Σext pI≡a qI≡p) bI

  fI≡bI : (u : [ φ ])  f u I  bI
  fI≡bI u = snd (β O'  i  (fst p i , q i)) φ f (b' , extends)) u 
    
  substSwap : {A : Set}{a a' : A}(B : A  Set)(p : a  a')(q : a'  a)(b : B a)(b' : B a')  subst B p b  b'  b  subst B q b'
  substSwap B refl refl b .b refl = refl
    
  substTrans : {A : Set}{a a' a'' : A}(B : A  Set)(p : a  a')(q : a'  a'')(b : B a)  subst B (trans q p) b  subst B q (subst B p b)
  substTrans B refl refl b = refl

  b≡bI' : (u : [ φ ])(equal : (a' , p , φ , pRefl)  (a , reflId A a))  subst B equal bI'  b
  b≡bI' u equal = let rr = symm (trans sbI≡sbI' b≡sbI) in rr where
    b≡sbI : b  subst B (trans equal (Σext pI≡a qI≡p)) bI
    b≡sbI = substSwap B (coePath I  j  symm (pRefl u j))  inl u ) (trans equal (Σext pI≡a qI≡p)) b bI (fI≡bI u)
    sbI≡sbI' : subst B (trans equal (Σext pI≡a qI≡p)) bI  subst B equal bI'
    sbI≡sbI' = substTrans B (Σext pI≡a qI≡p) equal bI

  atRefl : (u : [ φ ])  (triple A B a' (p , φ , pRefl) bI')  (triple A B a (reflId A a) b)
  atRefl u = tripleExt A B (trans (pRefl u I) (symm (snd (snd p)))) (funext (pRefl u)) (propext  _  tt)  _  u)) (b≡bI' u)


J :
  {Γ : Set}
  {A : Γ  Set}
  {x : Γ}
  {a : A x}
  (B : Σ a'  (A x) , Id A (x , (a , a'))  Set)
  (β : Fib B)
  (a' : A x)
  (e : Id A (x , (a , a')))
   -------------
  B (a , reflId A a)  B(a' , e)
J {Γ} {A} {x} {a} B β a' e b = fst (Jinternal {A = A} B β a' e b)


Jrefl :
  {Γ : Set}
  {A : Γ  Set}
  {x : Γ}
  {a : A x}
  (B : Σ a'  (A x) , Id A (x , (a , a'))  Set)
  (β : Fib B)
  (b : B (a , reflId A a))
   -------------
  J {A = A} B β a (reflId A a) b  b
Jrefl {Γ} {A} {x} {a} B β b = extractEq (snd (Jinternal {A = A} B β a (reflId A a) b) tt) where
  extractEq :
    {b b' : B (a , reflId A a)}
     -------------
    triple A B a (reflId A a) b  triple A B a (reflId A a) b'  b  b' 
  extractEq {b} .{b} refl = refl