Book cauchy reals #1182

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft

marcinjangrzybowski wants to merge 34 commits into agda:master from marcinjangrzybowski:book-cauchy-reals

Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -17,8 +17,8 @@ open import Cubical.Data.Empty as ⊥
  
    open import Cubical.HITs.FreeAbGroup

    open import Cubical.HITs.FreeGroup as FG hiding (rec)

    open import Cubical.HITs.SetQuotients as SQ hiding (_/_ ; rec)

    import Cubical.HITs.SetQuotients as SQ

    open import Cubical.HITs.SetQuotients using ([_])

    open import Cubical.Algebra.AbGroup

    open import Cubical.Algebra.AbGroup.Instances.Pi

    open import Cubical.Algebra.AbGroup.Instances.Int

Cubical/Algebra/AbGroup/Instances/Int/Fast.agda

-Original file line number
+Diff line change
@@ -0,0 +1,9 @@
+    module Cubical.Algebra.AbGroup.Instances.Int.Fast where
+    open import Cubical.Foundations.Prelude
+    open import Cubical.Data.Int.Fast
+    open import Cubical.Algebra.AbGroup.Base
+    open import Cubical.Algebra.Group.Instances.Int.Fast
+    ℤAbGroup : AbGroup ℓ-zero
+    ℤAbGroup = Group→AbGroup ℤGroup +Comm

Cubical/Algebra/CommRing/Instances/Int/Fast.agda

-Original file line number
+Diff line change
@@ -0,0 +1,23 @@
+    module Cubical.Algebra.CommRing.Instances.Int.Fast where
+    open import Cubical.Foundations.Prelude
+    open import Cubical.Algebra.CommRing
+    open import Cubical.Data.Int.Fast as Int renaming (_+_ to _+ℤ_; _·_ to _·ℤ_ ; -_ to -ℤ_)
+    open CommRingStr using (0r ; 1r ; _+_ ; _·_ ; -_ ; isCommRing)
+    ℤCommRing : CommRing ℓ-zero
+    fst ℤCommRing = ℤ
+r (snd ℤCommRing) = pos 0
+r (snd ℤCommRing) = pos 1
+    _+_ (snd ℤCommRing) = _+ℤ_
+    _·_ (snd ℤCommRing) = _·ℤ_
+    - snd ℤCommRing = -ℤ_
+    isCommRing (snd ℤCommRing) = isCommRingℤ
+      where
+      abstract
+        isCommRingℤ : IsCommRing (pos 0) (pos 1) _+ℤ_ _·ℤ_ -ℤ_
+        isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc +IdR
+                                     -Cancel Int.+Comm Int.·Assoc
+                                     Int.·IdR ·DistR+ Int.·Comm

Cubical/Algebra/CommRing/Instances/Rationals/Fast.agda

-Original file line number
+Diff line change
@@ -0,0 +1,33 @@
+    {- ℚ is a CommRing -}
+    module Cubical.Algebra.CommRing.Instances.Rationals.Fast where
+    open import Cubical.Foundations.Prelude
+    open import Cubical.Algebra.CommRing
+    open import Cubical.Data.Rationals.Fast as ℚ
+    open import Cubical.Algebra.CommRing.Instances.Int.Fast
+    open import Cubical.Data.NatPlusOne.Base
+    open import Cubical.Data.Nat using (zero)
+    import Cubical.Data.Int.Fast as ℤ
+    ℚCommRing : CommRing ℓ-zero
+    ℚCommRing .fst = ℚ
+    ℚCommRing .snd .CommRingStr.0r = 0
+    ℚCommRing .snd .CommRingStr.1r = 1
+    ℚCommRing .snd .CommRingStr._+_ = _+_
+    ℚCommRing .snd .CommRingStr._·_ = _·_
+    ℚCommRing .snd .CommRingStr.-_  = -_
+    ℚCommRing .snd .CommRingStr.isCommRing = p
+      where
+      p : IsCommRing 0 1 _+_ _·_ (-_)
+      p = makeIsCommRing isSetℚ +Assoc +IdR +InvR +Comm ·Assoc ·IdR ·DistL+ ·Comm
+    ℤ→ℚCommRingHom : CommRingHom ℤCommRing ℚCommRing
+    ℤ→ℚCommRingHom .fst x = [ x / 1+ zero ]
+    ℤ→ℚCommRingHom .snd .IsCommRingHom.pres0 = refl
+    ℤ→ℚCommRingHom .snd .IsCommRingHom.pres1 = refl
+    ℤ→ℚCommRingHom .snd .IsCommRingHom.pres+ x y =
+     eq/ _ _ (cong (ℤ._· 1) (cong₂ ℤ._+_ (sym (ℤ.·IdR x)) (sym (ℤ.·IdR y))))
+    ℤ→ℚCommRingHom .snd .IsCommRingHom.pres· _ _ = refl
+    ℤ→ℚCommRingHom .snd .IsCommRingHom.pres- x =
+     eq/ _ _ (cong (ℤ._· 1) (cong (ℤ.-_) (sym (ℤ.·IdL x)) ∙ ℤ.-DistL· 1 x))

