Algebra structures without eta

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,7 +54,7 @@ unquoteDecl IsAlgebraIsoΣ = declareRecordIsoΣ IsAlgebraIsoΣ (quote IsAlgebra)
 
 record AlgebraStr (R : Ring ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where
 
-  constructor algebrastr
+  no-eta-equality
 
   field
     0a             : A
@@ -72,6 +67,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 +205,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 +236,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/Subalgebra.agda

@@ -30,7 +30,8 @@ module _ (S : Subalgebra) where
             (CommAlgebraStr.·Comm (snd A) (fst x) (fst y)))}
 
   Subalgebra→CommAlgebraHom : CommAlgebraHom Subalgebra→CommAlgebra A
-  Subalgebra→CommAlgebraHom = Subalgebra→AlgebraHom S
+  fst Subalgebra→CommAlgebraHom = Subalgebra→AlgebraHom S .fst
+  snd Subalgebra→CommAlgebraHom = record { IsAlgebraHom (Subalgebra→AlgebraHom S .snd) }
 
   SubalgebraHom : (B : CommAlgebra R ℓ') (f : CommAlgebraHom B A)
                 → ((b : ⟨ B ⟩) → fst f b ∈ fst S)