----------------------------------------------------------------------
-- 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.paths where

open import prelude
open import impredicative
open import interval
open import cof
open import fibrations

----------------------------------------------------------------------
-- Path types
----------------------------------------------------------------------
_~~_ : {A : Int  Set}(a : A O)(a' : A I)  Set
_~~_ {A} a a' =  p  (Π A)  (p O  a) & (p I  a') 

_~_ : {A : Set}(a a' : A)  Set
_~_ {A} a a' = _~~_ {A = λ _  A} a a'

transDep : {A : Int  Set}{α : Fib A}{a a' : A O}{b : A I}  (a ~~ b)  (a' ~~ b)  (a ~ a')
transDep {A} {α} {a} {a'} {b} (p , pO , pI) (q , qO , qI) = ((λ i  fst (r i)) , rO≡a , rI≡a') where
  f : (i : Int)  [ i ≈O  i ≈I ]  Π A
  f i u j = OI-elim cases u where
    cases : (i  O)  (i  I)  A j
    cases (inl _) = p j
    cases (inr _) = q j
    
  r : (i : Int)   a  (A O)  ((i ≈O  i ≈I) , f i)  O  a 
  r i = α I' id (i ≈O  i ≈I) (f i) (b , or-elim-eq  u  f i u I) b pI qI)

  rO≡a : fst (r O)  a
  rO≡a = trans pO (symm (snd (r O)  inl refl ))

  rI≡a' : fst (r I)  a'
  rI≡a' = trans qO (symm (snd (r I)  inr refl ))

transDep' : {A : Int  Set}{α : Fib A}{a : A O}{b b' : A I}  (a ~~ b)  (a ~~ b')  (b ~ b')
transDep' {A} {α} {a} {b} {b'} (p , pO , pI) (q , qO , qI) = ((λ i  fst (r i)) , rO≡a , rI≡a') where
  f : (i : Int)  [ i ≈O  i ≈I ]  Π A
  f i u j = OI-elim cases u where
    cases : (i  O)  (i  I)  A j
    cases (inl _) = p j
    cases (inr _) = q j
    
  r : (i : Int)   b  (A I)  ((i ≈O  i ≈I) , f i)  I  b 
  r i = α O' id (i ≈O  i ≈I) (f i) (a , or-elim-eq  u  f i u O) a pO qO)

  rO≡a : fst (r O)  b
  rO≡a = trans pI (symm (snd (r O)  inl refl ))

  rI≡a' : fst (r I)  b'
  rI≡a' = trans qI (symm (snd (r I)  inr refl ))

transPath : {A : Set}(α : Fib {Γ = Unit}  _  A)){x y z : A}  x ~ y  y ~ z  x ~ z
transPath {A} α {x} {y} {z} p q = ((λ i  fst (r i)) , rO≡x , rI≡z) where
  f : (i : Int)  [ i ≈O  i ≈I ]  Π  _  A)
  f i u j = OI-elim cases u where
    cases : (i  O)  (i  I)  A
    cases (inl _) = x 
    cases (inr _) = fst q j
  
  qO=pI : (i : Int)(eq : i  I)  fst q O  fst p i
  qO=pI .I refl = trans (symm (snd (snd p))) (fst (snd q))

  pO=pi : (i : Int)(l : i  O)  fst p O  fst p i
  pO=pi .O refl = refl
  
  r : (i : Int)   a  A  ((i ≈O  i ≈I) , f i)  I  a 
  r i = α O'  _  tt) (i ≈O  i ≈I) (f i)
    ((fst p i , or-elim-eq  u  f i u O) (fst p i)  {l}  trans (pO=pi i l) (symm (fst (snd p))))  {r}  qO=pI i r)))

  rO≡x : fst (r O)  x
  rO≡x = symm (snd (r O)  inl refl )

  rI≡z : fst (r I)  z
  rI≡z = trans (snd (snd q)) (symm (snd (r I)  inr refl ))

congPath :
  {A : Set}
  {B : Set}
  (f : A  B)
  {x y : A}
  (p : x ~ y)
   -----------
  f x ~ f y
congPath f p = ((f  (fst p)) , (cong f (fst (snd p))) , cong f (snd (snd p)))


