```{-# 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 6 _∗_
_∗_ :
{ℓ ℓ' : 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
```