Cubical/Algebra/Group/Instances/Int/Fast.agda

-Original file line number
+Diff line change
@@ -0,0 +1,56 @@
+    module Cubical.Algebra.Group.Instances.Int.Fast where
+    open import Cubical.Foundations.Prelude
+    open import Cubical.Foundations.Isomorphism
+    open import Cubical.Foundations.Function
+    open import Cubical.Data.Int.Fast renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_)
+    open import Cubical.Data.Nat using (ℕ ; zero ; suc)
+    open import Cubical.Data.Fin.Inductive.Base
+    open import Cubical.Algebra.Group.Base
+    open import Cubical.Algebra.Group.Properties
+    open import Cubical.Algebra.Group.Morphisms
+    open import Cubical.Algebra.Group.MorphismProperties
+    open GroupStr
+    ℤGroup : Group₀
+    fst ℤGroup = ℤ
+g (snd ℤGroup) = 0
+    _·_ (snd ℤGroup) = _+ℤ_
+    inv (snd ℤGroup) = -ℤ_
+    isGroup (snd ℤGroup) = isGroupℤ
+      where
+      abstract
+        isGroupℤ : IsGroup (pos 0) (_+ℤ_) (-ℤ_)
+        isGroupℤ = makeIsGroup isSetℤ
+                               +Assoc +IdR +IdL
+                               -Cancel -Cancel'
+    ℤHom : (n : ℤ) → GroupHom ℤGroup ℤGroup
+    fst (ℤHom n) x = n ·ℤ x
+    snd (ℤHom n) =
+      makeIsGroupHom λ x y → ·DistR+ n x y
+    negEquivℤ : GroupEquiv ℤGroup ℤGroup
+    fst negEquivℤ =
+      isoToEquiv
+        (iso (GroupStr.inv (snd ℤGroup))
+             (GroupStr.inv (snd ℤGroup))
+             (GroupTheory.invInv ℤGroup)
+             (GroupTheory.invInv ℤGroup))
+    snd negEquivℤ =
+      makeIsGroupHom -Dist+
+    sumFinGroupℤComm : (G : Group₀) (h : GroupIso G ℤGroup) {n : ℕ}
+      (f : Fin n → fst G) → sumFinℤ {n = n} (λ a → Iso.fun (fst h) (f a))
+      ≡ Iso.fun (fst h) (sumFinGroup G {n = n} f)
+    sumFinGroupℤComm G h {n = zero} f = sym (IsGroupHom.pres1 (snd h))
+    sumFinGroupℤComm G h {n = suc n} f =
+        cong₂ _+ℤ_ (λ _ → Iso.fun (fst h) (f flast))
+          (sumFinGroupℤComm G h {n = n} (f ∘ injectSuc {n = n}))
+      ∙ sym (IsGroupHom.pres· (snd h) (f flast)
+        (sumFinGroup G {n = n} (λ x → f (injectSuc {n = n} x))))

Cubical/Algebra/Group/MorphismProperties.agda

-Original file line number
+Diff line change
@@ Expand Up / @@ -309,3 +309,18 @@ BijectionIso→GroupIso {G = G} {H = H} i = grIso @@
     BijectionIsoToGroupEquiv : BijectionIso G H → GroupEquiv G H
     BijectionIsoToGroupEquiv i = GroupIso→GroupEquiv (BijectionIso→GroupIso i)
