{-# 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
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)
~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 α
~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
~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))
isFibConst :
{ℓ ℓ' : Level}
{Γ : Set ℓ}
{A : Set ℓ'}
→
isFib (λ(_ : Γ) → A)
fst isFibConst _ _ _ = id
snd isFibConst _ = ~refl
Fib :
(ℓ : Level)
{ℓ' : Level}
(Γ : Set ℓ')
→
Set (ℓ' ⊔ lsuc ℓ)
Fib ℓ Γ = Σ A ∈ (Γ → Set ℓ) , isFib A
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