UniverseSIP.agda

{-# OPTIONS --cubical #-}

module UniverseSIP where

open import Cubical.Data.Prod
open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Core.Glue

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Foundations.CartesianKanOps
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Equiv

module _ where
  Σ-cong : ∀ {ℓx ℓa ℓb}{X : Type ℓx} (A : X → Type ℓa) (B : X → Type ℓb)
         → (A≃B : ∀ x → A x ≃ B x) → Σ _ A ≃ Σ _ B
  Σ-cong A B A≃B = isoToEquiv (iso f g f∘g g∘f) where
    f : Σ _ A → Σ _ B
    f (x , xa) = x , equivFun (A≃B x) xa
    g : Σ _ B → Σ _ A
    g (x , xb) = x , equivFun (invEquiv (A≃B x)) xb
    f∘g : ∀ x → f (g x) ≡ x
    f∘g (x , xb) i = x , A≃B x .snd .equiv-proof xb .fst .snd i
    g∘f : ∀ x → g (f x) ≡ x
    g∘f (x , xa) i = x , A≃B x .snd .equiv-proof (A≃B x .fst xa) .snd (xa , refl) i .fst

  Σ-change-of-variables : ∀{ℓx ℓy ℓa}{X : Type ℓx}{Y : Type ℓy}{A : Y → Type ℓa}
                        → (e : X ≃ Y) → Σ X (A ∘ equivFun e) ≃ Σ Y A
  Σ-change-of-variables {X = X} {Y} {A} e = isoToEquiv (iso f g f∘g g∘f) where
    loop : ∀ y → equivFun e (equivFun (invEquiv e) y) ≡ y
    loop y i = e .snd .equiv-proof y .fst .snd i
    pool : ∀ x → equivFun (invEquiv e) (equivFun e x) ≡ x
    pool x i = e .snd .equiv-proof (equivFun e x) .snd (x , refl) i .fst

    f : Σ X (A ∘ equivFun e) → Σ Y A
    f (x , a) = equivFun e x , a
    g : Σ Y A → Σ X (A ∘ equivFun e)
    g (y , a) = equivFun (invEquiv e) y , subst A (sym (loop y)) a
    f∘g : ∀ x → f (g x) ≡ x
    f∘g (y , a) i = loop y i , coe0→i (λ j → A (loop y (~ j))) (~ i) a
    g∘f : ∀ x → g (f x) ≡ x
    g∘f (x , a) i = pool x i , subst
        (λ b → PathP (λ k → A (equivFun e (pool x k))) (subst A (sym (loop (equivFun e x))) a) b)
        (substRefl {B = A} a) path i where
      path : PathP (λ k → A (equivFun e (pool x k))) (subst A (sym (loop (equivFun e x))) a) (subst A refl a)
      path i = subst A (sym (e .snd .equiv-proof (equivFun e x) .snd (x , refl) i .snd)) a

module BigSIP {u} (UNIV : Type u) (e : Level) where
  record Universe : Type (ℓ-max u (ℓ-suc e)) where
    field
      _≊_ : (S T : UNIV) → Type e
      id≊ : (S : UNIV) → S ≊ S
      ≡→≊ : ∀ {S T : UNIV} → (S ≡ T) → (S ≊ T)
      isEquiv≡→≊ : (S T : UNIV) → isEquiv (≡→≊ {S} {T})
      refl→id : ∀ {S} → ≡→≊ refl ≡ id≊ S

  module SIPDefinitions (U : Universe) {s : Level} (S : UNIV → Type s) where
    open Universe U
    ℓ-sns : Level → Level
    ℓ-sns w = ℓ-max (ℓ-max s (ℓ-suc w)) (ℓ-max u e)
    record SNS (w : Level) : Type (ℓ-sns w) where
      field
        ι : (X Y : Σ _ S) → (X .fst ≊ Y .fst) → Type w
        ρ : (X : Σ _ S) → ι X X (id≊ _)
      canonicalMap : ∀ {X} → (s t : S X) → s ≡ t → ι (X , s) (X , t) (id≊ _)
      canonicalMap {X} s t s≡t = subst _ s≡t (ρ (X , s))
      field
        θ : ∀ {X} → (s t : S X) → isEquiv (canonicalMap s t)

      canonicalEquiv : ∀ {X} → (s t : S X) → (s ≡ t) ≃ ι (X , s) (X , t) (id≊ _)
      canonicalEquiv s t = canonicalMap s t , θ s t

      canonicalEquiv′ : ∀ {X} → (s t : S X) → (s ≡ t) ≃ ι (X , s) (X , t) (≡→≊ refl)
      canonicalEquiv′ s t = compEquiv (canonicalEquiv s t) (transportEquiv ιPath) where
        ιPath : ι (_ , s) (_ , t) (id≊ _) ≡ ι (_ , s) (_ , t) (≡→≊ refl)
        ιPath = cong (ι (_ , s) (_ , t)) (sym refl→id)
        
      homomorphism-lemma : (A B : Σ _ S) (p : A .fst ≡ B .fst)
                         → (PathP (λ i → S (p i)) (A .snd) (B .snd)) ≃ ι A B (≡→≊ p)
      homomorphism-lemma (X , s) (Y , t) p = done where
        γ : (s ≡ subst S refl (subst S (sym p) t))
            ≃ ι (X , s) (X , subst S refl (subst S (sym p) t)) (≡→≊ refl)
        γ = canonicalEquiv′ s _
        almost : PathP (λ i → S (p i)) s (subst S p (subst S (sym p) t))
                 ≃ ι (X , s) (Y , subst S p (subst S (sym p) t)) (≡→≊ p)
        almost =
          J (λ Y′ X≡Y′ → PathP (λ i → S (X≡Y′ i)) s (subst S X≡Y′ (subst S (sym p) t))
                         ≃ ι (X , s) (Y′ , subst S X≡Y′ (subst S (sym p) t)) (≡→≊ X≡Y′)) γ p
        done : _
        done = subst (λ t → PathP (λ i → S (p i)) s t ≃ ι (X , s) (Y , t) (≡→≊ p))
                     (transportTransport⁻ (λ i → S (p i)) t) almost
      homomorphism-refl : (A : Σ _ S) → homomorphism-lemma A A refl ≡ canonicalEquiv′ _ _
      homomorphism-refl A =
        homomorphism-lemma A A refl
          ≡[ i ]⟨
            subst (λ t → (A .snd ≡ t) ≃ ι A (A .fst , t) (≡→≊ refl))
              (transportTransport⁻ refl (A .snd)) (
            JRefl (λ Y′ X≡Y′ → PathP (λ i → S (X≡Y′ i)) (A .snd) (subst S X≡Y′ (subst S refl (A .snd)))
                               ≃ ι A (Y′ , subst S X≡Y′ (subst S refl (A .snd))) (≡→≊ X≡Y′)) (
                  canonicalEquiv′ (A .snd) _
            ) i) 
          ⟩
        subst (λ t → (A .snd ≡ t) ≃ ι A (A .fst , t) (≡→≊ refl))
              (transportTransport⁻ refl (A .snd)) (
          canonicalEquiv′ (A .snd) _
        )
          ≡[ i ]⟨
            subst (λ t → (A .snd ≡ t) ≃ ι A (A .fst , t) (≡→≊ refl))
                  (λ j → transportTransport⁻ refl (A .snd) (j ∨ i)) (
              canonicalEquiv′ (A .snd) _
            )
          ⟩
        subst (λ t → (A .snd ≡ t) ≃ ι A (A .fst , t) (≡→≊ refl)) refl (
          canonicalEquiv′ (A .snd) _
        )
          ≡⟨ substRefl {B = λ t → (A .snd ≡ t) ≃ ι A (A .fst , t) (≡→≊ refl)} (canonicalEquiv′ (A .snd) _) ⟩
        canonicalEquiv′ _ _
          ∎
    open SNS renaming (ι to homomorphic ; ρ to idHomomorphism ; θ to isEquivCanonicalMap) public

  module SIP (U : Universe) where
    open SIPDefinitions U public
    open Universe U public

    _≃[_]_ : ∀ {s} {S : UNIV → Type s} {w} → Σ _ S → SNS S w → Σ _ S → Type _
    A ≃[ σ ] B = Σ[ f ∈ (A .fst ≊ B .fst) ] σ .homomorphic A B f

    characterization-of-≡ : ∀ {s} {S : UNIV → Type s} {w} (σ : SNS S w)
                          → (A B : Σ _ S)
                          → (A ≡ B) ≃ (A ≃[ σ ] B)
    characterization-of-≡ {S = S} σ A B =
      (A ≡ B)
        ≃⟨ invEquiv Σ≡ ⟩
      Σ[ p ∈ (A .fst ≡ B .fst) ] PathP (λ i → S (p i)) (A .snd) (B .snd)
        ≃⟨ Σ-cong _ _ (homomorphism-lemma S σ A B) ⟩
      Σ[ p ∈ (A .fst ≡ B .fst) ] homomorphic σ A B (≡→≊ p)
        ≃⟨ Σ-change-of-variables (≡→≊ , isEquiv≡→≊ (A .fst) (B .fst)) ⟩
      A ≃[ σ ] B
        ■
    characterization-of-refl : ∀ {s} {S : UNIV → Type s} {w} (σ : SNS S w) → {X : Σ _ S}
                             → characterization-of-≡ σ X X .fst refl ≡ (id≊ (X .fst) , idHomomorphism σ X)
    characterization-of-refl {S = S} σ {X} =
      characterization-of-≡ σ X X .fst refl
        ≡⟨ refl ⟩
      ( ≡→≊ refl , homomorphism-lemma _ σ X X refl .fst refl)
        ≡[ i ]⟨ ≡→≊ refl , homomorphism-refl S σ _ i .fst refl ⟩
      ( ≡→≊ refl , canonicalEquiv′ S σ _ _ .fst refl)
        ≡⟨ refl ⟩
      ( ≡→≊ refl , subst (homomorphic σ _ _) (sym refl→id) (canonicalMap S σ _ _ refl))
        ≡[ i ]⟨ ≡→≊ refl , subst (homomorphic σ _ _) (sym refl→id) (transportRefl (idHomomorphism σ X) i) ⟩
      ( ≡→≊ refl , subst (homomorphic σ _ _) (sym refl→id) (idHomomorphism σ X))
        ≡[ i ]⟨ refl→id i , coe1→i (λ i → homomorphic σ _ _ (refl→id i)) i (idHomomorphism σ X) ⟩
      (id≊ (X .fst) , idHomomorphism σ X)
        ∎

module IteratedSIP {u} {UNIV : Type u} {e} {U : BigSIP.Universe UNIV e} where
  open BigSIP UNIV e
  open SIP U

  iteratedUniv : ∀ {s} {S : UNIV → Type s} {w} (σ : SNS S w)
               → BigSIP.Universe (Σ _ S) _
  BigSIP.Universe._≊_ (iteratedUniv σ) = _≃[ σ ]_
  BigSIP.Universe.id≊ (iteratedUniv σ) X = _ , idHomomorphism σ X
  BigSIP.Universe.≡→≊ (iteratedUniv σ) = characterization-of-≡ σ _ _  .fst
  BigSIP.Universe.isEquiv≡→≊ (iteratedUniv σ) A B = characterization-of-≡ σ A B .snd
  BigSIP.Universe.refl→id (iteratedUniv σ) = characterization-of-refl σ

-- the "normal" sip
module PlainSIP (ℓ : Level) where
  open BigSIP (Type ℓ) ℓ
  TypeUniverse : Universe
  BigSIP.Universe._≊_ TypeUniverse = _≃_
  BigSIP.Universe.id≊ TypeUniverse = idEquiv
  BigSIP.Universe.≡→≊ TypeUniverse = univalence .fst
  BigSIP.Universe.isEquiv≡→≊ TypeUniverse _ _ = univalence .snd
  BigSIP.Universe.refl→id TypeUniverse = pathToEquivRefl

  open SIP TypeUniverse public

-- example, using the techniques from SIP for a structure depending on a family of types
module PointedSIP {ℓa} (𝒜 : Type ℓa) (ℓ-struct : Level) (ℓ : Level) where
  open BigSIP (𝒜 → Type ℓ) (ℓ-max ℓa ℓ)
  PointedUniverse : Universe
  PointedUniverse = record
    { _≊_ = _≊_
    ; id≊ = id≊
    ; ≡→≊ = sliceId→Eq _ _
    ; isEquiv≡→≊ = isEquivSliceId→Eq
    ; refl→id = sliceId→Eq≡idEquiv
    } where
    _≊_ : (S T : 𝒜 → Type ℓ) → Type (ℓ-max ℓa ℓ)
    S ≊ T = ∀ a → S a ≃ T a
    id≊ : (S : 𝒜 → Type ℓ) → S ≊ S
    id≊ S _ = idEquiv _

    sliceId→Eq : (S T : 𝒜 → Type ℓ)
               → S ≡ T → S ≊ T
    sliceId→Eq S T f a = pathToEquiv (funExt⁻ f a)

    isEquivSliceId→Eq : (S T : 𝒜 → Type ℓ)
                      → isEquiv (sliceId→Eq S T)
    isEquivSliceId→Eq S T = isoToIsEquiv (iso (sliceId→Eq S T) sliceEq→Id s r) where
      sliceEq→Id : S ≊ T → S ≡ T
      sliceEq→Id S≊T = funExt λ x → ua (S≊T x)
      s : ∀ x → sliceId→Eq S T (sliceEq→Id x) ≡ x
      s x = funExt λ a → pathToEquiv-ua (x a)
      r : ∀ p → sliceEq→Id (sliceId→Eq S T p) ≡ p
      r p i = funExt (λ x → ua-pathToEquiv (funExt⁻ p x) i)

    sliceId→Eq≡idEquiv : ∀ {X} → sliceId→Eq X X refl ≡ (id≊ X)
    sliceId→Eq≡idEquiv i _ = pathToEquivRefl i
  open Universe PointedUniverse
    renaming (≡→≊ to sliceId→Eq ; isEquiv≡→≊ to isEquivSliceId→Eq ; refl→id to sliceId→Eq≡idEquiv)
  open SIP PointedUniverse public
  
-- another example, working out associative ∞-magmas:
module ∞-magma (u : Level) where
  open PlainSIP u

  associative : {X : Type u} → (X → X → X) → Type u
  associative _·_ = ∀ x y z → (x · y) · z ≡ x · (y · z)

  ∞-magma-structure : Type u → Type u
  ∞-magma-structure X = X → X → X

  ∞-magma : Type (ℓ-suc u)
  ∞-magma = Σ[ X ∈ Type u ] ∞-magma-structure X

  magma-homomorphic : {X Y : Type u} → (X → X → X) → (Y → Y → Y) → (X → Y) → Type u
  magma-homomorphic {X} {Y} _·_ _*_ f = (λ (x y : X) → f (x · y)) ≡ (λ x y → f x * f y)

  magma-sns-data : SNS ∞-magma-structure u
  homomorphic magma-sns-data X Y (f , _) = magma-homomorphic (X .snd) (Y .snd) f
  idHomomorphism magma-sns-data X = refl
  isEquivCanonicalMap magma-sns-data s t = isoToIsEquiv (iso _ (idfun _) lemma lemma) where
    lemma : (a : s ≡ t) → subst (λ h → s ≡ h) a refl ≡ a
    lemma s≡t = fromPathP {A = λ k → s ≡ s≡t k} {x = refl} λ i j → s≡t (i ∧ j)

  ∞-amagma-structure : ∞-magma → Type u
  ∞-amagma-structure (_ , _·_) = (associative _·_)

  ∞-amagma : Type (ℓ-suc u)
  ∞-amagma = Σ ∞-magma ∞-amagma-structure

  respect-assoc : {X A : Type u } (_·_ : X → X → X) (_*_ : A → A → A)
                → associative _·_ → associative _*_
                → (f : X → A) → magma-homomorphic _·_ _*_ f → Type u
  respect-assoc _·_ _*_ α β f h  =  fα ≡ βf
    where
    l : ∀ x y z → f ((x · y) · z) ≡ (f x * f y) * f z
    l = λ x y z → f ((x · y) · z)   ≡[ i ]⟨ h i (x · y) z ⟩
                  f (x · y) * f z   ≡[ i ]⟨ h i x y * f z ⟩
                  (f x * f y) * f z ∎

    r : ∀ x y z → f (x · (y · z)) ≡ f x * (f y * f z)
    r = λ x y z → f (x · (y · z))   ≡[ i ]⟨ h i x (y · z) ⟩
                  f x * f (y · z)   ≡[ i ]⟨ f x * h i y z ⟩
                  f x * (f y * f z) ∎

    fα βf : ∀ x y z → (f x * f y) * f z ≡ f x * (f y * f z)
    fα x y z = sym (l x y z) ∙ cong f (α x y z) ∙ r x y z
    βf x y z = β (f x) (f y) (f z)

  open import Cubical.Foundations.GroupoidLaws
  rrr : ∀ {a}{A : Type a}{x y : A} (p : x ≡ y) → refl ∙ p ∙ refl ≡ p
  rrr p = sym (lUnit (p ∙ refl)) ∙ sym (rUnit p)
  p : ∀ {X} _·_ → (α : ∞-amagma-structure (X , _·_))
    → (λ x y z → sym (refl ∙ refl ∙ refl) ∙ (α x y z) ∙ (refl ∙ refl ∙ refl)) ≡ α
  p _ α = funExt λ x → funExt λ y → funExt λ z →
    sym (refl ∙ refl ∙ refl) ∙ α x y z ∙ (refl ∙ refl ∙ refl)
      ≡[ i ]⟨ sym (rrr refl i) ∙ α x y z ∙ rrr refl i ⟩
    refl ∙ α x y z ∙ refl
      ≡⟨ rrr (α x y z) ⟩
    α x y z
      ∎

  module ∞-magmaSIP = BigSIP.SIP _ _ (IteratedSIP.iteratedUniv magma-sns-data)
  amagma-sns-data : ∞-magmaSIP.SNS ∞-amagma-structure u
  homomorphic amagma-sns-data ((X , _·_) , α) ((Y , _⋆_) , β) ((f , _) , h) = respect-assoc _·_ _⋆_ α β f h
  idHomomorphism amagma-sns-data ((X , _·_) , α) = p _·_ α
  isEquivCanonicalMap amagma-sns-data {X = (X , _·_)} α β =
    isoToIsEquiv (iso intr elim intr∘elim elim∘intr) where
    intr : α ≡ β → respect-assoc _·_ _·_ α β _ _
    intr α≡β = subst (λ v → respect-assoc _·_ _·_ α v _ _) α≡β (p _·_ α)
    elim : respect-assoc _·_ _·_ α β _ _ → α ≡ β
    elim respects = sym (p _·_ α) ∙ respects

    intr∘elim : ∀ ras → intr (elim ras) ≡ ras
    intr∘elim ras =
      subst (λ v → respect-assoc _·_ _·_ α v _ _) (sym (p _·_ α) ∙ ras) (p _·_ α)
        ≡⟨ fromPathP {A = λ k → respect-assoc _·_ _·_ α ((sym (p _·_ α) ∙ ras) k) _ _} (λ i j → compPath-filler (p _·_ α) (sym (p _·_ α) ∙ ras) i j) ⟩
      (p _·_ α) ∙ (sym (p _·_ α) ∙ ras)
        ≡⟨ assoc _ _ _ ⟩
      ((p _·_ α) ∙ sym (p _·_ α)) ∙ ras
        ≡[ i ]⟨ rCancel (p _·_ α) i ∙ ras ⟩
      refl ∙ ras
        ≡⟨ sym (lUnit _) ⟩
      ras ∎
    elim∘intr : ∀ α≡β → elim (intr α≡β) ≡ α≡β
    elim∘intr α≡β =
      sym (p _·_ α) ∙ subst (λ v → respect-assoc _·_ _·_ α v _ _) α≡β (p _·_ α)
        ≡[ i ]⟨ sym (p _·_ α) ∙ fromPathP {A = λ k → respect-assoc _·_ _·_ α (α≡β k) _ _} (λ i j → compPath-filler (p _·_ α) α≡β i j) i ⟩
      sym (p _·_ α) ∙ (p _·_ α ∙ α≡β)
        ≡⟨ assoc _ _ _ ⟩
      (sym (p _·_ α) ∙ (p _·_ α)) ∙ α≡β
        ≡[ i ]⟨ lCancel (p _·_ α) i ∙ α≡β ⟩
      refl ∙ α≡β
        ≡⟨ sym (lUnit _) ⟩
      α≡β ∎

  _∞-amagma-≅_ : ∞-amagma → ∞-amagma → Type u
  ((X , _·_) , α) ∞-amagma-≅ ((Y , _*_) , β) =
    Σ[ ((f , _) , h) ∈ Σ[ (f , _) ∈ X ≃ Y ] magma-homomorphic _·_ _*_ f ] respect-assoc _·_ _*_ α β f h

  characterization-of-∞-aMagma-≡ : (A B : ∞-amagma) → (A ≡ B) ≃ (A ∞-amagma-≅ B)
  characterization-of-∞-aMagma-≡ =  ∞-magmaSIP.characterization-of-≡ amagma-sns-data