{-# OPTIONS --rewriting #-}

module Contractible where

open import Bijection
open import Empty
open import Equality
open import EquationalReasoning
open import FunctionExtensionality
open import Fibration
open import Function
open import Interval
open import Level
open import Path
open import Product
open import Proposition
open import Quotient
open import Sum
open import UIP
open import Unit
 
----------------------------------------------------------------------
-- Path-contractible types
----------------------------------------------------------------------
record isContr {ℓ : Level}(A : Set ℓ) : Set ℓ where
  field
    centre  : A
    ~centre : (x : A) → x ~ centre

open isContr{{...}} public

----------------------------------------------------------------------
-- Path-to-1 for a fibrant family of contractible types
----------------------------------------------------------------------
Λeq :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {x : Γ}
  (i : 𝕀)
  → ----------------
  A x → A x → Set ℓ'
Λeq _ i a b = (a ≡ b) or Lift (i ≡ I)

Λ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  → ---------------
  Γ × 𝕀 → Set ℓ'
Λ {ℓ} {ℓ'} A (x , i) = A x / Λeq A i

ΛO :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {x : Γ}
  → ------------------
  A x → Λ A (x , O)
ΛO A a  = [ a ]/ Λeq A O

ΛO⁻¹ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {x : Γ}
  → ------------------
  Λ A (x , O) → A x
ΛO⁻¹ A {x} = qrec (Λeq A O) (A x) id f where
  f : (a b : A x) → Λeq A O a b → a ≡ b
  f a b p = orrec id g (λ _ _ → uip) guniq h p where
    g : Lift (O ≡ I) → a ≡ b
    g (lift p) = Ø-elim (O≠I p)

    guniq : (u v : Lift (O ≡ I)) → g u ≡ g v
    guniq (lift _) (lift _) = cong (g ∘ lift) uip

    h : (p : a ≡ b)(u : Lift(O ≡ I)) → p ≡ g u
    h _ (lift p) = Ø-elim (O≠I p)

ΛO⁻¹∘ΛO :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {x : Γ}
  (a : A x)
  → ---------------------------
  ΛO⁻¹ A (ΛO A a) ≡ a
ΛO⁻¹∘ΛO _ _ = refl

ΛO∘ΛO⁻¹ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {x : Γ}
  (c : Λ A (x , O))
  → ---------------------------
  ΛO A (ΛO⁻¹ A c) ≡ c
ΛO∘ΛO⁻¹ A =
  qelim
    (Λeq A O)
    (λ c → ΛO A (ΛO⁻¹ A c) ≡ c)
    (λ _ → refl)
    (λ _ _ _ → uip)

instance
  isBijΛO :
    {ℓ ℓ' : Level}
    {Γ : Set ℓ}
    (A : Γ → Set ℓ')
    {x : Γ}
    → -------------------
    isBij (ΛO A {x})
  _⁻¹  {{isBijΛO A}} = ΛO⁻¹ A
  bijl {{isBijΛO A}} = funext (ΛO⁻¹∘ΛO A)
  bijr {{isBijΛO A}} = funext (ΛO∘ΛO⁻¹ A)

ΛI :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  (κ_ : (x : Γ) → isContr (A x))
  (x : Γ)
  → -----------------------------
  ⊤ → Λ A (x , I)
ΛI A κ x _ = [ centre {{κ x}} ]/ Λeq A I

ΛI⁻¹ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {x : Γ}
  → ----------------
  Λ A (x , I) → ⊤
ΛI⁻¹ _ _ = tt

ΛI⁻¹∘ΛI :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {κ : (x : Γ) → isContr (A x)}
  {x : Γ}
  (a : ⊤)
  → --------------------------------------
  ΛI⁻¹ A (ΛI A κ x a) ≡ a
ΛI⁻¹∘ΛI _ _ = refl

ΛI∘ΛI⁻¹ :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  (κ : (x : Γ) → isContr (A x))
  (x : Γ)
  (c : Λ A (x , I))
  → --------------------------------
  ΛI A κ x (ΛI⁻¹ A c) ≡ c
ΛI∘ΛI⁻¹ A κ x =
  qelim
    (Λeq A I)
    (λ c → ΛI A κ x (ΛI⁻¹ A c) ≡ c)
    (λ _ → by (inr (lift refl) mod∇))
    (λ _ _ _ → uip)
    
instance
  isBijΛI :
    {ℓ ℓ' : Level}
    {Γ : Set ℓ}
    (A : Γ → Set ℓ')
    (κ : (x : Γ) → isContr (A x))
    (x : Γ)
    → ---------------------------
    isBij (ΛI A κ x)
  _⁻¹  {{isBijΛI A κ x}} = ΛI⁻¹ A
  bijl {{isBijΛI A κ x}} = funext (ΛI⁻¹∘ΛI A {κ} {x})
  bijr {{isBijΛI A κ x}} = funext (ΛI∘ΛI⁻¹ A κ x)

ΛAct :
  {ℓ ℓ' : Level}
  {Γ : Set ℓ}
  (A : Γ → Set ℓ')
  {{_ : isFib A}}
  (κ : (x : Γ) → isContr (A x))
  {xi yj : Γ × 𝕀}
  (p : xi ~ yj)
  → ---------------------------
  Λ A xi → Λ A yj
ΛAct A {{α}} κ {x , i} {y , j} p =
  qrec (Λeq A i) (Λ A (y , j)) f e
  where
  f : A x → Λ A (y , j)
  f a = [ (~centre {{κ y}} (~cong fst p ∗ a)) at i ]/ Λeq A j

  e : (a b : A x)(u : Λeq A i a b) → f a ≡ f b
  e a b u = orrec (cong f) g (λ _ _ → uip) (λ _ _ → uip) (λ _ _ → uip) u
    where
    g : Lift (i ≡ I) → f a ≡ f b
    g (lift u) =
      proof:
        [ (~centre {{κ y}} (~cong fst p ∗ a)) at i ]/ Λeq A j
      ≡[ cong (λ i → [ (~centre {{κ y}} (~cong fst p ∗ a)) at i ]/ Λeq A j)
         u ]
        [ centre {{κ y}} ]/ Λeq A j
      ≡[ cong (λ i → [ (~centre {{κ y}} (~cong fst p ∗ b)) at i ]/ Λeq A j)
         (symm u) ]
        [ (~centre {{κ y}} (~cong fst p ∗ b)) at i ]/ Λeq A j
      qed