Initial Boolean Algebra (#1239)

* moved Initial Boolean algebra to new branch

* Added Boolean maps

* used copattern-matching for idemCommRing->BR

* BoolBRStr now uses copattern-matching

* moved BoolBR and BoolCR to instances of CommRing and BooleanRing
repsectively

* Renamed BooleanStr to BooleanRingStr

* use copattern matching for BooleanRingStr->CommRingStr

Author: Freek98

Cubical/Algebra/BooleanRing/Base.agda

@@ -23,7 +23,7 @@ record IsBooleanRing {B : Type ℓ}
 
   open IsCommRing isCommRing public
 
-record BooleanStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
+record BooleanRingStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
   field
     𝟘          : A
     𝟙          : A
@@ -39,22 +39,49 @@ record BooleanStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
   open IsBooleanRing isBooleanRing public
 
 BooleanRing : ∀ ℓ → Type (ℓ-suc ℓ)
-BooleanRing ℓ = TypeWithStr ℓ BooleanStr
-
-BooleanStr→CommRingStr : { A : Type ℓ } →  BooleanStr A  → CommRingStr A
-BooleanStr→CommRingStr x = record { isCommRing = IsBooleanRing.isCommRing (BooleanStr.isBooleanRing x) }
+BooleanRing ℓ = TypeWithStr ℓ BooleanRingStr
+
+module _ {A : Type ℓ} (BRStr : BooleanRingStr A) where
+  open CommRingStr
+  open BooleanRingStr( BRStr)
+  BooleanRingStr→CommRingStr : CommRingStr A
+  0r  BooleanRingStr→CommRingStr = _
+  1r  BooleanRingStr→CommRingStr = _
+  _+_ BooleanRingStr→CommRingStr = _
+  _·_ BooleanRingStr→CommRingStr = _
+  -   BooleanRingStr→CommRingStr = _
+  isCommRing BooleanRingStr→CommRingStr = isCommRing BRStr
 
 BooleanRing→CommRing : BooleanRing ℓ → CommRing ℓ
-BooleanRing→CommRing (carrier , structure ) = carrier , BooleanStr→CommRingStr structure
+BooleanRing→CommRing (carrier , structure ) = carrier , BooleanRingStr→CommRingStr structure
 
-BooleanStr→RingStr : { A : Type ℓ } → BooleanStr A → RingStr A
-BooleanStr→RingStr S = CommRingStr→RingStr (BooleanStr→CommRingStr S)
+BooleanRingStr→RingStr : { A : Type ℓ } → BooleanRingStr A → RingStr A
+BooleanRingStr→RingStr S = CommRingStr→RingStr (BooleanRingStr→CommRingStr S)
 
 BooleanRing→Ring : BooleanRing ℓ → Ring ℓ
-BooleanRing→Ring (carrier , structure ) = carrier , BooleanStr→RingStr structure
+BooleanRing→Ring (carrier , structure ) = carrier , BooleanRingStr→RingStr structure
+
+isIdemRing : {ℓ : Level} → CommRing ℓ → Type ℓ
+isIdemRing R = ∀ (r : ⟨ R ⟩) → (str R) .CommRingStr._·_ r r ≡ r
+
+module _ {ℓ : Level} (R : CommRing ℓ) (idem : isIdemRing R) where
+  open BooleanRingStr
+  open IsBooleanRing
+  idemCommRing→BR : BooleanRing ℓ
+  fst idemCommRing→BR = ⟨ R ⟩
+  𝟘 (snd idemCommRing→BR)   = _
+  𝟙 (snd idemCommRing→BR)   = _
+  _+_ (snd idemCommRing→BR) = _
+  _·_ (snd idemCommRing→BR) = _
+  - snd idemCommRing→BR     = _
+  isCommRing (isBooleanRing (snd idemCommRing→BR)) = (str R) .CommRingStr.isCommRing
+  ·Idem (isBooleanRing (snd idemCommRing→BR))      = idem
+
+BoolHom : {ℓ ℓ' : Level} → (A : BooleanRing ℓ) → (B : BooleanRing ℓ') → Type _
+BoolHom A B = CommRingHom (BooleanRing→CommRing A) (BooleanRing→CommRing B)
 
 module BooleanAlgebraStr (A : BooleanRing ℓ)  where
-  open BooleanStr (A . snd)
+  open BooleanRingStr (A . snd)
   _∨_ : ⟨ A ⟩ → ⟨ A ⟩ → ⟨ A ⟩
   a ∨ b = (a + b) + (a · b)
   _∧_ : ⟨ A ⟩ → ⟨ A ⟩ → ⟨ A ⟩
@@ -257,3 +284,4 @@ module BooleanAlgebraStr (A : BooleanRing ℓ)  where
     ((𝟙 + x)  + (𝟙 + x)) + (y + y)  + 𝟙 + x · y
       ≡⟨ solve! (BooleanRing→CommRing A) ⟩
     ¬ x ∨ ¬ y ∎
+

Cubical/Algebra/BooleanRing/Initial.agda

@@ -0,0 +1,50 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.BooleanRing.Initial where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Function
+
+open import Cubical.Algebra.BooleanRing.Base
+open import Cubical.Data.Bool renaming (elim to bool-ind)
+open import Cubical.Algebra.CommRing
+open import Cubical.Tactics.CommRingSolver
+
+open import Cubical.Algebra.BooleanRing.Instances.Bool
+open import Cubical.Algebra.CommRing.Instances.Bool
+
+module _ {ℓ : Level} (B : BooleanRing ℓ) where
+  private
+    B' = BooleanRing→CommRing B
+
+  open CommRingStr (snd B')
+  open BooleanAlgebraStr B
+  open IsCommRingHom
+
+  BoolBR→BAMap : Bool → ⟨ B ⟩
+  BoolBR→BAMap = bool-ind 1r 0r
+
+  BoolBR→BAIsCommRingHom : IsCommRingHom (snd BoolCR) BoolBR→BAMap (snd B')
+  pres0 BoolBR→BAIsCommRingHom = refl
+  pres1 BoolBR→BAIsCommRingHom = refl
+  pres+ BoolBR→BAIsCommRingHom =
+    λ { false false → solve! B'
+    ; false true  → solve! B'
+    ; true  false → solve! B'
+    ; true  true  → sym characteristic2
+    }
+  pres· BoolBR→BAIsCommRingHom =
+    λ { false false → solve! B'
+    ; false true  → solve! B'
+    ; true  false → solve! B'
+    ; true  true  → solve! B'
+    }
+  pres- BoolBR→BAIsCommRingHom false = solve! B'
+  pres- BoolBR→BAIsCommRingHom true  = -IsId :> 1r ≡ - 1r
+
+  BoolBR→ : BoolHom BoolBR B
+  BoolBR→ = BoolBR→BAMap , BoolBR→BAIsCommRingHom
+
+  BoolBR→IsUnique : (f : BoolHom BoolBR B) → (fst f) ≡ fst (BoolBR→)
+  BoolBR→IsUnique f =  funExt (bool-ind (pres1 (snd f)) (pres0 (snd f)))

Cubical/Algebra/BooleanRing/Instances/Bool.agda

@@ -0,0 +1,28 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.BooleanRing.Instances.Bool where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Algebra.BooleanRing.Base
+open import Cubical.Data.Bool renaming (elim to bool-ind)
+open import Cubical.Algebra.CommRing
+
+open BooleanRingStr
+open IsBooleanRing
+
+BoolBRStr : BooleanRingStr Bool
+𝟘 BoolBRStr   = false
+𝟙 BoolBRStr   = true
+_+_ BoolBRStr = _⊕_
+_·_ BoolBRStr = _and_
+- BoolBRStr   = λ x → x
+isCommRing (isBooleanRing BoolBRStr) = makeIsCommRing
+  isSetBool ⊕-assoc ⊕-identityʳ
+  (bool-ind refl refl) ⊕-comm and-assoc
+  and-identityʳ (bool-ind (λ _ _ → refl)
+  (λ _ _ → refl)) and-comm
+·Idem (isBooleanRing BoolBRStr) = bool-ind refl refl
+
+BoolBR : BooleanRing ℓ-zero
+BoolBR = Bool , BoolBRStr
+

Cubical/Algebra/CommRing/Instances/Bool.agda

@@ -0,0 +1,12 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Algebra.CommRing.Instances.Bool where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Algebra.BooleanRing.Base
+open import Cubical.Algebra.CommRing
+
+open import Cubical.Algebra.BooleanRing.Instances.Bool
+
+BoolCR : CommRing ℓ-zero
+BoolCR = BooleanRing→CommRing BoolBR