+    Aut[_] : Group ℓ → Group ℓ
+    Aut[ Ĝ@(G , Gstr) ] =
+      makeGroup {G = GroupIso Ĝ Ĝ}
+        idGroupIso compGroupIso
+          invGroupIso  (isSetΣ (isSet-SetsIso (is-set Gstr) (is-set Gstr)) (λ _ → isProp→isSet (isPropIsGroupHom _ _)))
+            (λ _ _ _ → GroupIso≡ (i≡ refl))
+             (λ _ → GroupIso≡ (i≡ refl))
+             (λ _ → GroupIso≡ (i≡ refl))
+             (λ (x , _) → GroupIso≡ (i≡ (funExt (Iso.leftInv x))))
+             (λ (x , _) → GroupIso≡ (i≡ (funExt (Iso.rightInv x))))
+     where
+     open GroupStr Gstr
+     i≡ = SetsIso≡fun (is-set Gstr) (is-set Gstr)

Cubical/Algebra/OrderedCommRing/Base.agda

-Original file line number
+Diff line change
@@ -1,6 +1,6 @@
     module Cubical.Algebra.OrderedCommRing.Base where
     {-
-      Definition of an commutative ordered ring.
+      Definition of an ordered commutative ring.
     -}
     open import Cubical.Foundations.Prelude
@@ Expand Down @@

Cubical/Algebra/OrderedCommRing/Instances/Int.agda

-Original file line number
+Diff line change
@@ -0,0 +1,66 @@
+    module Cubical.Algebra.OrderedCommRing.Instances.Int where
+    open import Cubical.Foundations.Prelude
+    open import Cubical.Foundations.Function
+    open import Cubical.Foundations.Equiv
+    open import Cubical.Data.Empty as ⊥
+    open import Cubical.HITs.PropositionalTruncation
+    open import Cubical.Data.Int as ℤ
+      renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
+    open import Cubical.Data.Int.Order
+      renaming (_<_ to _<ℤ_ ; _≤_ to _≤ℤ_)
+    open import Cubical.Algebra.CommRing
+    open import Cubical.Algebra.CommRing.Instances.Int
+    open import Cubical.Algebra.OrderedCommRing
+    open import Cubical.Relation.Nullary
+    open import Cubical.Relation.Binary.Order.StrictOrder
+    open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Int
+    open import Cubical.Relation.Binary.Order.Pseudolattice
+    open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Int
+    open CommRingStr
+    open OrderedCommRingStr
+    open PseudolatticeStr
+    open StrictOrderStr
+    ℤOrderedCommRing : OrderedCommRing ℓ-zero ℓ-zero
+    fst ℤOrderedCommRing = ℤ
+r  (snd ℤOrderedCommRing) = 0
+r  (snd ℤOrderedCommRing) = 1
+    _+_ (snd ℤOrderedCommRing) = _+ℤ_
+    _·_ (snd ℤOrderedCommRing) = _·ℤ_
+    -_  (snd ℤOrderedCommRing) = -ℤ_
+    _<_ (snd ℤOrderedCommRing) = _<ℤ_
+    _≤_ (snd ℤOrderedCommRing) = _≤ℤ_
+    isOrderedCommRing (snd ℤOrderedCommRing) = isOrderedCommRingℤ
+      where
+        open IsOrderedCommRing
+        isOrderedCommRingℤ : IsOrderedCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_ _<ℤ_ _≤ℤ_
+        isOrderedCommRingℤ .isCommRing      = ℤCommRing .snd .isCommRing
+        isOrderedCommRingℤ .isPseudolattice = ℤ≤Pseudolattice .snd .is-pseudolattice
+        isOrderedCommRingℤ .isStrictOrder   = ℤ<StrictOrder .snd .isStrictOrder
+        isOrderedCommRingℤ .<-≤-weaken      = λ _ _ → <-weaken
+        isOrderedCommRingℤ .≤≃¬>            = λ x y →
+          propBiimpl→Equiv isProp≤ (isProp¬ (y <ℤ x))
+            (λ x≤y y<x → isIrrefl< (≤<-trans x≤y y<x))
+            (λ ¬y<x → case x ≟ y return (λ _ → x ≤ℤ y) of λ {
+              (lt x<y) → <-weaken x<y ;
+              (eq x≡y) → subst (x ≤ℤ_) x≡y isRefl≤ ;
+              (gt y<z) → ⊥.rec (¬y<x y<z) })
+        isOrderedCommRingℤ .+MonoR≤         = λ _ _ z → ≤-+o {o = z}
+        isOrderedCommRingℤ .+MonoR<         = λ _ _ z → <-+o {o = z}
+        isOrderedCommRingℤ .posSum→pos∨pos  = λ _ _ → ∣_∣₁ ∘ 0<+ _ _
+        isOrderedCommRingℤ .<-≤-trans       = λ _ _ _ → <≤-trans
+        isOrderedCommRingℤ .≤-<-trans       = λ _ _ _ → ≤<-trans
+        isOrderedCommRingℤ .·MonoR≤         = λ _ _ _ → 0≤o→≤-·o
+        isOrderedCommRingℤ .·MonoR<         = λ _ _ _ → 0<o→<-·o
+        isOrderedCommRingℤ .0<1             = isRefl≤

