CommAlgebras as CommRingHoms (#1145)

* move univalence code

* start...

* boilerplate

* fix auto-univalence

* fix FreeCommAlg

* fix subalgebra

* fix FPAlgebra

* copy Evans approach for Groups

* refactor

* refactor

* no-eta for algebra structures

* opaque quotients, fix unicity

* fast tc for quotient comm rings

* uniform indentation

* cleanup /remove flag

* improve names

* clean up

* WIP: deactivate problematic code

* refactor/simplify

* WIP

* start with stuff on the new comm alg

* Revert "Auxiliary commit to revert individual files from c5e74aa"

This reverts commit cea8a34f6ab8876640fad0a558743f1499fa15c5.

* Quotients

* update comm ring hom interface

* more boilerplate

* kernels

* syntax for new algebras

* more on comm ring quotients

* fix

* algebra quotients

* more opaque definitions, more use of set-level equalities

* commRingHom fixes

* unit comm algebra

* quotients

* no-eta for the equations of a ring

* WIP: Univalence

* equality characterization with help from Evan

* WIP

* typevariate polynomials as comm ring

* polynomials as comm algebra

* remove opaque structure again

the idea is, that it might be not worth the effort and the isRing part is still
'opaque' due to the no-eta-equality of isRing.

* Revert "WIP: deactivate problematic code"

This reverts commit d7192ee.

* make one example more meaningful

* univalence for comm algebras with Evans help

* various fixes, continue with typevariate polynomials

* induce a com ring hom

* Comm ring of polynomials on a general variable type and its universal property

* improve interface

* more interface, more opaque

* fix

* start with localization, fixes, more opaque things

* make ring quotients' isRing opaque instead of no-eta

* update to new interface for comm ring homs

* update to new interface for comm ring homs

* stub for polynomials, fix

* finish localization

* start with OnCoproduct, change default notation for R[I]

* universal property of polynomials as rings

* move old CommAlgebra

* category structure

* fix ref

* fix/move algebra as module

* refs

* remove old CommAlgebra.agda, move all refs

* fix

* make the new CommAlgebra the default

* remove no-eta for structure

* start with fp algebras

* small additions

* WIP: start with FP algebra examples

* change def, fix thinghs

* fix localization, adapt univalence, rearrange base

* fix quotients

* fix

* fix

* solver examples with new comm algebras

* fix

* more boilterplate, morphism contructor

* polynomial ring is fp

* add more calcualtions

* port initial algebra

* fix comment

* WIP

* WIP

* flatten

* universal property of fp algebras

* more fp algebras

* use name "terminal" instead of "unit"

* terminal R-algebra is fp, notation

* finite choice for FinData Fin

* minor changes

* refactor

* WIP

* reduce problem

* reduce problem

* Revert "reduce problem"

This reverts commit 7c1e4d1.

* Revert "reduce problem"

This reverts commit c00ec56.

* refactor QuotientAlgebra

* proof on 0Ideal and imageIdeal

* add important remark (would have saved me time)

* remove superfluous opaqueness

* boilerplate

* fix terminology

* lemma on quotients

* make checkable

* missed ref

* hom linear combination

* iamges of fgIdeals

* comment

* boilerplate

* itereted quotients for CommAlgebras

* iterated fg ideal quotients

* add lemma on quotients

* fp quotients

* remove obsoleted

* maek dependency on old CommAlgebra explicit

Author: felixwellen

Cubical/Algebra/Algebra/Base.agda

@@ -10,11 +10,6 @@ open import Cubical.Foundations.SIP
 
 open import Cubical.Data.Sigma
 
-open import Cubical.Displayed.Base
-open import Cubical.Displayed.Auto
-open import Cubical.Displayed.Record
-open import Cubical.Displayed.Universe
-
 open import Cubical.Reflection.RecordEquiv
 
 open import Cubical.Algebra.Monoid
@@ -36,7 +31,7 @@ record IsAlgebra (R : Ring ℓ) {A : Type ℓ'}
                  (0a 1a : A) (_+_ _·_ : A → A → A) (-_ : A → A)
                  (_⋆_ : ⟨ R ⟩ → A → A) : Type (ℓ-max ℓ ℓ') where
 
-  constructor isalgebra
+  no-eta-equality
 
   open RingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·r_)
 
@@ -59,8 +54,6 @@ unquoteDecl IsAlgebraIsoΣ = declareRecordIsoΣ IsAlgebraIsoΣ (quote IsAlgebra)
 
 record AlgebraStr (R : Ring ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where
 
-  constructor algebrastr
-
   field
     0a             : A
     1a             : A
@@ -72,6 +65,8 @@ record AlgebraStr (R : Ring ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where
 
   open IsAlgebra isAlgebra public
 
+unquoteDecl AlgebraStrIsoΣ = declareRecordIsoΣ AlgebraStrIsoΣ (quote AlgebraStr)
+
 Algebra : (R : Ring ℓ) → ∀ ℓ' → Type (ℓ-max ℓ (ℓ-suc ℓ'))
 Algebra R ℓ' = Σ[ A ∈ Type ℓ' ] AlgebraStr R A
 
@@ -208,13 +203,15 @@ isPropIsAlgebra R _ _ _ _ _ _ = let open IsLeftModule in
 isPropIsAlgebraHom : (R : Ring ℓ) {A : Type ℓ'} {B : Type ℓ''}
                      (AS : AlgebraStr R A) (f : A → B) (BS : AlgebraStr R B)
                    → isProp (IsAlgebraHom AS f BS)
-isPropIsAlgebraHom R AS f BS = isOfHLevelRetractFromIso 1 IsAlgebraHomIsoΣ
-                               (isProp×5 (is-set _ _)
-                                         (is-set _ _)
-                                         (isPropΠ2 λ _ _ → is-set _ _)
-                                         (isPropΠ2 λ _ _ → is-set _ _)
-                                         (isPropΠ λ _ → is-set _ _)
-                                         (isPropΠ2 λ _ _ → is-set _ _))
+isPropIsAlgebraHom R AS f BS =
+  isOfHLevelRetractFromIso 1
+    IsAlgebraHomIsoΣ
+    (isProp×5 (is-set _ _)
+              (is-set _ _)
+              (isPropΠ2 λ _ _ → is-set _ _)
+              (isPropΠ2 λ _ _ → is-set _ _)
+              (isPropΠ λ _ → is-set _ _)
+              (isPropΠ2 λ _ _ → is-set _ _))
   where
   open AlgebraStr BS
 
@@ -237,33 +234,6 @@ isSetAlgebraEquiv M N = isSetΣ (isOfHLevel≃ 2 M.is-set N.is-set)
 AlgebraHom≡ : {φ ψ : AlgebraHom A B} → fst φ ≡ fst ψ → φ ≡ ψ
 AlgebraHom≡ = Σ≡Prop λ f → isPropIsAlgebraHom _ _ f _
 
-𝒮ᴰ-Algebra : (R : Ring ℓ) → DUARel (𝒮-Univ ℓ') (AlgebraStr R) (ℓ-max ℓ ℓ')
-𝒮ᴰ-Algebra R =
-  𝒮ᴰ-Record (𝒮-Univ _) (IsAlgebraEquiv {R = R})
-    (fields:
-      data[ 0a ∣ nul ∣ pres0 ]
-      data[ 1a ∣ nul ∣ pres1 ]
-      data[ _+_ ∣ bin ∣ pres+ ]
-      data[ _·_ ∣ bin ∣ pres· ]
-      data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
-      data[ _⋆_ ∣ autoDUARel _ _ ∣ pres⋆ ]
-      prop[ isAlgebra ∣ (λ _ _ → isPropIsAlgebra _ _ _ _ _ _ _) ])
-  where
-  open AlgebraStr
-
-  -- faster with some sharing
-  nul = autoDUARel (𝒮-Univ _) (λ A → A)
-  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)
-
-AlgebraPath : (A B : Algebra R ℓ') → (AlgebraEquiv A B) ≃ (A ≡ B)
-AlgebraPath {R = R} = ∫ (𝒮ᴰ-Algebra R) .UARel.ua
-
-uaAlgebra : AlgebraEquiv A B → A ≡ B
-uaAlgebra {A = A} {B = B} = equivFun (AlgebraPath A B)
-
-isGroupoidAlgebra : isGroupoid (Algebra R ℓ')
-isGroupoidAlgebra _ _ = isOfHLevelRespectEquiv 2 (AlgebraPath _ _) (isSetAlgebraEquiv _ _)
-
 -- Smart constructor for algebra homomorphisms
 -- that infers the other equations from pres1, pres+, pres·, and pres⋆
 

Cubical/Algebra/Algebra/Properties.agda

@@ -10,8 +10,7 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Path
 open import Cubical.Foundations.Transport
-open import Cubical.Foundations.Univalence
-open import Cubical.Foundations.SIP
+open import Cubical.Foundations.SIP using (⟨_⟩)
 
 open import Cubical.Data.Sigma
 
@@ -185,57 +184,15 @@ module AlgebraEquivs where
           (λ g → isPropIsAlgebraHom _ (B .snd) g (C .snd))
           (isoOnTypes .leftInv (g .fst))
 
--- the Algebra version of uaCompEquiv
-module AlgebraUAFunctoriality where
- open AlgebraStr
- open AlgebraEquivs
-
- Algebra≡ : (A B : Algebra R ℓ') → (
-   Σ[ p ∈ ⟨ A ⟩ ≡ ⟨ B ⟩ ]
-   Σ[ q0 ∈ PathP (λ i → p i) (0a (snd A)) (0a (snd B)) ]
-   Σ[ q1 ∈ PathP (λ i → p i) (1a (snd A)) (1a (snd B)) ]
-   Σ[ r+ ∈ PathP (λ i → p i → p i → p i) (_+_ (snd A)) (_+_ (snd B)) ]
-   Σ[ r· ∈ PathP (λ i → p i → p i → p i) (_·_ (snd A)) (_·_ (snd B)) ]
-   Σ[ s- ∈ PathP (λ i → p i → p i) (-_ (snd A)) (-_ (snd B)) ]
-   Σ[ s⋆ ∈ PathP (λ i → ⟨ R ⟩ → p i → p i) (_⋆_ (snd A)) (_⋆_ (snd B)) ]
-   PathP (λ i → IsAlgebra R (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i)) (isAlgebra (snd A))
-                                                                     (isAlgebra (snd B)))
-   ≃ (A ≡ B)
- Algebra≡ A B = isoToEquiv theIso
-   where
-   open Iso
-   theIso : Iso _ _
-   fun theIso (p , q0 , q1 , r+ , r· , s- , s⋆ , t) i = p i
-                 , algebrastr (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i) (t i)
-   inv theIso x = cong ⟨_⟩ x , cong (0a ∘ snd) x , cong (1a ∘ snd) x
-                , cong (_+_ ∘ snd) x , cong (_·_ ∘ snd) x , cong (-_ ∘ snd) x , cong (_⋆_ ∘ snd) x
-                , cong (isAlgebra ∘ snd) x
-   rightInv theIso _ = refl
-   leftInv theIso _ = refl
-
- caracAlgebra≡ : (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
- caracAlgebra≡ {A = A} {B = B} p q P =
-   sym (transportTransport⁻ (ua (Algebra≡ A B)) p)
-                                    ∙∙ cong (transport (ua (Algebra≡ A B))) helper
-                                    ∙∙ transportTransport⁻ (ua (Algebra≡ A B)) q
-     where
-     helper : transport (sym (ua (Algebra≡ A B))) p ≡ transport (sym (ua (Algebra≡ A B))) q
-     helper = Σ≡Prop
-                (λ _ → isPropΣ
-                          (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
-                          λ _ → isOfHLevelPathP 1 (isPropIsAlgebra _ _ _ _ _ _ _) _ _)
-               (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))
-
- uaCompAlgebraEquiv : (f : AlgebraEquiv A B) (g : AlgebraEquiv B C)
-                  → uaAlgebra (compAlgebraEquiv f g) ≡ uaAlgebra f ∙ uaAlgebra g
- uaCompAlgebraEquiv f g = caracAlgebra≡ _ _ (
-   cong ⟨_⟩ (uaAlgebra (compAlgebraEquiv f g))
-     ≡⟨ uaCompEquiv _ _ ⟩
-   cong ⟨_⟩ (uaAlgebra f) ∙ cong ⟨_⟩ (uaAlgebra g)
-     ≡⟨ sym (cong-∙ ⟨_⟩ (uaAlgebra f) (uaAlgebra g)) ⟩
-   cong ⟨_⟩ (uaAlgebra f ∙ uaAlgebra g) ∎)
+isSetAlgebraStr : (A : Type ℓ') → isSet (AlgebraStr R A)
+isSetAlgebraStr A =
+  let open AlgebraStr
+  in isOfHLevelSucIfInhabited→isOfHLevelSuc 1 λ str →
+  isOfHLevelRetractFromIso 2 AlgebraStrIsoΣ $
+  isSetΣ (str .is-set) λ _ →
+  isSetΣ (str .is-set) λ _ →
+  isSetΣ (isSet→ (isSet→ (str .is-set))) λ _ →
+  isSetΣ (isSet→ (isSet→ (str .is-set))) λ _ →
+  isSetΣ (isSet→ (str .is-set)) (λ _ →
+  isSetΣSndProp (isSet→ (isSet→ (str .is-set))) λ _ →
+  isPropIsAlgebra _ _ _ _ _ _ _)

Cubical/Algebra/Algebra/Univalence.agda

@@ -0,0 +1,86 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Algebra.Univalence where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.SIP
+
+open import Cubical.Functions.Embedding
+
+open import Cubical.Data.Sigma
+
+open import Cubical.Displayed.Base
+open import Cubical.Displayed.Auto
+open import Cubical.Displayed.Record
+open import Cubical.Displayed.Universe
+
+open import Cubical.Algebra.Ring.Base
+open import Cubical.Algebra.Algebra.Base
+open import Cubical.Algebra.Algebra.Properties
+
+private
+  variable
+    ℓ ℓ' ℓ'' ℓ''' : Level
+    R : Ring ℓ
+    A B C D : Algebra R ℓ
+
+open IsAlgebraHom
+
+𝒮ᴰ-Algebra : (R : Ring ℓ) → DUARel (𝒮-Univ ℓ') (AlgebraStr R) (ℓ-max ℓ ℓ')
+𝒮ᴰ-Algebra R =
+  𝒮ᴰ-Record (𝒮-Univ _) (IsAlgebraEquiv {R = R})
+    (fields:
+      data[ 0a ∣ nul ∣ pres0 ]
+      data[ 1a ∣ nul ∣ pres1 ]
+      data[ _+_ ∣ bin ∣ pres+ ]
+      data[ _·_ ∣ bin ∣ pres· ]
+      data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
+      data[ _⋆_ ∣ autoDUARel _ _ ∣ pres⋆ ]
+      prop[ isAlgebra ∣ (λ A ΣA →
+                          isPropIsAlgebra
+                            R
+                            (snd (fst (fst (fst (fst (fst ΣA))))))
+                            (snd (fst (fst (fst (fst ΣA)))))
+                            (snd (fst (fst (fst ΣA))))
+                            (snd (fst (fst ΣA)))
+                            (snd (fst ΣA))
+                            (snd ΣA))  ])
+  where
+  open AlgebraStr
+
+  -- faster with some sharing
+  nul = autoDUARel (𝒮-Univ _) (λ A → A)
+  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)
+
+AlgebraPath : (A B : Algebra R ℓ') → (AlgebraEquiv A B) ≃ (A ≡ B)
+AlgebraPath {R = R} = ∫ (𝒮ᴰ-Algebra R) .UARel.ua
+
+uaAlgebra : AlgebraEquiv A B → A ≡ B
+uaAlgebra {A = A} {B = B} = equivFun (AlgebraPath A B)
+
+isGroupoidAlgebra : isGroupoid (Algebra R ℓ')
+isGroupoidAlgebra _ _ = isOfHLevelRespectEquiv 2 (AlgebraPath _ _) (isSetAlgebraEquiv _ _)
+
+-- the Algebra version of uaCompEquiv
+module AlgebraUAFunctoriality where
+ open AlgebraStr
+ open AlgebraEquivs
+
+ caracAlgebra≡ : (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
+ caracAlgebra≡ _ _ α =
+   isEmbedding→Inj (iso→isEmbedding (invIso ΣPathIsoPathΣ)) _ _ $
+   Σ≡Prop (λ _ → isOfHLevelPathP' 1 (isSetAlgebraStr _) _ _) α
+
+ uaCompAlgebraEquiv : (f : AlgebraEquiv A B) (g : AlgebraEquiv B C)
+                  → uaAlgebra (compAlgebraEquiv f g) ≡ uaAlgebra f ∙ uaAlgebra g
+ uaCompAlgebraEquiv f g = caracAlgebra≡ _ _ (
+   cong ⟨_⟩ (uaAlgebra (compAlgebraEquiv f g))
+     ≡⟨ uaCompEquiv _ _ ⟩
+   cong ⟨_⟩ (uaAlgebra f) ∙ cong ⟨_⟩ (uaAlgebra g)
+     ≡⟨ sym (cong-∙ ⟨_⟩ (uaAlgebra f) (uaAlgebra g)) ⟩
+   cong ⟨_⟩ (uaAlgebra f ∙ uaAlgebra g) ∎)

Cubical/Algebra/CommAlgebra/AsModule.agda

@@ -0,0 +1,5 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommAlgebra.AsModule where
+
+open import Cubical.Algebra.CommAlgebra.AsModule.Base public
+open import Cubical.Algebra.CommAlgebra.AsModule.Properties public