Derivative.Indexed.Univalence

{-# OPTIONS --safe #-}
module Derivative.Indexed.Univalence where

open import Derivative.Prelude
open import Derivative.Basics.Equiv using (univalenceᴰ)
open import Derivative.Indexed.Container

open import Cubical.Data.Sigma
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Equiv.Dependent
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Functions.FunExtEquiv


private
  variable
    ℓ : Level
    Ix : Type ℓ

module _ (F G : Container ℓ Ix) where
  open Container F renaming (Shape to S ; Pos to P)
  open Container G renaming (Shape to T ; Pos to Q)

  Coverᴰ : (f : S ≃ T) → Type _
  Coverᴰ f = ∀ ix → Σ[ e ∈ mapOver (equivFun f) (P ix) (Q ix) ] isEquivOver {Q = Q ix} e

  Cover : Type _
  Cover = Σ[ f ∈ S ≃ T ] Coverᴰ f

  Equiv≃Cover : (Equiv F G) ≃ Cover
  Equiv≃Cover =
    Equiv F G
      ≃⟨ Equiv-Σ-equiv F G ⟩
    Σ[ f ∈ S ≃ T ] (∀ ix s → Q ix (equivFun f s) ≃ P ix s)
      ≃⟨ Σ-cong-equiv-snd snd-equiv ⟩
    Cover
      ≃∎ where
    snd-equiv : (f : S ≃ T) → (∀ ix s → Q ix (equivFun f s) ≃ P ix s) ≃ Coverᴰ f
    snd-equiv f =
      (∀ ix s → Q ix (equivFun f s) ≃ P ix s)
        ≃⟨ equivΠCod (λ ix → equivΠCod λ s → invEquivEquiv) ⟩
      (∀ ix s → P ix s ≃ Q ix (equivFun f s))
        ≃⟨ equivΠCod (λ ix → Σ-Π-≃) ⟩
      (∀ ix → Σ[ e ∈ (∀ s → P ix s → Q ix (equivFun f s)) ] (∀ s → isEquiv (e s)))
        ≃∎

  Cover≃Path : Cover ≃ (F ≡ G)
  Cover≃Path =
    Cover
      ≃⟨ Σ-cong-equiv-snd (λ e → equivΠCod λ ix → invEquiv (univalenceᴰ e)) ⟩
    Σ[ e ∈ S ≃ T ] (∀ ix → PathP (λ i → ua e i → Type ℓ) (P ix) (Q ix))
      ≃⟨ Σ-cong-equiv-fst (invEquiv univalence) ⟩
    Σ[ p ∈ S ≡ T ] (∀ ix → PathP (λ i → p i → Type ℓ) (P ix) (Q ix))
      ≃⟨ Σ-cong-equiv-snd (λ p → funExtEquiv) ⟩
    Σ[ p ∈ S ≡ T ] (PathP (λ i → Ix → p i → Type ℓ) P Q)
      ≃⟨ ΣPathP≃PathPΣ ⟩
    (S , P) ≡ (T , Q)
      ≃⟨ invEquiv (congEquiv Container-Σ-equiv) ⟩
    (F ≡ G)
      ≃∎

  Equiv≃Path : (Equiv F G) ≃ (F ≡ G)
  Equiv≃Path = Equiv≃Cover ∙ₑ Cover≃Path

ContainerEquivContr : (G : Container ℓ Ix) → ∃![ F ∈ Container _ _ ] Equiv F G
ContainerEquivContr G = isOfHLevelRespectEquiv  (Σ-cong-equiv-snd λ F → symEquiv ∙ₑ invEquiv (Equiv≃Path F G)) (isContrSingl G)

contrContainerSinglEquiv : {F G : Container ℓ Ix}
  → (e : Equiv F G)
  → (G , idₑ G) ≡ (F , e)
contrContainerSinglEquiv {F} {G} e = isContr→isProp (ContainerEquivContr G) (G , idₑ G) (F , e)

opaque
  ContainerEquivJ : ∀ {ℓ'} {F G : Container ℓ Ix}
    → (P : (F : Container ℓ Ix) → Equiv F G → Type ℓ')
    → (r : P G (idₑ G))
    → (e : Equiv F G) → P F e
  ContainerEquivJ P r e = subst (λ (F , e) → P F e) (contrContainerSinglEquiv e) r

isEquivContainerEquivPreComp : {F G : Container ℓ Ix}
  → (e : F ⧟ G)
  → (H : Container ℓ Ix)
  → isEquiv (λ (g : G ⊸ H) → Equiv.as-⊸ e ⋆ g)
isEquivContainerEquivPreComp {ℓ} {Ix} {G} = ContainerEquivJ
  (λ F e → ∀ H → isEquiv (λ (g : G ⊸ H) → Equiv.as-⊸ e ⋆ g))
  is-equiv-at-id
  where
    is-equiv-at-id : (H : Container ℓ Ix) → isEquiv (λ (g : G ⊸ H) → Equiv.as-⊸ (idₑ G) ⋆ g)
    is-equiv-at-id H = isoToIsEquiv iso where
      iso : Iso (G ⊸ H) (G ⊸ H)
      iso .Iso.fun = Equiv.as-⊸ (idₑ G) ⋆_
      iso .Iso.inv = idfun _
      iso .Iso.rightInv g = ⋆-id-left g
      iso .Iso.leftInv g = ⋆-id-left g

containerEquivPreCompEquiv : {F G : Container ℓ Ix}
  → (e : F ⧟ G)
  → (H : Container ℓ Ix)
  → (G ⊸ H) ≃ (F ⊸ H)
containerEquivPreCompEquiv e H .fst = Equiv.as-⊸ e ⋆_
containerEquivPreCompEquiv e H .snd = isEquivContainerEquivPreComp e H