----------------------------------------------------------------------
-- 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 fibrations where 

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

----------------------------------------------------------------------
-- Path composition structure
----------------------------------------------------------------------
Comp : OI  (Int  Set)  Set
Comp e A = (φ : Cof)(f : [ φ ]  Π A) 
   x₁  (A  e )  (φ , f)   e   x₁  
   x₀  (A  ! e )  (φ , f)   ! e   x₀ 

----------------------------------------------------------------------
-- Fibrations
----------------------------------------------------------------------
Fib : {Γ : Set}(A : Γ  Set)  Set
Fib {Γ} A = (e : OI)(p : Int  Γ)  Comp e (A  p)

----------------------------------------------------------------------
-- Terminal object is fibrant
----------------------------------------------------------------------
FibUnit : {Γ : Set}  Fib(λ(_ : Γ)  Unit)
fst (FibUnit _ _ _ _ (unit , _))   = unit
snd (FibUnit _ _ _ _ (unit , _)) _ = refl

----------------------------------------------------------------------
-- Initial object is fibrant
----------------------------------------------------------------------
Fib∅ : {Γ : Set}  Fib(λ(_ : Γ)  )
Fib∅ _ _ _ _ (() , _)

----------------------------------------------------------------------
-- Fibrations are closed under isomorphism
----------------------------------------------------------------------
_≅_ : {Γ : Set}(A B : Γ  Set)  Set
_≅_ {Γ} A B = (x : Γ)  Σ f  (A x  B x) , Σ g  (B x  A x) , (g  f  id) × (f  g  id)

FibIso : {Γ : Set}(A B : Γ  Set)  (A  B)  Fib A  Fib B
FibIso A B iso α e p φ q b = b' where
  !e : Int
  !e =  ! e 
  f : (i : Int)  A (p i)  B (p i)
  f i = fst (iso (p i))
  g : (i : Int)  B (p i)  A (p i)
  g i = fst (snd (iso (p i)))
  q' : [ φ ]  Π (A  p)
  q' u i = g i (q u i)
  a :  a  ((A  p)  e )  ((φ , q')   e )  a 
  fst a = g  e  (fst b)
  snd a u = cong (g  e ) (snd b u)
  a' :  a  ((A  p) !e)  ((φ , q')  !e)  a 
  a' = α e p φ q' a
  b' :  b  ((B  p) !e)  ((φ , q)  !e)  b 
  fst b' = f !e (fst a')
  snd b' u = trans fgq≡b' (symm (fgq≡q)) where
    fgq≡b' : f !e (g !e (q u !e))  fst b'
    fgq≡b' = cong (f !e) (snd a' u)
    fgq≡q : f !e (g !e (q u !e))  q u !e
    fgq≡q = cong  f  f (q u !e)) (snd (snd (snd (iso (p !e)))))

----------------------------------------------------------------------
-- Path filling structure
----------------------------------------------------------------------
Fill : OI  (Int  Set)  Set
Fill e A =
  (φ : Cof)
  (f : [ φ ]  Π A)
  (a : A  e )
  (_ : prf ((φ , f)   e   a))
   --------------------------------------
   p  Π A  ((φ , f )  p) & (p  e   a) 

----------------------------------------------------------------------
-- Compatible partial functions
----------------------------------------------------------------------
_⌣_ : {A : Set}   A   A  Ω
(φ , f)  (ψ , g) = All u  [ φ ] , All v  [ ψ ] , f u  g v

_∪_ :
  {A : Set}
  {φ ψ : Cof}
  (f : [ φ ]  A)
  (g : [ ψ ]  A)
  {p : prf((φ , f)  (ψ , g))}
   ---------------------------
  [ φ  ψ ]  A