Cubical/Algebra/OrderedCommRing/Instances/Int/Fast.agda

-Original file line number
+Diff line change
@@ -0,0 +1,69 @@
+    module Cubical.Algebra.OrderedCommRing.Instances.Int.Fast where
+    open import Cubical.Foundations.Prelude
+    open import Cubical.Foundations.Function
+    open import Cubical.Foundations.Equiv
+    open import Cubical.Data.Empty as ⊥
+    open import Cubical.HITs.PropositionalTruncation
+    open import Cubical.Data.Int.Fast as ℤ
+      renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
+    open import Cubical.Data.Int.Fast.Order
+      renaming (_<_ to _<ℤ_ ; _≤_ to _≤ℤ_)
+    open import Cubical.Algebra.CommRing
+    open import Cubical.Algebra.CommRing.Instances.Int.Fast
+    open import Cubical.Algebra.OrderedCommRing
+    open import Cubical.Relation.Nullary
+    open import Cubical.Relation.Binary.Order.StrictOrder
+    open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Int.Fast
+    open import Cubical.Relation.Binary.Order.Pseudolattice
+    open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Int.Fast
+    open import Cubical.Relation.Binary
+    open BinaryRelation
+    open CommRingStr
+    open OrderedCommRingStr
+    open PseudolatticeStr
+    open StrictOrderStr
+    ℤOrderedCommRing : OrderedCommRing ℓ-zero ℓ-zero
+    fst ℤOrderedCommRing = ℤ
+r  (snd ℤOrderedCommRing) = 0
+r  (snd ℤOrderedCommRing) = 1
+    _+_ (snd ℤOrderedCommRing) = _+ℤ_
+    _·_ (snd ℤOrderedCommRing) = _·ℤ_
+    -_  (snd ℤOrderedCommRing) = -ℤ_
+    _<_ (snd ℤOrderedCommRing) = _<ℤ_
+    _≤_ (snd ℤOrderedCommRing) = _≤ℤ_
+    isOrderedCommRing (snd ℤOrderedCommRing) = isOrderedCommRingℤ
+      where
+        open IsOrderedCommRing
+        isOrderedCommRingℤ : IsOrderedCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_ _<ℤ_ _≤ℤ_
+        isOrderedCommRingℤ .isCommRing      = ℤCommRing .snd .isCommRing
+        isOrderedCommRingℤ .isPseudolattice = ℤ≤Pseudolattice .snd .is-pseudolattice
+        isOrderedCommRingℤ .isStrictOrder   = ℤ<StrictOrder .snd .isStrictOrder
+        isOrderedCommRingℤ .<-≤-weaken      = λ x y → <-weaken {x} {y}
+        isOrderedCommRingℤ .≤≃¬>            = λ x y →
+          propBiimpl→Equiv (isProp≤ {x} {y}) (isProp¬ (y <ℤ x))
+            (λ x≤y y<x → isIrrefl< (≤<-trans {x} {y} x≤y y<x))
+            (λ ¬y<x → case x ≟ y return (λ _ → x ≤ℤ y) of λ {
+              (lt x<y) → <-weaken {x} {y} x<y ;
+              (eq x≡y) → subst (x ≤ℤ_) x≡y isRefl≤ ;
+              (gt y<z) → ⊥.rec (¬y<x y<z) })
+        isOrderedCommRingℤ .+MonoR≤         = λ x y z → ≤-+o {x} {y} {z}
+        isOrderedCommRingℤ .+MonoR<         = λ x y z → <-+o {x} {y} {z}
+        isOrderedCommRingℤ .posSum→pos∨pos  = λ _ _ → ∣_∣₁ ∘ 0<+ _ _
+        isOrderedCommRingℤ .<-≤-trans       = λ x y z → <≤-trans {x} {y} {z}
+        isOrderedCommRingℤ .≤-<-trans       = λ x y z → ≤<-trans {x} {y} {z}
+        isOrderedCommRingℤ .·MonoR≤         = λ x y z → 0≤o→≤-·o {z} {x} {y}
+        isOrderedCommRingℤ .·MonoR<         = λ x y z → 0<o→<-·o {z} {x} {y}
+        isOrderedCommRingℤ .0<1             = isRefl≤

