{-# OPTIONS --rewriting #-}

module Fibration where

open import Equality
open import EquationalReasoning
open import Function
open import FunctionExtensionality
open import Interval
open import Level
open import Path
open import Product
open import UIP

----------------------------------------------------------------------
-- Fibration structure
----------------------------------------------------------------------
isFib :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  → --------------
  Set (ℓ ⊔ ℓ')
isFib A =
  Σ s ∈ ((x y : _) → (x ~ y) → A x → A y),
  ((x : _)(a : A x) → a ~ s x x (~refl x) a)
{- using a Σ-type rather than a record type, and no implicit
arguments, makes it easier to prove properties of equality of
fibration structures via Σext -- see for example Fib'id and Fib'comp
below -}

~subst :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  (α : isFib A)
  {x y : Γ}
  (p : x ~ y)
  → --------------
  A x → A y
~subst α  = fst α _ _

~substrefl :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  (α : isFib A)
  {x : Γ}
  (a : A x)
  → ----------------------
  a ~ ~subst α (~refl x) a
~substrefl α = snd α _ 

infixr  _∗_
_∗_ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  {{α : isFib A}}
  {x y : Γ}
  (p : x ~ y)
  → -------------
  A x → A y
_∗_ {{α}} = ~subst α

-- asociativity of transport
~substassoc :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  {{α : isFib A}}
  {x y z : Γ}
  (q : y ~ z)
  (p : x ~ y)
  (a : A x)
  → -----------------------
  (q ∙ p) ∗ a ~ q ∗ (p ∗ a)
~substassoc {{α}} q p a =
  path:
    (q ∙ p) ∗ a
  ~[ ~cong ((q ∙ p) ∗_) (~substrefl α a) ]
    (q ∙ p) ∗ (~refl _ ∗ a)
  ~[ ⟨ i ⟩((q ∙ (p from i)) ∗ ((p upto i) ∗ a)) ]
    (q ∙ ~refl _) ∗ (p ∗ a)
  ~[ ~cong (_∗ (p ∗ a)) (~symm (∙refl q)) ]
    q ∗ (p ∗ a)
  endp

----------------------------------------------------------------------
-- Path lifting
----------------------------------------------------------------------
~lift' :
  {ℓ  ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  {{_ : isFib A}}
  {x y : Γ}
  (p : x ~ y)
  (a : A x)
  → -------------------------------
  (x , (~refl x) ∗ a) ~ (y , p ∗ a)
~lift' p a = ⟨ i ⟩(p at i , (p upto i) ∗ a)

~lift'refl :
  {ℓ  ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  {{_ : isFib A}}
  (x : Γ)
  (a : A x)
  → ------------------------------------------
  ~lift' (~refl x) a ≡ ~refl (x , ~refl x ∗ a)
~lift'refl _ _ = atInj refl

~lift :
  {ℓ  ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  {{_ : isFib A}}
  {x y : Γ}
  (p : x ~ y)
  (a : A x)
  → -------------------
  (x , a) ~ (y , p ∗ a)
~lift {{α}} {x} p a = ~lift' p a ∙ ~cong (x ,_) (~substrefl α a)

~liftrefl :
  {ℓ  ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  {{α : isFib A}}
  (x : Γ)
  (a : A x)
  → -----------------------------------------------
  ~lift (~refl x) a ~ ~cong (x ,_) (~substrefl α a) 
~liftrefl {{α}} x a =
  path:
    ~lift' (~refl x) a ∙ ~cong (x ,_) (~substrefl α a)
  ~[ ≡to~ (cong (_∙ ~cong (x ,_) (~substrefl α a)) (~lift'refl x a)) ]
    ~refl (x , ~refl x ∗ a) ∙ ~cong (x ,_) (~substrefl α a)
  ~[ ~symm (refl∙ (~cong (x ,_) (~substrefl α a))) ]
    ~cong (x ,_) (~substrefl α a)
  endp

I~∗O :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (f : (x : Γ) → A x)
  {x y : Γ}
  (p : x ~ y)
  → -----------------
  f y ~ p ∗ f x
I~∗O A {{α}} f {x} {y} p =
  ⟨ i ⟩((p from (rev i)) ∗ f (p at (rev i))) ∙ ~substrefl α (f y)  

I~∗Oid :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{α : isFib A}}
  (f : (x : Γ) → A x)
  (x : Γ)
  → -------------------------------------
  ~substrefl α (f x) ~ I~∗O A f (~refl x)
I~∗Oid A {{α}} f x = refl∙ (~substrefl α (f x))

snd' :
  {ℓ  ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  {{_ : isFib A}}
  {x y : Γ}
  {a : A x}
  {b : A y}
  (p : (x , a) ~ (y , b))
  → ---------------------
  (~cong fst p) ∗ a ~ b
snd' {{α}} (path f)  =
  ~symm (~substrefl α (snd (f I))) ∙
  ⟨ i ⟩(~subst α (⟨ j ⟩(fst (f (cvx i j I)))) (snd (f i)))

snd'idp :
  {ℓ  ℓ' : Level}
  {Γ : Set ℓ}
  {A : Γ → Set ℓ'}
  {{α : isFib A}}
  (x : Γ)
  (a : A x)
  → -------------------------------------------
  ~symm (~substrefl α a) ~ snd' (~refl (x , a)) 
snd'idp {{α}} x a = 
  path:
    ~symm (~substrefl α a)
  ~[ ∙refl (~symm (~substrefl α a)) ]
    ~symm (~substrefl α a) ∙ ~refl (~subst α (~refl x) a)
  ~[ ≡to~ (cong (~symm (~substrefl α a) ∙_) u) ]
    ~symm (~substrefl α a) ∙ ⟨ i ⟩(~subst α ((~refl x) from i) a)   
  endp
  where
  u : ~refl (~subst α(~refl x)a) ≡ ⟨ i ⟩(~subst α((~refl x) from i)a)
  u = atInj (funext (λ _ → refl))

----------------------------------------------------------------------
-- Constant families
----------------------------------------------------------------------
isFibConst :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  {A : Set ℓ'}
  → ------------------
  isFib (λ(_ : Γ) → A)
fst isFibConst _ _ _ = id
snd isFibConst _     = ~refl 

----------------------------------------------------------------------
-- Fibrations
----------------------------------------------------------------------
Fib :
  (ℓ : Level)
  {ℓ' : Level}
  (Γ : Set ℓ')
  → ---------------
  Set (ℓ' ⊔ lsuc ℓ)
Fib ℓ Γ =  Σ A ∈ (Γ → Set ℓ) , isFib A

----------------------------------------------------------------------
-- Re-indexing fibrations
----------------------------------------------------------------------
isFib' :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ'}
  {Γ' : Set ℓ''}
  (γ : Γ' → Γ)
  {A : Γ → Set ℓ}
  (α : isFib A)
  → ---------------
  isFib (A ∘ γ)
fst (isFib' γ α) _ _ = fst α (γ _) (γ _) ∘ ~cong γ
snd (isFib' γ α) _   = snd α (γ _) 

Fib' :
  {ℓ ℓ' ℓ'' : Level}
  {Γ : Set ℓ'}
  {Γ' : Set ℓ''}
  (γ : Γ' → Γ)
  → -------------------
  Fib ℓ Γ → Fib ℓ Γ'
Fib' γ (A , α) = (A ∘ γ , isFib' γ α)

isFib'id :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ'} 
  {A : Γ → Set ℓ}
  (α : isFib A)
  → --------------
  isFib' id α ≡ α
isFib'id (_ , _) = Σext refl refl 

Fib'id :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ'}
  (Φ : Fib ℓ Γ)
  → ------------
  Fib' id Φ ≡ Φ
Fib'id _ = Σext refl refl

isFib'comp :
  {ℓ ℓ' ℓ'' ℓ''' : Level}
  {Γ : Set ℓ'}
  {Γ' : Set ℓ''}
  {Γ'' : Set ℓ'''}
  (γ : Γ' → Γ)
  (γ' : Γ'' → Γ')
  {A : Γ → Set ℓ}
  (α : isFib A)
  → ----------------------------------------
  isFib' γ' (isFib' γ α) ≡ isFib' (γ ∘ γ') α
isFib'comp _ _ _ = Σext refl refl

Fib'comp :
  {ℓ ℓ' ℓ'' ℓ''' : Level}
  {Γ : Set ℓ'}
  {Γ' : Set ℓ''}
  {Γ'' : Set ℓ'''}
  (γ : Γ' → Γ)
  (γ' : Γ'' → Γ')
  (Φ : Fib ℓ Γ)
  → -----------------------------------
  Fib' γ' (Fib' γ Φ) ≡ Fib' (γ ∘ γ') Φ
Fib'comp _ _ _ = Σext refl refl