_∪_ {A} {φ} {ψ} f g {p} w = ∥∥-elim h q w where

  h : [ φ ]  [ ψ ]  A
  h (inl u) = f u
  h (inr v) = g v

  q : (z z' : [ φ ]  [ ψ ])  h z  h z'
  q (inl _) (inl _) = cong f (eq (fst φ))
  q (inl u) (inr v) = p u v
  q (inr v) (inl u) = symm (p u v)
  q (inr _) (inr _) = cong g (eq (fst ψ))

----------------------------------------------------------------------
-- Path filling from path composition
----------------------------------------------------------------------

private
 fillInternal :
  {Γ : Set}
  {A : Γ  Set}
  (e : OI)
  (α : Fib A)
  (p : Int  Γ)
  (φ : Cof)
  (f : [ φ ]  Π (A  p))
  (a : A (p  e ))
  (u : prf ((φ , f)   e   a))
   -----------
  Σ fill   p  Π (A  p)  ((φ , f )  p) & (p  e   a)  , fst fill  ! e   fst (α e p φ f (a , u))
fillInternal {Γ} {A} e α p φ f a u = (result , fillAtOne) where
  p' : (i : Int)  Int  Γ
  p' i j = p (cnx e i j)

  f' : (i : Int)  [ φ ]  Π(A  (p' i))
  f' i u j = f u (cnx e i j)

  g : (i : Int)  [ i ≈OI e ]  Π(A  (p' i))
  g .( e ) refl j = a

  agree : (i : Int)  prf ((φ , f' i)  (i ≈OI e , g i))
  agree .( e ) v refl = funext  j  u v)

  h : (i : Int)  [ φ  i ≈OI e ]  Π(A  (p' i))
  h i = _∪_ {φ = φ} {ψ = i ≈OI e} (f' i) (g i) { p = agree i }

  AtZero : Int  Ω
  AtZero i = ((φ  i ≈OI e) , h i)   e   a
  hAtZero : (i : Int)  prf (AtZero i)
  hAtZero i v = ∥∥-rec (AtZero i) (cases i) v v where
    cases : (i : Int)  prf (fst φ)  (i   e )  prf (AtZero i)
    cases i (inl x) v = -- φ holds
      proof:
        snd (((φ  i ≈OI e) , h i)   e ) v
          ≡[ cong (snd (((φ  i ≈OI e) , h i)   e )) (equ ((fst φ or i   e )) v ( inl x )) ]≡
        snd (((φ  i ≈OI e) , h i)   e ) ( inl x )
          ≡[ refl ]≡
        f x  e 
          ≡[ u x ]≡
        a
      qed
    cases .( e ) (inr refl) v = -- i=0 holds
      proof:
        snd (((φ   e  ≈OI e) , h  e )   e ) v
          ≡[ cong (snd (((φ   e  ≈OI e) , h  e )   e )) (equ ((fst φ or  e    e )) v ( inr refl )) ]≡
        snd (((φ   e  ≈OI e) , h  e )   e ) ( inr refl )
          ≡[ refl ]≡
        g  e  refl  e 
          ≡[ refl ]≡
        a
      qed

  fill : (i : Int)   a  (A  p) i  ((φ  i ≈OI e) , h i)   ! e   a 
  fill i = (α e (p' i) (φ  i ≈OI e) (h i) (a , hAtZero i))

  extendsF : (v : [ φ ])(i : Int)  f v i  fst (fill i)
  extendsF v i = snd (fill i)  inl v 

  atZero : fst (fill  e )  a
  atZero = symm (snd (fill  e )  inr refl )

  result :  p  Π (A  p)  ((φ , f )  p) & (p  e   a) 
  fst result i = fst (fill i)
  fst (snd result) v = funext (extendsF v)
  snd (snd result) = atZero

  φAtOne : (φ   ! e  ≈OI e)  φ
  φAtOne = cofEq (propext forwards backwards) where
    forwards : prf (fst (φ   ! e  ≈OI e))  prf (fst φ)
    forwards v = ∥∥-rec (fst φ) cases v where
      cases : prf (fst φ)  ( ! e    e )  prf (fst φ)
      cases (inl p) = p
      cases (inr !e=e) = e≠!e (symm !e=e)
    backwards : prf (fst φ)  prf (fst (φ   ! e  ≈OI e))
    backwards v =  inl v 

  propSwap :
    {A : Set}
    {P Q : Cof}
    (p : P  Q)
    {f : [ P ]  A}
    (u : [ Q ])
    (v : [ P ])
     -----------
    subst  φ  [ φ ]  A) p f u  f v
  propSwap {A} {P} .{P} refl {f} u v = cong f (equ (fst P) u v)

  hAtOne : _≡_ {A =  ((i : Int)  A (p i))} ((φ   ! e  ≈OI e) , h  ! e ) (φ , f)
  hAtOne = Σext φAtOne (funext hIi≡fi) where
    hIi≡fi : (u : [ φ ])  subst  φ₁  [ φ₁ ]  (i : Int)  A (p i)) φAtOne (h  ! e ) u  f u
    hIi≡fi u =
      proof:
        subst  φ₁  [ φ₁ ]  (i : Int)  A (p i)) φAtOne (h  ! e ) u
          ≡[ propSwap φAtOne u   inl u  ]≡
        h  ! e    inl u 
          ≡[ refl ]≡
        f u
      qed

  tupleFiddle :
    {A : Set}
    {B : A  Set}
    {C : (x : A)  B x  Set}
    {a a' : A}
    {b : B a}{b' : B a'}
    {c : C a b}{c' : C a' b'}
    (p : ((a , b) , c)  ((a' , b') , c'))
     -----------
    (a , (b , c))  (a' , (b' , c'))
  tupleFiddle refl = refl

  abstract
   fillAtOne : fst (fill  ! e )  fst (α e p φ f (a , u))
   fillAtOne =
    proof:
      fst (fill  ! e )
        ≡[ refl ]≡
      fst (α e p (φ   ! e  ≈OI e) (h  ! e ) (a , hAtZero  ! e ))
        ≡[ cong (λ{(ψ , f , u)  fst (α e p ψ f (a , u))}) (tupleFiddle (Σext hAtOne (eq (((φ , f)   e   a))))) ]≡
      fst (α e p φ f (a , u)) 
    qed

abstract
 fill :
  {Γ : Set}
  {A : Γ  Set}
  (e : OI)
  (α : Fib A)
  (p : Int  Γ)
   -----------
  Fill e (A  p)
 fill {Γ} {A} e α p φ f a u = fst (fillInternal {A = A} e α p φ f a u)

abstract
 fillAtEnd :
  {Γ : Set}
  {A : Γ  Set}
  (e : OI)
  (α : Fib A)
  (p : Int  Γ)
  (φ : Cof)
  (f : [ φ ]  Π (A  p))
  (a : A (p  e ))
  (u : prf ((φ , f)   e   a))
   -----------
  fst (fill {A = A} e α p φ f a u)  ! e   fst (α e p φ f (a , u))
 fillAtEnd {Γ} {A} α e p φ f a u = snd (fillInternal {A = A} α e p φ f a u)