Cubical/Algebra/OrderedCommRing/Instances/Rationals/Fast.agda

-Original file line number
+Diff line change
@@ -0,0 +1,68 @@
+    {- ℚ is an ordered commutative ring -}
+    module Cubical.Algebra.OrderedCommRing.Instances.Rationals.Fast where
+    open import Cubical.Foundations.Prelude
+    open import Cubical.Foundations.Function
+    open import Cubical.Foundations.Equiv
+    open import Cubical.Data.Empty as ⊥
+    open import Cubical.HITs.PropositionalTruncation
+    open import Cubical.Data.Rationals.Fast as ℚ
+      renaming (_+_ to _+ℚ_ ; _-_ to _-ℚ_; -_ to -ℚ_ ; _·_ to _·ℚ_)
+    open import Cubical.Data.Rationals.Fast.Order
+      renaming (_<_ to _<ℚ_ ; _≤_ to _≤ℚ_)
+    open import Cubical.Algebra.CommRing
+    open import Cubical.Algebra.CommRing.Instances.Rationals.Fast
+    open import Cubical.Algebra.OrderedCommRing
+    open import Cubical.Relation.Nullary
+    open import Cubical.Relation.Binary.Order.StrictOrder
+    open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Rationals.Fast
+    open import Cubical.Relation.Binary.Order.Pseudolattice
+    open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Rationals.Fast
+    open CommRingStr
+    open OrderedCommRingStr
+    open PseudolatticeStr
+    open StrictOrderStr
+    ℚOrderedCommRing : OrderedCommRing ℓ-zero ℓ-zero
+    fst ℚOrderedCommRing = ℚ
+r  (snd ℚOrderedCommRing) = 0
+r  (snd ℚOrderedCommRing) = 1
+    _+_ (snd ℚOrderedCommRing) = _+ℚ_
+    _·_ (snd ℚOrderedCommRing) = _·ℚ_
+    -_  (snd ℚOrderedCommRing) = -ℚ_
+    _<_ (snd ℚOrderedCommRing) = _<ℚ_
+    _≤_ (snd ℚOrderedCommRing) = _≤ℚ_
+    isOrderedCommRing (snd ℚOrderedCommRing) = isOrderedCommRingℚ
+      where
+      open IsOrderedCommRing
+      isOrderedCommRingℚ : IsOrderedCommRing 0 1 _+ℚ_ _·ℚ_ -ℚ_ _<ℚ_ _≤ℚ_
+      isOrderedCommRingℚ .isCommRing      = ℚCommRing .snd .isCommRing
+      isOrderedCommRingℚ .isPseudolattice = ℚ≤Pseudolattice .snd .is-pseudolattice
+      isOrderedCommRingℚ .isStrictOrder   = ℚ<StrictOrder .snd .isStrictOrder
+      isOrderedCommRingℚ .<-≤-weaken      = <Weaken≤
+      isOrderedCommRingℚ .≤≃¬>            = λ x y →
+        propBiimpl→Equiv (isProp≤ x y) (isProp¬ (y <ℚ x))
+        (λ x≤y y<x → isIrrefl< x (isTrans≤< x y x x≤y y<x))
+        (λ ¬y<x → case x ≟ y return (λ _ → x ≤ℚ y) of λ {
+              (lt x<y) → <Weaken≤ x y x<y
+            ; (eq x≡y) → subst (x ≤ℚ_) x≡y (isRefl≤ x)
+            ; (gt y<z) → ⊥.rec (¬y<x y<z) })
+      isOrderedCommRingℚ .+MonoR≤         = ≤-+o
+      isOrderedCommRingℚ .+MonoR<         = <-+o
+      isOrderedCommRingℚ .posSum→pos∨pos  = λ x y → ∣_∣₁ ∘ 0<+ x y
+      isOrderedCommRingℚ .<-≤-trans       = isTrans<≤
+      isOrderedCommRingℚ .≤-<-trans       = isTrans≤<
+      isOrderedCommRingℚ .·MonoR≤         = ≤-·o
+      isOrderedCommRingℚ .·MonoR<         = <-·o
+      isOrderedCommRingℚ .0<1             = inj (_ , refl)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Book cauchy reals #1182

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

Book cauchy reals #1182

Are you sure you want to change the base?

Uh oh!

Book cauchy reals #1182

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!