Upper natural numbers

Cubical/Algebra/CommMonoid/Base.agda

@@ -83,6 +83,18 @@ CommMonoidStr→MonoidStr (commmonoidstr _ _ H) = monoidstr _ _ (IsCommMonoid.is
 CommMonoid→Monoid : CommMonoid ℓ → Monoid ℓ
 CommMonoid→Monoid (_ , commmonoidstr  _ _ M) = _ , monoidstr _ _ (IsCommMonoid.isMonoid M)
 
+isSetFromIsCommMonoid :
+  {M : Type ℓ} {ε : M} {_·_ : M → M → M}
+  (isCommMonoid : IsCommMonoid ε _·_)
+  → isSet M
+isSetFromIsCommMonoid isCommMonoid =
+  isSetFromIsMonoid (MonoidStr.isMonoid (CommMonoidStr→MonoidStr (commmonoidstr _ _ isCommMonoid)))
+
+isSetCommMonoid : (M : CommMonoid ℓ) → isSet ⟨ M ⟩
+isSetCommMonoid M =
+  let open CommMonoidStr (snd M)
+  in isSetFromIsCommMonoid isCommMonoid
+
 CommMonoidHom : (L : CommMonoid ℓ) (M : CommMonoid ℓ') → Type (ℓ-max ℓ ℓ')
 CommMonoidHom L M = MonoidHom (CommMonoid→Monoid L) (CommMonoid→Monoid M)
 

Cubical/Algebra/CommMonoid/Properties.agda

@@ -21,7 +21,33 @@ open import Cubical.Algebra.CommMonoid.Base
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' : Level
+
+module _
+    (M : CommMonoid ℓ)
+    (P : ⟨ M ⟩ → hProp ℓ')
+    where
+  open CommMonoidStr (snd M)
+  module _
+    (·Closed : (x y : ⟨ M ⟩) → ⟨ P x ⟩ → ⟨ P y ⟩ → ⟨ P (x · y) ⟩)
+    (εContained : ⟨ P ε ⟩)
+    where
+    private
+      subtype = Σ[ x ∈ ⟨ M ⟩ ] ⟨ P x ⟩
+
+    makeSubCommMonoid : CommMonoid _
+    fst makeSubCommMonoid = subtype
+    CommMonoidStr.ε (snd makeSubCommMonoid) = ε , εContained
+    CommMonoidStr._·_ (snd makeSubCommMonoid) (x , xContained) (y , yContained) =
+      (x · y) , ·Closed x y xContained yContained
+    IsCommMonoid.isMonoid (CommMonoidStr.isCommMonoid (snd makeSubCommMonoid)) =
+      makeIsMonoid
+        (isOfHLevelΣ 2 (isSetFromIsCommMonoid isCommMonoid) λ _ → isProp→isSet (snd (P _)))
+        (λ x y z → Σ≡Prop (λ _ → snd (P _)) (assoc (fst x) (fst y) (fst z)))
+        (λ x → Σ≡Prop (λ _ → snd (P _)) (rid (fst x)))
+        λ x → Σ≡Prop (λ _ → snd (P _)) (lid (fst x))
+    IsCommMonoid.comm (CommMonoidStr.isCommMonoid (snd makeSubCommMonoid)) =
+      λ x y → Σ≡Prop (λ _ → snd (P _)) (comm (fst x) (fst y))
 
 module CommMonoidTheory (M' : CommMonoid ℓ) where
  open CommMonoidStr (snd M')

Cubical/Algebra/CommSemiring.agda

@@ -0,0 +1,4 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommSemiring where
+
+open import Cubical.Algebra.CommSemiring.Base public

Cubical/Algebra/CommSemiring/Base.agda

@@ -0,0 +1,60 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommSemiring.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.SIP
+
+open import Cubical.Algebra.CommMonoid
+open import Cubical.Algebra.Monoid
+
+private
+  variable
+    ℓ ℓ' : Level
+
+record IsCommSemiring {R : Type ℓ}
+                  (0r 1r : R) (_+_ _·_ : R → R → R) : Type ℓ where
+
+  field
+    +IsCommMonoid  : IsCommMonoid 0r _+_
+    ·IsCommMonoid  : IsCommMonoid 1r _·_
+    ·LDist+        : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
+    0LAnnihil      : (x : R) → 0r · x ≡ 0r
+
+  open IsCommMonoid +IsCommMonoid public
+    renaming
+      ( assoc       to +Assoc
+      ; identity    to +Identity
+      ; lid         to +Lid
+      ; rid         to +Rid
+      ; comm        to +Comm
+      ; isSemigroup to +IsSemigroup
+      ; isMonoid    to +IsMonoid)
+
+  open IsCommMonoid ·IsCommMonoid public
+    renaming
+      ( assoc       to ·Assoc
+      ; identity    to ·Identity
+      ; lid         to ·Lid
+      ; rid         to ·Rid
+      ; comm        to ·Comm
+      ; isSemigroup to ·IsSemigroup
+      ; isMonoid    to ·IsMonoid)
+    hiding
+      ( is-set ) -- We only want to export one proof of this
+
+record CommSemiringStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
+
+  field
+    0r      : A
+    1r      : A
+    _+_     : A → A → A
+    _·_     : A → A → A
+    isCommSemiring  : IsCommSemiring 0r 1r _+_ _·_
+
+  infixl 7 _·_
+  infixl 6 _+_
+
+  open IsCommSemiring isCommSemiring public
+
+CommSemiring : ∀ ℓ → Type (ℓ-suc ℓ)
+CommSemiring ℓ = TypeWithStr ℓ CommSemiringStr

Cubical/Algebra/CommSemiring/Instances/UpperNat.agda

@@ -0,0 +1,205 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommSemiring.Instances.UpperNat where
+{-
+  based on:
+  https://github.com/DavidJaz/Cohesion/blob/master/UpperNaturals.agda
+
+  and the slides here (for arithmetic operation):
+  https://felix-cherubini.de/myers-slides-II.pdf
+-}
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Functions.Logic
+open import Cubical.Functions.Embedding
+
+open import Cubical.Algebra.CommMonoid
+open import Cubical.Algebra.OrderedCommMonoid
+open import Cubical.Algebra.OrderedCommMonoid.PropCompletion
+open import Cubical.Algebra.OrderedCommMonoid.Instances
+open import Cubical.Algebra.CommSemiring
+
+open import Cubical.Data.Nat using (ℕ; ·-distribˡ)
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Empty hiding (⊥)
+open import Cubical.Data.Sigma
+
+open import Cubical.HITs.Truncation
+open import Cubical.HITs.PropositionalTruncation renaming (rec to propTruncRec)
+
+private
+  variable
+    ℓ : Level
+
+{- The Upper Naturals
+   An upper natural is an upward closed proposition on natural numbers.
+   The interpretation is that an upper natural is a natural ``defined by its upper bounds'', in the
+   sense that for the proposition N holding of a natural n means that n is an upper bound of N.
+   The important bit about upper naturals is that they satisfy the well-ordering principle,
+   constructively (no proof of that is given here).
+
+   Example Application:
+   The degree of a polynomial P=∑_{i=0}^{n} aᵢ · Xⁱ may be defined as an upper natural:
+
+     deg(P) :≡ (λ n → all non-zero indices have index smaller n)
+
+     Or: deg(∑_{i=0}^{n} aᵢ · Xⁱ) = λ (k : ℕ) → ∀ (k+1 ≤ i ≤ n) aᵢ≡0
+
+   This works even if a constructive definition of polynomial is used.
+
+   However the upper naturals are a bit too unconstraint and do not even form a semiring,
+   since they include 'infinity' elements like the proposition that is always false.
+
+   This is different for the subtype of *bounded* upper naturals ℕ↑b.
+-}
+
+module ConstructionUnbounded where
+  ℕ↑-+ = PropCompletion ℕ≤+
+  ℕ↑-· = PropCompletion ℕ≤·
+
+  open OrderedCommMonoidStr (snd ℕ↑-+)
+    using ()
+    renaming (assoc to +Assoc; comm to +Comm; rid to +Rid;
+              _·_ to _+_; ε to 0↑)
+
+  open OrderedCommMonoidStr (snd ℕ≤·)
+   using (MonotoneL; MonotoneR)
+
+  open OrderedCommMonoidStr (snd ℕ≤+)
+   using ()
+   renaming (_·_ to _+ℕ_;
+             MonotoneL to +MonotoneL; MonotoneR to +MonotoneR;
+             comm to ℕ+Comm)
+
+  open OrderedCommMonoidStr ⦃...⦄
+    using (_·_)
+    renaming (assoc to ·Assoc; comm to ·Comm; rid to ·Rid)
+
+  private
+    instance
+      _ : OrderedCommMonoidStr _ _
+      _  = snd ℕ↑-·
+      _ : OrderedCommMonoidStr _ _
+      _ = snd ℕ≤·
+
+  ℕ↑ : Type₁
+  ℕ↑ = fst ℕ↑-+
+
+  open PropCompletion ℓ-zero ℕ≤+
+    using (typeAt; pathFromImplications)
+
+  open <-Reasoning using (_≤⟨_⟩_)
+
+  +LDist· : (x y z : ℕ↑) →
+            x · (y + z) ≡ (x · y) + (x · z)
+  +LDist· x y z =
+    pathFromImplications
+      (x · (y + z)) ((x · y) + (x · z))
+      (⇒) ⇐
+    where
+      ⇒ : (n : ℕ) → typeAt n (x · (y + z))  → typeAt n ((x · y) + (x · z))
+      ⇒ n = propTruncRec
+             isPropPropTrunc
+             λ {((a , b) , xa , (y+zb , a·b≤n)) →
+                 propTruncRec
+                   isPropPropTrunc
+                   (λ {((a' , b') , ya' , (zb' , a'+b'≤b))
+                     → ∣ ((a · a') , (a · b')) ,
+                          ∣ (a , a') , (xa , (ya' , ≤-refl)) ∣₁ ,
+                          (∣ (a , b') , (xa , (zb' , ≤-refl)) ∣₁ ,
+                          subst (_≤ n) (sym (·-distribˡ a a' b'))
+                            (≤-trans (MonotoneL {z = a} a'+b'≤b) a·b≤n)) ∣₁ })
+                   y+zb}
+      ⇐ : (n : ℕ) → _
+      ⇐ n =
+        propTruncRec
+          isPropPropTrunc
+          λ {((a , b) , x·ya , (x·zb , a+b≤n))
+          → propTruncRec
+              isPropPropTrunc
+              (λ {((a' , b') , a'x , (b'y , a'·b'≤a))
+              → propTruncRec
+                  isPropPropTrunc
+                  (λ {((a″ , b″) , a″x , (zb″ , a″·b″≤b))
+                  → ∣ ≤CaseInduction {n = a'} {m = a″}
+                        (λ a'≤a″ →
+                          (a' , (b' +ℕ b″)) , a'x ,
+
+                          (∣ (b' , b″) , (b'y , (zb″ , ≤-refl)) ∣₁ ,
+                           (a' · (b' +ℕ b″)       ≤⟨ subst
+                                                       (_≤ (a' · b') +ℕ (a' · b″))
+                                                       (·-distribˡ a' b' b″) ≤-refl ⟩
+                           (a' · b') +ℕ (a' · b″) ≤⟨ +MonotoneR a'·b'≤a ⟩
+                            a +ℕ (a' · b″)        ≤⟨ +MonotoneL
+                                                       (≤-trans (MonotoneR a'≤a″) a″·b″≤b) ⟩
+                            a+b≤n ))
+                        )
+                        (λ a″≤a' →
+                         (a″ , (b' +ℕ b″)) , (a″x ,
+                         (∣ (b' , b″) , (b'y , (zb″ , ≤-refl)) ∣₁ ,
+                           ((a″ · (b' +ℕ b″))      ≤⟨ subst
+                                                        (_≤ (a″ · b') +ℕ (a″ · b″))
+                                                        (·-distribˡ a″ b' b″) ≤-refl ⟩
+                            (a″ · b') +ℕ (a″ · b″) ≤⟨ +MonotoneR
+                                                        ((a″ · b') ≤⟨ MonotoneR a″≤a' ⟩ a'·b'≤a) ⟩
+                            a +ℕ (a″ · b″)         ≤⟨ +MonotoneL a″·b″≤b  ⟩
+                            a+b≤n)))
+                        )
+                    ∣₁})
+                  x·zb})
+              x·ya}
+
+
+module ConstructionBounded where
+  ℕ↑-+b = BoundedPropCompletion ℕ≤+
+  ℕ↑-·b = BoundedPropCompletion ℕ≤·
+
+  open OrderedCommMonoidStr (snd ℕ≤+)
+    using ()
+    renaming (_·_ to _+ℕ_;
+              MonotoneL to +MonotoneL; MonotoneR to +MonotoneR; rid to +Rid;
+              comm to ℕ+Comm)
+  open OrderedCommMonoidStr (snd ℕ↑-+b)
+    using ()
+    renaming (assoc to +Assoc; comm to +Comm;
+              _·_ to _+_; ε to 0↑)
+
+  open OrderedCommMonoidStr (snd ℕ↑-·b)
+    using (_·_)
+
+  open PropCompletion ℓ-zero ℕ≤+
+    using (typeAt; pathFromImplications)
+
+  ℕ↑b : Type₁
+  ℕ↑b = fst ℕ↑-+b
+
+  0LAnnihil : (x : ℕ↑b) → 0↑ · x ≡ 0↑
+  0LAnnihil x =
+    Σ≡Prop (λ s → PropCompletion.isPropIsBounded ℓ-zero ℕ≤+ s)
+           (pathFromImplications (fst (0↑ · x)) (fst 0↑) (⇒) ⇐)
+    where
+     ⇒ : (n : ℕ) → typeAt n (fst (0↑ · x)) → typeAt n (fst 0↑)
+     ⇒ n _ = n , ℕ+Comm n 0
+     ⇐ : (n : ℕ) → typeAt n (fst 0↑) → typeAt n (fst (0↑ · x))
+     ⇐ n _ =
+       propTruncRec
+         isPropPropTrunc
+         (λ {(m , mIsUpperBound) → ∣ (0 , m) , ((0 , refl) , (mIsUpperBound , n ,  +Rid n)) ∣₁})
+         (snd x)
+
+
+  asCommSemiring : CommSemiring (ℓ-suc ℓ-zero)
+  fst asCommSemiring = ℕ↑b
+  CommSemiringStr.0r (snd asCommSemiring) = 0↑
+  CommSemiringStr.1r (snd asCommSemiring) = OrderedCommMonoidStr.ε (snd ℕ↑-·b)
+  CommSemiringStr._+_ (snd asCommSemiring) = _+_
+  CommSemiringStr._·_ (snd asCommSemiring) = _·_
+  IsCommSemiring.+IsCommMonoid (CommSemiringStr.isCommSemiring (snd asCommSemiring)) =
+    OrderedCommMonoidStr.isCommMonoid (snd ℕ↑-+b)
+  IsCommSemiring.·IsCommMonoid (CommSemiringStr.isCommSemiring (snd asCommSemiring)) =
+    OrderedCommMonoidStr.isCommMonoid (snd ℕ↑-·b)
+  IsCommSemiring.·LDist+ (CommSemiringStr.isCommSemiring (snd asCommSemiring)) =
+    λ x y z → Σ≡Prop (λ s → PropCompletion.isPropIsBounded ℓ-zero ℕ≤+ s)
+                     (ConstructionUnbounded.+LDist· (fst x) (fst y) (fst z))
+  IsCommSemiring.0LAnnihil (CommSemiringStr.isCommSemiring (snd asCommSemiring)) = 0LAnnihil

Cubical/Algebra/Monoid/Base.agda

@@ -102,6 +102,12 @@ record IsMonoidHom {A : Type ℓ} {B : Type ℓ'}
 MonoidHom : (L : Monoid ℓ) (M : Monoid ℓ') → Type (ℓ-max ℓ ℓ')
 MonoidHom L M = Σ[ f ∈ (⟨ L ⟩ → ⟨ M ⟩) ] IsMonoidHom (L .snd) f (M .snd)
 
+isSetFromIsMonoid :
+  {M : Type ℓ} {ε : M} {_·_ : M → M → M}
+  (isMonoid : IsMonoid ε _·_)
+  → isSet M
+isSetFromIsMonoid isMonoid = IsSemigroup.is-set (IsMonoid.isSemigroup isMonoid)
+
 IsMonoidEquiv : {A : Type ℓ} {B : Type ℓ'} (M : MonoidStr A) (e : A ≃ B) (N : MonoidStr B)
   → Type (ℓ-max ℓ ℓ')
 IsMonoidEquiv M e N = IsMonoidHom M (e .fst) N
@@ -148,4 +154,3 @@ module MonoidTheory {ℓ} (M : Monoid ℓ) where
     (y · x) · z ≡⟨ cong (λ - → - · z) left-inverse ⟩
     ε · z       ≡⟨ lid z ⟩
     z ∎
-

Cubical/Algebra/OrderedCommMonoid.agda

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