From e997ccd847a475611621e0e2c9caceb78ff5805c Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Fri, 2 Aug 2024 18:04:47 +0200 Subject: [PATCH] univalence for comm algebras with Evans help --- Cubical/Algebra/CommAlgebraAlt/Base.agda | 30 ++++------ .../Algebra/CommAlgebraAlt/Univalence.agda | 58 +++++++++---------- 2 files changed, 38 insertions(+), 50 deletions(-) diff --git a/Cubical/Algebra/CommAlgebraAlt/Base.agda b/Cubical/Algebra/CommAlgebraAlt/Base.agda index a3e3c600d..1b8143839 100644 --- a/Cubical/Algebra/CommAlgebraAlt/Base.agda +++ b/Cubical/Algebra/CommAlgebraAlt/Base.agda @@ -9,10 +9,12 @@ open import Cubical.Foundations.Structure using (⟨_⟩) open import Cubical.Foundations.HLevels open import Cubical.Foundations.Univalence open import Cubical.Foundations.Transport +open import Cubical.Foundations.Path open import Cubical.Data.Sigma open import Cubical.Algebra.CommRing +open import Cubical.Algebra.CommRing.Univalence open import Cubical.Algebra.Ring private @@ -73,26 +75,6 @@ module _ {R : CommRing ℓ} where p) where open CommRingStr (B .fst .snd) using (is-set) - CommAlgebra≡ : - {A B : CommAlgebra R ℓ'} - → (p : (A .fst) ≡ (B .fst)) - → (pathToEquiv $ cong fst p) .fst ∘ (A .snd) .fst ≡ (B .snd) .fst - → A ≡ B - CommAlgebra≡ {A = A} {B = B} p q = ΣPathTransport→PathΣ A B (p , pComm) - where - pComm : subst (CommRingHom R) p (A .snd) ≡ B .snd - pComm = - CommRingHom≡ - (fst (subst (CommRingHom R) p (A .snd)) - ≡⟨ sym (substCommSlice (CommRingHom R) (λ X → ⟨ R ⟩ → ⟨ X ⟩) (λ _ → fst) p (A .snd)) ⟩ - subst (λ X → ⟨ R ⟩ → ⟨ X ⟩) p (A .snd .fst) - ≡⟨ fromPathP (funTypeTransp (λ _ → ⟨ R ⟩) ⟨_⟩ p (A .snd .fst)) ⟩ - subst ⟨_⟩ p ∘ A .snd .fst ∘ subst (λ _ → ⟨ R ⟩) (sym p) - ≡⟨ cong ((subst ⟨_⟩ p ∘ A .snd .fst) ∘_) (funExt (λ _ → transportRefl _)) ⟩ - (pathToEquiv $ cong (λ r → fst r) p) .fst ∘ A .snd .fst - ≡⟨ q ⟩ - fst (B .snd) ∎) - CommAlgebraEquiv : (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'') → Type _ CommAlgebraEquiv A B = Σ[ f ∈ CommRingEquiv (A .fst) (B .fst) ] (f .fst .fst , f .snd) ∘cr A .snd ≡ B .snd @@ -109,6 +91,14 @@ module _ {R : CommRing ℓ} where (CommRingEquivs.CommRingEquiv≡ p) where open CommRingStr (B .fst .snd) using () renaming (is-set to isSetB) + isSetCommAlgebraEquiv : (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'') + → isSet (CommAlgebraEquiv A B) + isSetCommAlgebraEquiv A B = + isSetΣSndProp + (isSetCommRingEquiv _ _) + (λ e → isSetΣSndProp (isSet→ isSetB) (λ _ → isPropIsCommRingHom _ _ _) _ _) + where open CommRingStr (B .fst .snd) using () renaming (is-set to isSetB) + module CommAlgebraStr (A : CommAlgebra R ℓ') where open CommRingStr {{...}} instance diff --git a/Cubical/Algebra/CommAlgebraAlt/Univalence.agda b/Cubical/Algebra/CommAlgebraAlt/Univalence.agda index 0e595efab..7095418b0 100644 --- a/Cubical/Algebra/CommAlgebraAlt/Univalence.agda +++ b/Cubical/Algebra/CommAlgebraAlt/Univalence.agda @@ -7,6 +7,8 @@ open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Structure using (⟨_⟩) open import Cubical.Foundations.HLevels open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Transport +open import Cubical.Foundations.Path open import Cubical.Data.Sigma @@ -19,38 +21,34 @@ private ℓ ℓ' ℓ'' : Level -module _ (R : CommRing ℓ) where - private - to : (A B : CommAlgebra R ℓ') → CommAlgebraEquiv A B → A ≡ B - to A B e = CommAlgebra≡ - r≡ - ((pathToEquiv $ cong fst r≡) .fst ∘ A .snd .fst - ≡⟨ cong (_∘ A .snd .fst) (cong fst $ pathToEquiv-ua (e .fst .fst) ) ⟩ - CommAlgebraEquiv→CommRingHom e .fst ∘ A .snd .fst - ≡⟨ cong fst (e .snd) ⟩ - B .snd .fst ∎) - where r≡ : (A .fst) ≡ (B .fst) - r≡ = CommRingPath (A .fst) (B .fst) .fst (e .fst) - - test : (A : CommAlgebra R ℓ') → to A A (idCAlgEquiv A) ≡ refl - test A = {!to A A (idCAlgEquiv A)!} ≡⟨ {!!} ⟩ ? ≡⟨ {!!} ⟩ refl ∎ - - toIsEquiv : (A : CommAlgebra R ℓ') {B' : CommAlgebra R ℓ'} → (p : A ≡ B') → isContr (fiber (to A B') p) - toIsEquiv A = - J (λ B' A≡B' → isContr (fiber (to A B') A≡B')) - ((idCAlgEquiv A , {!test A!}) , - λ {(e , toe≡refl) → {!!}}) - - CommAlgebraPath : (A B : CommAlgebra R ℓ') → (CommAlgebraEquiv A B) ≃ (A ≡ B) - CommAlgebraPath {ℓ' = ℓ'} A B = to A B , {!!} - -{- -CommAlgebraPath : (R : CommRing ℓ) → (A B : CommAlgebra R ℓ') → (CommAlgebraEquiv A B) ≃ (A ≡ B) -CommAlgebraPath R = ∫ (𝒮ᴰ-CommAlgebra R) .UARel.ua +CommAlgebraPath : + (R : CommRing ℓ) + (A B : CommAlgebra R ℓ') + → (Σ[ f ∈ CommRingEquiv (A .fst) (B .fst) ] (f .fst .fst , f .snd) ∘cr A .snd ≡ B .snd) + ≃ (A ≡ B) +CommAlgebraPath R A B = + (Σ-cong-equiv + (CommRingPath _ _) + (λ e → compPathlEquiv (computeSubst e))) + ∙ₑ ΣPathTransport≃PathΣ A B + where computeSubst : + (e : CommRingEquiv (fst A) (fst B)) + → subst (CommRingHom R) (uaCommRing e) (A .snd) + ≡ (CommRingEquiv→CommRingHom e) ∘cr A .snd + computeSubst e = + CommRingHom≡ $ + (subst (CommRingHom R) (uaCommRing e) (A .snd)) .fst + ≡⟨ sym (substCommSlice (CommRingHom R) (λ X → ⟨ R ⟩ → ⟨ X ⟩) (λ _ → fst) (uaCommRing e) (A .snd)) ⟩ + subst (λ X → ⟨ R ⟩ → ⟨ X ⟩) (uaCommRing e) (A .snd .fst) + ≡⟨ fromPathP (funTypeTransp (λ _ → ⟨ R ⟩) ⟨_⟩ (uaCommRing e) (A .snd .fst)) ⟩ + subst ⟨_⟩ (uaCommRing e) ∘ A .snd .fst ∘ subst (λ _ → ⟨ R ⟩) (sym (uaCommRing e)) + ≡⟨ cong ((subst ⟨_⟩ (uaCommRing e) ∘ A .snd .fst) ∘_) (funExt (λ _ → transportRefl _)) ⟩ + (subst ⟨_⟩ (uaCommRing e) ∘ (A .snd .fst)) + ≡⟨ funExt (λ _ → uaβ (e .fst) _) ⟩ + (CommRingEquiv→CommRingHom e ∘cr A .snd) .fst ∎ uaCommAlgebra : {R : CommRing ℓ} {A B : CommAlgebra R ℓ'} → CommAlgebraEquiv A B → A ≡ B uaCommAlgebra {R = R} {A = A} {B = B} = equivFun (CommAlgebraPath R A B) isGroupoidCommAlgebra : {R : CommRing ℓ} → isGroupoid (CommAlgebra R ℓ') -isGroupoidCommAlgebra A B = isOfHLevelRespectEquiv 2 (CommAlgebraPath _ _ _) (isSetAlgebraEquiv _ _) --} +isGroupoidCommAlgebra A B = isOfHLevelRespectEquiv 2 (CommAlgebraPath _ _ _) (isSetCommAlgebraEquiv _ _)