Path : {Γ : Set}(A : Γ  Set)  Σ x  Γ , A x × A x  Set
Path A (x , (a , a')) = a ~ a'

reflPath : {Γ : Set}{A : Γ  Set}{x : Γ}(a : A x)  Path A (x , (a , a))
reflPath a = ((λ _  a) , refl , refl)

reflPath' : {A : Set}{a a' : A}  (a  a')  a ~ a'
reflPath' {A} {a} .{a} refl = ((λ _  a) , (refl , refl))

reflPathEval : {A : Set}{a a' : A}(p : a  a')(i : Int)  fst (reflPath' p) i  a'
reflPathEval refl i = refl

PathExt : {A : Set}{a a' : A}{p q : a ~ a'}  fst p  fst q  p  q
PathExt refl = Σext refl (Σext uipImp uipImp)

FibPath :
  {Γ : Set}
  {A : Γ  Set}
  (α : Fib A)
   -----------
  Fib (Path A)
FibPath {Γ} {A} α e p φ f path₀ = (path₁ , fExtends) where
  f' : Int  [ φ ]  Π (A  fst  p)
  f' i u j = fst (f u j) i
  
  f₀ : (i : Int)   g  ([ i ≈O ]  Π (A  fst  p))  (φ , f' i)  (i ≈O , g) 
  fst (f₀ i) _ j = fst (snd (p j))
  snd (f₀ .O) u refl = funext  j  fst (snd (f u j)))
  
  f₀' : (i : Int)  [ φ  i ≈O ]  Π (A  fst  p)
  f₀' i = _∪_ {φ = φ} {ψ = i ≈O} (f' i) (fst (f₀ i)) {p = snd (f₀ i)}
  
  f₁ : (i : Int)   g  ([ i ≈I ]  Π (A  fst  p))  ((φ  i ≈O) , f₀' i)   (i ≈I , g) 
  fst (f₁ i) _ j = snd (snd (p j))
  snd (f₁ .I) u refl = funext  j 
    or-elim-eq  v  f₀' I v j) (snd (snd (p j)))  {u'}  snd (snd (f u' j)))  {I≡O}  ∅-elim (O≠I (symm I≡O))) u)
    
  f₁' : (i : Int)  [ (φ  i ≈O)  i ≈I ]  Π (A  fst  p)
  f₁' i = _∪_ {φ = φ  i ≈O} {ψ = i ≈I} (f₀' i) (fst (f₁ i)) {p = snd (f₁ i)}
  
  extends : (i : Int)  prf ((((φ  i ≈O)  i ≈I) , f₁' i)   e   fst (fst path₀) i)
  extends i u = or-elim-eq  v  f₁' i v  e ) (fst (fst path₀) i)  {l}  leftCase l)  {r}  rightCase i r) u where
    rightCase : (i : Int)(r : i  I)  f₁' i  inr r   e   fst (fst path₀) i
    rightCase .I refl = symm (snd (snd (fst path₀)))
    leftCase : (l : prf (fst (φ  i ≈O)))  f₁' i  inl l   e   fst (fst path₀) i
    leftCase l = or-elim-eq  v  f₁' i  inl v   e ) (fst (fst path₀) i)  {l}  llCase l)  {r}  rlCase i r) l where
      rlCase : (i : Int)(r : i  O)  f₁' i  inl  inr r    e   fst (fst path₀) i
      rlCase .O refl = symm (fst (snd (fst path₀)))
      llCase : (l : [ φ ])  f₁' i  inl  inl l    e   fst (fst path₀) i
      llCase u = cong  p  fst p i) (snd path₀ u)
      
  comp : (i : Int)   a  ((A  fst  p)  ! e )  (((φ  i ≈O)  i ≈I) , f₁' i)   ! e   a 
  comp i = α e (fst  p) ((φ  i ≈O)  i ≈I) (f₁' i) (fst (fst path₀) i , extends i)
  
  path₁ : (Path A  p)  ! e 
  fst path₁ i = fst (comp i)
  fst (snd path₁) = symm eqAtO where
    eqAtO : fst (snd (p  ! e ))  fst (comp O)
    eqAtO = snd (comp O)  inl  inr refl  
  snd (snd path₁) = symm eqAtI where
    eqAtI : snd (snd (p  ! e ))  fst (comp I)
    eqAtI = snd (comp I)  inr refl 

  fExtends : prf ((φ , f)   ! e   path₁)
  fExtends u = PathExt (funext  i  snd (comp i)  inl  inl u  ))


funextPath : {A B : Set}{f g : A  B}  ((a : A)  f a ~ g a)  f ~ g
fst (funextPath pointwise) i a = fst (pointwise a) i
fst (snd (funextPath pointwise)) = funext  a  fst (snd (pointwise a)))
snd (snd (funextPath pointwise)) = funext  a  snd (snd (pointwise a)))