Move Bool to live on its own (#118)

2025-10-12 23:28:39 +00:00 · 2020-04-18 17:14:39 +01:00
parent 264a5e2bd9
commit 84a146f72c
30 changed files with 270 additions and 123 deletions
--- a/.travis.yml
+++ b/.travis.yml
@@ -13,6 +13,6 @@ script:
  - export BRANCH=$(if [ "$TRAVIS_PULL_REQUEST" == "false" ]; then echo $TRAVIS_BRANCH; else echo $TRAVIS_PULL_REQUEST_BRANCH; fi)
  - docker run -i --detach --name agda smaug451/agda:basic
  - docker exec agda bash -c "cd ~/; git clone https://github.com/Smaug123/agdaproofs.git; cd agdaproofs; git fetch; git checkout $BRANCH"
-  - docker exec agda bash -c "cd ~/agdaproofs; agda Everything/Safe.agda && agda Everything/WithK.agda"
+  - docker exec agda bash -c "cd ~/agdaproofs; agda Everything/Safe.agda && agda Everything/WithK.agda && agda Everything/Guardedness.agda"
  - docker exec agda bash -c "cd ~/agdaproofs; find . -type f -name '*.agda' | sort > /tmp/agdas.txt; find . -type f -name '*.agdai' | sort | rev | cut -c 2- | rev > /tmp/compiled.txt; diff /tmp/agdas.txt /tmp/compiled.txt | grep '<' || true"
  - docker stop agda
--- a/Boolean/Definition.agda
+++ b/Boolean/Definition.agda
@@ -0,0 +1,28 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Boolean.Definition where
+
+data Bool : Set where
+  BoolTrue : Bool
+  BoolFalse : Bool
+{-# BUILTIN BOOL  Bool  #-}
+{-# BUILTIN TRUE  BoolTrue  #-}
+{-# BUILTIN FALSE BoolFalse #-}
+
+if_then_else_ : {a : _} → {A : Set a} → Bool → A → A → A
+if BoolTrue then tr else fls = tr
+if BoolFalse then tr else fls = fls
+
+not : Bool → Bool
+not BoolTrue = BoolFalse
+not BoolFalse = BoolTrue
+
+boolAnd : Bool → Bool → Bool
+boolAnd BoolTrue y = y
+boolAnd BoolFalse y = BoolFalse
+
+boolOr : Bool → Bool → Bool
+boolOr BoolTrue y = BoolTrue
+boolOr BoolFalse y = y
--- a/Decidable/Reduction.agda
+++ b/Decidable/Reduction.agda
@@ -0,0 +1,16 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Decidable.Relations
+open import Boolean.Definition
+
+module Decidable.Reduction where
+
+squash : {a b : _} {A : Set a} {f : A → Set b} → DecidableRelation f → A → Bool
+squash rel a with rel a
+... | inl x = BoolTrue
+... | inr x = BoolFalse
+
+unsquash : {a b : _} {A : Set a} {f : A → Set b} → (rel : DecidableRelation f) → {x : A} → .(squash rel x ≡ BoolTrue) → f x
+unsquash rel {x} pr with rel x
+... | inl ans = ans
--- a/Everything/Guardedness.agda
+++ b/Everything/Guardedness.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --warning=error --safe --without-K --guardedness #-}
+
+open import Everything.Safe
+
+open import Numbers.Reals.Definition
+open import Fields.Orders.Limits.Definition
+open import Rings.Orders.Partial.Bounded
+open import Rings.Orders.Total.Bounded
+open import Rings.Orders.Total.BaseExpansion
+open import Fields.Orders.Limits.Lemmas
+open import Fields.CauchyCompletion.Archimedean
+
+open import Sets.Cardinality.Infinite.Examples
+
+module Everything.Guardedness where
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --warning=error --safe --without-K --guardedness #-}
+{-# OPTIONS --warning=error --safe --without-K #-}

 -- This file contains everything that can be compiled in --safe mode.

@@ -10,7 +10,6 @@ open import Numbers.BinaryNaturals.Subtraction
 open import Numbers.Primes.PrimeNumbers
 open import Numbers.Primes.IntegerFactorisation
 open import Numbers.Rationals.Lemmas
-open import Numbers.Reals.Definition

 open import Numbers.Modulo.Group

@@ -53,10 +52,9 @@ open import Groups.LectureNotes.Lecture1
 open import Fields.Fields
 open import Fields.Orders.Partial.Definition
 open import Fields.Orders.Total.Definition
-open import Fields.Orders.Total.Archimedean
+open import Fields.Orders.Partial.Archimedean
 open import Fields.Orders.LeastUpperBounds.Examples
 open import Fields.Orders.Lemmas
-open import Fields.Orders.Limits.Definition
 open import Fields.FieldOfFractions.Field
 open import Fields.FieldOfFractions.Lemmas
 open import Fields.FieldOfFractions.Order
@@ -97,9 +95,6 @@ open import Rings.InitialRing
 open import Rings.Homomorphisms.Lemmas
 open import Rings.UniqueFactorisationDomains.Definition
 open import Rings.Examples.Examples
-open import Rings.Orders.Total.Bounded
-open import Rings.Orders.Partial.Bounded
-open import Rings.Orders.Total.BaseExpansion

 open import Setoids.Setoids
 open import Setoids.DirectSum
@@ -113,7 +108,6 @@ open import Setoids.Union.Lemmas
 open import Setoids.Cardinality.Infinite.Lemmas
 open import Setoids.Cardinality.Finite.Definition

-open import Sets.Cardinality.Infinite.Examples
 open import Sets.Cardinality.Infinite.Lemmas
 open import Sets.Cardinality.Countable.Lemmas
 open import Sets.Cardinality.Finite.Lemmas
@@ -121,6 +115,7 @@ open import Sets.Cardinality
 open import Sets.FinSet.Lemmas

 open import Decidable.Sets
+open import Decidable.Reduction
 open import Decidable.Relations

 open import Vectors
@@ -163,9 +158,6 @@ open import Modules.PolynomialModule
 open import Modules.Lemmas
 open import Modules.DirectSum

-open import Fields.CauchyCompletion.Archimedean
-open import Fields.Orders.Limits.Lemmas
-
 open import ProjectEuler.Problem1

 module Everything.Safe where
--- a/Everything/WithK.agda
+++ b/Everything/WithK.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --warning=error --safe --guardedness #-}
+{-# OPTIONS --warning=error --safe #-}

 open import Everything.Safe

--- a/Fields/CauchyCompletion/Archimedean.agda
+++ b/Fields/CauchyCompletion/Archimedean.agda
@@ -17,7 +17,7 @@ open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Fields.Orders.Total.Archimedean

-module Fields.CauchyCompletion.Archimedean {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (arch : ArchimedeanField {F = F} record { oRing = order }) where
+module Fields.CauchyCompletion.Archimedean {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) (arch : ArchimedeanField {F = F} (record { oRing = pRing })) where

 open import Fields.CauchyCompletion.Group order F
 open import Fields.CauchyCompletion.Ring order F
--- a/Fields/CauchyCompletion/Field.agda
+++ b/Fields/CauchyCompletion/Field.agda
@@ -30,6 +30,7 @@ open Group (Ring.additiveGroup R)

 open import Rings.Orders.Total.Cauchy order
 open import Rings.Orders.Total.Lemmas order
+open import Rings.Orders.Total.AbsoluteValue order
 open import Fields.CauchyCompletion.Definition order F
 open import Fields.CauchyCompletion.Multiplication order F
 open import Fields.CauchyCompletion.Addition order F
--- a/Fields/CauchyCompletion/PartiallyOrderedRing.agda
+++ b/Fields/CauchyCompletion/PartiallyOrderedRing.agda
@@ -107,42 +107,14 @@ private
      ans : (m : ℕ) → (index (CauchyCompletion.elts (injection b +C a)) m + index (map inverse (CauchyCompletion.elts a)) m) ∼ b
      ans m rewrite indexAndApply (CauchyCompletion.elts (injection b)) (CauchyCompletion.elts a) _+_ {m} | indexAndConst b m | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) = transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)

-{-
-  minAddLemma : (a b : A) → (0R < a) → (min a b) < (a + b)
-  minAddLemma a b 0<a with totality a b
-  ... | inl (inl x) = <WellDefined identLeft groupIsAbelian (orderRespectsAddition (<Transitive 0<a x) a)
-  ... | inl (inr x) = <WellDefined identLeft reflexive (orderRespectsAddition 0<a b)
-  ... | inr x = <WellDefined identLeft groupIsAbelian (orderRespectsAddition (<WellDefined reflexive x 0<a) a)
-
-  addInequalities : {a b : CauchyCompletion} → 0R r<C a → 0R r<C b → 0R r<C (a +C b)
-  addInequalities {a} {b} record { e = eA ; 0<e = 0<eA ; N = Na ; pr = prA } record { e = eB ; 0<e = 0<eB ; N = Nb ; pr = prB } = record { e = min eA eB ; 0<e = minInequalitiesR 0<eA 0<eB ; N = N ; pr = λ m N<m → <Transitive (<WellDefined (symmetric identLeft) reflexive (minAddLemma eA eB 0<eA)) (<WellDefined (+WellDefined identLeft identLeft) (identityOfIndiscernablesLeft _∼_ reflexive (indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _+_ {m})) (ringAddInequalities (prA m (p2 m N<m)) (prB m (p1 m N<m)))) }
-    where
-      N = succ (TotalOrder.max ℕTotalOrder Na Nb)
-      Nb<N : Nb <N succ (TotalOrder.max ℕTotalOrder Na Nb)
-      Nb<N with TotalOrder.totality ℕTotalOrder Na Nb
-      ... | inl (inl x) = le 0 refl
-      ... | inl (inr x) = lessTransitive x (le 0 refl)
-      ... | inr x = le 0 refl
-      Na<N : Na <N succ (TotalOrder.max ℕTotalOrder Na Nb)
-      Na<N with TotalOrder.totality ℕTotalOrder Na Nb
-      ... | inl (inl x) = lessTransitive x (le 0 refl)
-      ... | inl (inr x) = le 0 refl
-      ... | inr x = le 0 (applyEquality succ x)
-      p1 : (m : ℕ) → (N <N m) → Nb <N m
-      p1 m N<m = lessTransitive Nb<N N<m
-      p2 : (m : ℕ) → (N <N m) → Na <N m
-      p2 m N<m = lessTransitive Na<N N<m
-
-}
-
  invInj : (i : A) → Setoid._∼_ cauchyCompletionSetoid (injection (inverse i) +C injection i) (injection 0R)
-  invInj i = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (inverse i) +C injection i) }} {record { converges = CauchyCompletion.converges ((-C (injection i)) +C injection i) }} {record { converges = CauchyCompletion.converges (injection 0R) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse i)) }} {record { converges = CauchyCompletion.converges (injection i)}} {record { converges = CauchyCompletion.converges (-C (injection i)) }} {record { converges = CauchyCompletion.converges (injection i) }} homRespectsInverse (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection i) }})) (Group.invLeft CGroup {injection i})
+  invInj i = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (inverse i) +C injection i) }} {record { converges = CauchyCompletion.converges ((-C (injection i)) +C injection i) }} {record { converges = CauchyCompletion.converges (injection 0R) }} (Group.+WellDefinedLeft CGroup {record { converges = CauchyCompletion.converges (injection (inverse i)) }} {record { converges = CauchyCompletion.converges (injection i)}} {record { converges = CauchyCompletion.converges (-C (injection i)) }} homRespectsInverse) (Group.invLeft CGroup {injection i})

  cOrderMove : (a b : A) (c : CauchyCompletion) → (injection a +C c) <Cr b → a r<C (injection b +C (-C c))
  cOrderMove a b c record { e = e ; 0<e = 0<e ; N = N ; property = property } = record { e = e ; 0<e = 0<e ; N = N ; pr = λ m N<m → <WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts (injection a)) (CauchyCompletion.elts c) _+_ {m})) reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst a m)) invRight) identRight)))) groupIsAbelian)) (transitive (+WellDefined (identityOfIndiscernablesLeft _∼_ reflexive (indexAndConst b m)) (identityOfIndiscernablesRight _∼_ reflexive (mapAndIndex (CauchyCompletion.elts c) inverse m))) (identityOfIndiscernablesLeft _∼_ reflexive (indexAndApply (CauchyCompletion.elts (injection b)) (CauchyCompletion.elts (-C c)) _+_ {m}))) (orderRespectsAddition (property m N<m) (inverse (index (CauchyCompletion.elts c) m))) }

  cOrderMove' : (a b : A) (c : CauchyCompletion) → (injection a +C (-C c)) <Cr b → a r<C (injection b +C c)
-  cOrderMove' a b c pr = r<CWellDefinedRight _ _ _ (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection b) }} {record { converges = CauchyCompletion.converges (-C (-C c)) }} {record { converges = CauchyCompletion.converges (injection b) }} {record {converges = CauchyCompletion.converges c }} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection b) }}) (invTwice CGroup record { converges = CauchyCompletion.converges c })) (cOrderMove a b (-C c) pr)
+  cOrderMove' a b c pr = r<CWellDefinedRight _ _ _ (Group.+WellDefinedRight CGroup {record { converges = CauchyCompletion.converges (injection b) }} {record { converges = CauchyCompletion.converges (-C (-C c)) }} {record {converges = CauchyCompletion.converges c }} (invTwice CGroup record { converges = CauchyCompletion.converges c })) (cOrderMove a b (-C c) pr)

  cOrderMove'' : (a : CauchyCompletion) (b c : A) → (a +C (-C injection b)) <Cr c → a <Cr (b + c)
  cOrderMove'' a b c record { e = e ; 0<e = 0<e ; N = N ; property = property } = record { e = e ; 0<e = 0<e ; N = N ; property = λ m N<m → <WellDefined (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (identityOfIndiscernablesRight _∼_ reflexive (indexAndApply (CauchyCompletion.elts a) _ _+_ {m})) reflexive) (transitive (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (transitive (identityOfIndiscernablesLeft _∼_ reflexive (mapAndIndex _ inverse m)) (inverseWellDefined additiveGroup (identityOfIndiscernablesRight _∼_ reflexive (indexAndConst b m)))) reflexive) invLeft))) identRight)))) groupIsAbelian (orderRespectsAddition (property m N<m) b) }
@@ -157,7 +129,7 @@ private
      g' : ((injection aboveC +C (-C c)) +C injection a) <C (injection (b-a/2 + a))
      g' = <CWellDefined (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((injection aboveC +C (-C c)) +C injection a) }}) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (b-a/2 + a)) }} {record { converges = CauchyCompletion.converges (injection b-a/2 +C injection a) }} (GroupHom.groupHom CInjectionGroupHom)) g
      t : (injection (a + aboveC) +C (-C c)) <Cr (b-a/2 + a)
-      t = <CRelaxR' (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (((injection aboveC) +C (-C c)) +C injection a) }} {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC) +C (-C c)) }} (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection aboveC +C (-C c)) }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (((injection a) +C (injection aboveC)) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((injection (a + aboveC)) +C (-C c)) }} (Group.+Associative CGroup {record { converges = CauchyCompletion.converges (injection a) }} {record { converges = CauchyCompletion.converges (injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }}) (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (-C c) }} (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} (GroupHom.groupHom CInjectionGroupHom)) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C c)}})))) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (b-a/2 + a)) }}) g')
+      t = <CRelaxR' (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (((injection aboveC) +C (-C c)) +C injection a) }} {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC) +C (-C c)) }} (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection aboveC +C (-C c)) }} {record { converges = CauchyCompletion.converges (injection a) }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection a +C ((injection aboveC) +C (-C c))) }} {record { converges = CauchyCompletion.converges (((injection a) +C (injection aboveC)) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((injection (a + aboveC)) +C (-C c)) }} (Group.+Associative CGroup {record { converges = CauchyCompletion.converges (injection a) }} {record { converges = CauchyCompletion.converges (injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }}) (Group.+WellDefinedLeft CGroup {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (a + aboveC)) }} {record { converges = CauchyCompletion.converges (injection a +C injection aboveC) }} (GroupHom.groupHom CInjectionGroupHom))))) (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (b-a/2 + a)) }}) g')
      lemm : 0R < b-a/2
      lemm = halvePositive' prDiff (moveInequality a<b)
      u : (b-a/2 + a) < b
@@ -167,16 +139,7 @@ private
  cOrderRespectsAdditionLeft''Flip a b c a<b = <CWellDefined ((Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection a) }} {record { converges = CauchyCompletion.converges c }})) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection b) }} {record { converges = CauchyCompletion.converges c }}) (cOrderRespectsAdditionLeft'' a b c a<b)

  cOrderRespectsAdditionLeft''' : (a b : CauchyCompletion) (c : A) → (a <C b) → (a +C injection c) <C (b +C injection c)
-  cOrderRespectsAdditionLeft''' a b c record { i = i ; a<i = a<i ; i<b = i<b } = <CTransitive (cOrderRespectsAdditionLeft' a i c a<i) (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C injection i) }} {record { converges = CauchyCompletion.converges (injection i +C injection c) }} (GroupHom.groupHom CInjectionGroupHom) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges (injection i) }})) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}) (flip<C' {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C b) }} (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((-C b) +C injection (inverse c)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (-C b) }} {record { converges = CauchyCompletion.converges (injection (inverse c)) }} {record { converges = CauchyCompletion.converges (-C b) }} {record { converges = CauchyCompletion.converges (-C (injection c)) }} (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C b) }}) homRespectsInverse) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} (invContravariant CGroup {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}))) homRespectsInverse' (cOrderRespectsAdditionLeft' (-C b) (inverse i) (inverse c) (flipR<C i<b)))))
-
-{-
-
-Have 0<a, so 0 < a- < a < a+
-Have c < a- + c, by cOrderRespectsAdditionLeft''
-Have a- + c < a+ + c     by cOrderRespectsAdditionLeft''
-  so a- + c < K < a+ + c
-
-}
+  cOrderRespectsAdditionLeft''' a b c record { i = i ; a<i = a<i ; i<b = i<b } = <CTransitive (cOrderRespectsAdditionLeft' a i c a<i) (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C injection i) }} {record { converges = CauchyCompletion.converges (injection i +C injection c) }} (GroupHom.groupHom CInjectionGroupHom) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges (injection i) }})) (Ring.groupIsAbelian CRing {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}) (flip<C' {record { converges = CauchyCompletion.converges (injection (c + i)) }} {record { converges = CauchyCompletion.converges (injection c +C b) }} (<CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((-C b) +C injection (inverse c)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} (Group.+WellDefinedRight CGroup {record { converges = CauchyCompletion.converges (-C b) }} {record { converges = CauchyCompletion.converges (injection (inverse c)) }} {record { converges = CauchyCompletion.converges (-C (injection c)) }} homRespectsInverse) (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C (injection c +C b)) }} {record { converges = CauchyCompletion.converges ((-C b) +C (-C (injection c))) }} (invContravariant CGroup {record { converges = CauchyCompletion.converges (injection c) }} {record { converges = CauchyCompletion.converges b }}))) homRespectsInverse' (cOrderRespectsAdditionLeft' (-C b) (inverse i) (inverse c) (flipR<C i<b)))))

  cOrderRespectsAdditionRightZero : (a : CauchyCompletion) → (0R r<C a) → (c : CauchyCompletion) → c <C (a +C c)
  cOrderRespectsAdditionRightZero a record { e = e ; 0<e = 0<e ; N = N1 ; pr = pr } c with halve charNot2 e
@@ -211,7 +174,7 @@ Have a- + c < a+ + c     by cOrderRespectsAdditionLeft''
      open Equivalence (Setoid.eq cauchyCompletionSetoid) renaming (transitive to tr)

  cOrderRespectsAdditionRight : (a : A) (b : CauchyCompletion) (c : CauchyCompletion) → (a r<C b) → (injection a +C c) <C (b +C c)
-  cOrderRespectsAdditionRight a b c a<b = <CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (Group.inverse CGroup (injection (inverse a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (Group.inverse CGroup ((-C injection a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection a +C c) }} (inverseWellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse a) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((-C (injection a)) +C (-C c)) }} (Group.+WellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse a)) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (-C (injection a)) }} {record { converges = CauchyCompletion.converges (-C c) }} homRespectsInverse (Equivalence.reflexive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (-C c) }}))) (lemma2 (injection a) c)) (lemma2 b c) (flip<C (cOrderRespectsAdditionLeft _ _ (Group.inverse CGroup c) (flipR<C a<b)))
+  cOrderRespectsAdditionRight a b c a<b = <CWellDefined (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges (Group.inverse CGroup (injection (inverse a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (Group.inverse CGroup ((-C injection a) +C (-C c))) }} {record { converges = CauchyCompletion.converges (injection a +C c) }} (inverseWellDefined CGroup {record { converges = CauchyCompletion.converges (injection (inverse a) +C (-C c)) }} {record { converges = CauchyCompletion.converges ((-C (injection a)) +C (-C c)) }} (Group.+WellDefinedLeft CGroup {record { converges = CauchyCompletion.converges (injection (inverse a)) }} {record { converges = CauchyCompletion.converges (-C c) }} {record { converges = CauchyCompletion.converges (-C (injection a)) }} homRespectsInverse)) (lemma2 (injection a) c)) (lemma2 b c) (flip<C (cOrderRespectsAdditionLeft _ _ (Group.inverse CGroup c) (flipR<C a<b)))

  cOrderRespectsAddition : (a b : CauchyCompletion) → (a <C b) → (c : CauchyCompletion) → (a +C c) <C (b +C c)
  cOrderRespectsAddition a b record { i = i ; a<i = a<i ; i<b = i<b } c = SetoidPartialOrder.<Transitive <COrder (cOrderRespectsAdditionLeft a i c a<i) (cOrderRespectsAdditionRight i b c i<b)
--- a/Fields/FieldOfFractions/Addition.agda
+++ b/Fields/FieldOfFractions/Addition.agda
@@ -13,13 +13,11 @@ module Fields.FieldOfFractions.Addition {a b : _} {A : Set a} {S : Setoid {a} {b
 open import Fields.FieldOfFractions.Setoid I

 fieldOfFractionsPlus : fieldOfFractionsSet → fieldOfFractionsSet → fieldOfFractionsSet
-fieldOfFractionsPlus (record { num = a ; denom = b ; denomNonzero = b!=0 }) (record { num = c ; denom = d ; denomNonzero = d!=0 }) = record { num = ((a * d) + (b * c)) ; denom = b * d ; denomNonzero = ans }
-  where
-    open Setoid S
-    open Ring R
-    ans : ((b * d) ∼ Ring.0R R) → False
-    ans pr with IntegralDomain.intDom I pr
-    ans pr | f = exFalso (d!=0 (f b!=0))
+fieldOfFractionsSet.num (fieldOfFractionsPlus (record { num = a ; denom = b ; denomNonzero = b!=0 }) (record { num = c ; denom = d ; denomNonzero = d!=0 })) = (a * d) + (b * c)
+fieldOfFractionsSet.denom (fieldOfFractionsPlus (record { num = a ; denom = b ; denomNonzero = b!=0 }) (record { num = c ; denom = d ; denomNonzero = d!=0 })) = b * d
+fieldOfFractionsSet.denomNonzero (fieldOfFractionsPlus (record { num = a ; denom = b ; denomNonzero = b!=0 }) (record { num = c ; denom = d ; denomNonzero = d!=0 })) = λ pr → exFalso (d!=0 (IntegralDomain.intDom I pr b!=0))
+
+--record { num = ((a * d) + (b * c)) ; denom = b * d ; denomNonzero = λ pr → exFalso (d!=0 (IntegralDomain.intDom I pr b!=0)) }

 plusWellDefined : {a b c d : fieldOfFractionsSet} → (Setoid._∼_ fieldOfFractionsSetoid a c) → (Setoid._∼_ fieldOfFractionsSetoid b d) → Setoid._∼_ fieldOfFractionsSetoid (fieldOfFractionsPlus a b) (fieldOfFractionsPlus c d)
 plusWellDefined {record { num = a ; denom = b ; denomNonzero = b!=0 }} {record { num = c ; denom = d ; denomNonzero = d!=0 }} {record { num = e ; denom = f ; denomNonzero = f!=0 }} {record { num = g ; denom = h ; denomNonzero = h!=0 }} af=be ch=dg = need
--- a/Fields/FieldOfFractions/Archimedean.agda
+++ b/Fields/FieldOfFractions/Archimedean.agda
@@ -14,7 +14,7 @@ open import Rings.Orders.Partial.Definition
 open import Rings.Orders.Total.Definition
 open import Groups.Orders.Archimedean

-module Fields.FieldOfFractions.Archimedean {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) {c : _} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (nonempty : (Setoid._∼_ S (Ring.0R R) (Ring.1R R)) → False) where
+module Fields.FieldOfFractions.Archimedean {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (I : IntegralDomain R) {c : _} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) where

 open import Groups.Cyclic.Definition
 open import Fields.FieldOfFractions.Setoid I
@@ -23,9 +23,9 @@ open import Fields.FieldOfFractions.Addition I
 open import Fields.FieldOfFractions.Ring I
 open import Fields.FieldOfFractions.Order I order
 open import Fields.FieldOfFractions.Field I
-open import Fields.Orders.Total.Archimedean
+open import Fields.Orders.Partial.Archimedean {F = fieldOfFractions} record { oRing = fieldOfFractionsPOrderedRing }
 open import Rings.Orders.Partial.Lemmas pRing
-open import Rings.Orders.Total.Lemmas order
+open import Rings.Orders.Total.Lemmas

 open Setoid S
 open Equivalence eq
@@ -48,21 +48,33 @@ private

  simpPower : (n : ℕ) → Setoid._∼_ fieldOfFractionsSetoid (positiveEltPower fieldOfFractionsGroup record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I} n) record { num = positiveEltPower (Ring.additiveGroup R) (Ring.1R R) n ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }
  simpPower zero = Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) {Group.0G fieldOfFractionsGroup}
-  simpPower (succ n) = Equivalence.transitive (Setoid.eq fieldOfFractionsSetoid) {record { denomNonzero = d (fieldOfFractionsPlus (record { num = 1R ; denom = 1R ; denomNonzero = λ t → nonempty (symmetric t) }) (positiveEltPower fieldOfFractionsGroup _ n)) }} {record { denomNonzero = λ t → nonempty (symmetric (transitive (symmetric identIsIdent) t)) }} {record { denomNonzero = λ t → nonempty (symmetric t) }} (Group.+WellDefined fieldOfFractionsGroup {record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }} {positiveEltPower fieldOfFractionsGroup record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I } n} {record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }} {record { num = positiveEltPower (Ring.additiveGroup R) (Ring.1R R) n ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }} (Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) {record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I}}) (simpPower n)) (transitive (transitive (transitive *Commutative (transitive identIsIdent (+WellDefined identIsIdent identIsIdent))) (symmetric identIsIdent)) (*WellDefined (symmetric identIsIdent) reflexive))
+  simpPower (succ n) = Equivalence.transitive (Setoid.eq fieldOfFractionsSetoid) {record { denomNonzero = d (fieldOfFractionsPlus (record { num = 1R ; denom = 1R ; denomNonzero = λ t → IntegralDomain.nontrivial I t }) (positiveEltPower fieldOfFractionsGroup _ n)) }} {record { denomNonzero = λ t → IntegralDomain.nontrivial I (transitive (symmetric identIsIdent) t) }} {record { denomNonzero = IntegralDomain.nontrivial I }} (Group.+WellDefined fieldOfFractionsGroup {record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }} {positiveEltPower fieldOfFractionsGroup record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I } n} {record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }} {record { num = positiveEltPower (Ring.additiveGroup R) (Ring.1R R) n ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I }} (Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) {record { num = Ring.1R R ; denom = Ring.1R R ; denomNonzero = IntegralDomain.nontrivial I}}) (simpPower n)) (transitive (transitive (transitive *Commutative (transitive identIsIdent (+WellDefined identIsIdent identIsIdent))) (symmetric identIsIdent)) (*WellDefined (symmetric identIsIdent) reflexive))

  lemma : (n : ℕ) {num denom : A} .(d!=0 : denom ∼ 0G → False) → (num * denom) < positiveEltPower additiveGroup 1R n → fieldOfFractionsComparison (record { num = num ; denom = denom ; denomNonzero = d!=0}) record { num = positiveEltPower additiveGroup (Ring.1R R) n ; denom = 1R ; denomNonzero = IntegralDomain.nontrivial I }
  lemma n {num} {denom} d!=0 numdenom<n with totality 0G denom
  ... | inl (inl 0<denom) with totality 0G 1R
  ... | inl (inl 0<1) = {!!}
-  ... | inl (inr x) = exFalso (1<0False x)
-  ... | inr x = exFalso (nonempty x)
+  ... | inl (inr x) = exFalso (1<0False order x)
+  ... | inr x = exFalso (IntegralDomain.nontrivial I (symmetric x))
  lemma n {num} {denom} d!=0 numdenom<n | inl (inr denom<0) with totality 0G 1R
  ... | inl (inl 0<1) = {!!}
-  ... | inl (inr 1<0) = exFalso (1<0False 1<0)
-  ... | inr 0=1 = exFalso (nonempty 0=1)
+  ... | inl (inr 1<0) = exFalso (1<0False order 1<0)
+  ... | inr 0=1 = exFalso (IntegralDomain.nontrivial I (symmetric 0=1))
  lemma n {num} {denom} d!=0 numdenom<n | inr 0=denom = exFalso (d!=0 (symmetric 0=denom))

-fieldOfFractionsArchimedean : Archimedean (toGroup R pRing) → ArchimedeanField {F = fieldOfFractions} record { oRing = fieldOfFractionsOrderedRing }
-fieldOfFractionsArchimedean arch (record { num = num ; denom = denom ; denomNonzero = denom!=0 }) with arch (num * denom) {!!} {!!} {!!}
-... | bl = {!!}
+fieldOfFractionsArchimedean : Archimedean (toGroup R pRing) → ArchimedeanField
+fieldOfFractionsArchimedean arch (record { num = num ; denom = denom ; denomNonzero = denom!=0 }) 0<q with totality 0G denom ,, totality 0G 1R
+... | inl (inl 0<denom) ,, inl (inl 0<1) rewrite refl { x = 0} = {!!}
+... | inl (inl 0<denom) ,, inl (inr x) = exFalso {!!}
+... | inl (inl 0<denom) ,, inr x = exFalso {!!}
+... | inl (inr denom<0) ,, inl (inl 0<1) = 0 , {!!}
+  where
+    t : {!!}
+    t = {!!}
+... | inl (inr denom<0) ,, inl (inr x) = exFalso {!!}
+... | inl (inr denom<0) ,, inr x = exFalso {!!}
+... | inr x ,, snd = exFalso (denom!=0 (symmetric x))
 --... | N , pr = N , SetoidPartialOrder.<WellDefined fieldOfFractionsOrder {record { denomNonzero = denom!=0 }} {record { denomNonzero = denom!=0 }} {record { denomNonzero = λ t → nonempty (symmetric t) }} {record { denomNonzero = d (positiveEltPower fieldOfFractionsGroup record { num = 1R ; denom = 1R ; denomNonzero = λ t → nonempty (symmetric t) } N) }} (Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) { record { denomNonzero = denom!=0 } }) (Equivalence.symmetric (Setoid.eq fieldOfFractionsSetoid) {record { denomNonzero = λ t → d (positiveEltPower fieldOfFractionsGroup record { num = 1R ; denom = 1R ; denomNonzero = λ t → nonempty (symmetric t) } N) t }} {record { denomNonzero = λ t → nonempty (symmetric t) }} (simpPower N)) (lemma N denom!=0 pr)
+
+fieldOfFractionsArchimedean' : Archimedean (toGroup R pRing) → Archimedean (toGroup fieldOfFractionsRing fieldOfFractionsPOrderedRing)
+fieldOfFractionsArchimedean' arch = archFieldToGrp (reciprocalPositive fieldOfFractionsOrderedRing) (fieldOfFractionsArchimedean arch)
--- a/Fields/FieldOfFractions/Order.agda
+++ b/Fields/FieldOfFractions/Order.agda
@@ -27,6 +27,17 @@ open SetoidTotalOrder (TotallyOrderedRing.total order)
 open import Rings.Orders.Partial.Lemmas
 open PartiallyOrderedRing pRing

+fieldOfFractionsComparison : Rel fieldOfFractionsSet
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) with (totality (Ring.0R R) denomA ,, totality (Ring.0R R) denomB)
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inl 0<denomA) ,, inl (inl 0<denomB) = (numA * denomB) < (numB * denomA)
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inl 0<denomA) ,, inl (inr denomB<0) = (numB * denomA) < (numA * denomB)
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inl 0<denomA) ,, inr 0=denomB = exFalso (denomB!=0 (symmetric 0=denomB))
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inr denomA<0) ,, inl (inl 0<denomB) = (numB * denomA) < (numA * denomB)
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inr denomA<0) ,, inl (inr denomB<0) = (numA * denomB) < (numB * denomA)
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inr denomA<0) ,, inr 0=denomB = exFalso (denomB!=0 (symmetric 0=denomB))
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inr 0=denomA ,, _ = exFalso (denomA!=0 (symmetric 0=denomA))
+
+{-
 fieldOfFractionsComparison : Rel fieldOfFractionsSet
 fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) with totality (Ring.0R R) denomA
 fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inl 0<denomA) with totality (Ring.0R R) denomB
@@ -38,6 +49,18 @@ fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero
 fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inr denomA<0) | inl (inr denomB<0) = (numA * denomB) < (numB * denomA)
 fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inr denomA<0) | inr 0=denomB = exFalso (denomB!=0 (symmetric 0=denomB))
 fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inr 0=denomA = exFalso (denomA!=0 (symmetric 0=denomA))
+fieldOfFractionsComparison : Rel fieldOfFractionsSet
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) with totality (Ring.0R R) denomA
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inl 0<denomA) with totality (Ring.0R R) denomB
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inl 0<denomA) | inl (inl 0<denomB) = (numA * denomB) < (numB * denomA)
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inl 0<denomA) | inl (inr denomB<0) = (numB * denomA) < (numA * denomB)
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inl 0<denomA) | inr 0=denomB = exFalso (denomB!=0 (symmetric 0=denomB))
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inr denomA<0) with totality (Ring.0R R) denomB
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inr denomA<0) | inl (inl 0<denomB) = (numB * denomA) < (numA * denomB)
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inr denomA<0) | inl (inr denomB<0) = (numA * denomB) < (numB * denomA)
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inl (inr denomA<0) | inr 0=denomB = exFalso (denomB!=0 (symmetric 0=denomB))
+fieldOfFractionsComparison (record { num = numA ; denom = denomA ; denomNonzero = denomA!=0 }) (record { num = numB ; denom = denomB ; denomNonzero = denomB!=0 }) | inr 0=denomA = exFalso (denomA!=0 (symmetric 0=denomA))
+-}

 private
  abstract
--- a/Fields/Orders/Partial/Archimedean.agda
+++ b/Fields/Orders/Partial/Archimedean.agda
@@ -0,0 +1,58 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import Sets.EquivalenceRelations
+open import Numbers.Naturals.Semiring
+open import Numbers.Integers.Definition
+open import Numbers.Naturals.Order
+open import LogicalFormulae
+open import Groups.Definition
+open import Rings.Orders.Partial.Definition
+open import Setoids.Orders.Partial.Definition
+open import Setoids.Setoids
+open import Functions
+open import Rings.Definition
+open import Fields.Fields
+open import Fields.Orders.Partial.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Fields.Orders.Partial.Archimedean {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {_<_ : A → A → Set c} {pOrder : SetoidPartialOrder S _<_} {F : Field R} (p : PartiallyOrderedField F pOrder) where
+
+open Setoid S
+open Equivalence eq
+open Ring R
+open Group additiveGroup
+open import Groups.Lemmas additiveGroup
+open import Groups.Cyclic.Definition additiveGroup
+open import Groups.Cyclic.DefinitionLemmas additiveGroup
+open import Groups.Orders.Archimedean (toGroup R (PartiallyOrderedField.oRing p))
+open import Rings.Orders.Partial.Lemmas (PartiallyOrderedField.oRing p)
+open import Rings.InitialRing R
+open SetoidPartialOrder pOrder
+open PartiallyOrderedRing (PartiallyOrderedField.oRing p)
+open Field F
+
+ArchimedeanField : Set (a ⊔ c)
+ArchimedeanField = (x : A) → (0R < x) → Sg ℕ (λ n → x < (fromN n))
+
+private
+  lemma : (r : A) (N : ℕ) → (positiveEltPower 1R N * r) ∼ positiveEltPower r N
+  lemma r zero = timesZero'
+  lemma r (succ n) = transitive *DistributesOver+' (+WellDefined identIsIdent (lemma r n))
+
+  findBound : (0<1 : 0R < 1R) → (r s : A) (N : ℕ) → (1R < r) → (s < positiveEltPower 1R N) → s < positiveEltPower r N
+  findBound _ r s zero 1<r s<N = s<N
+  findBound 0<1 r s (succ N) 1<r s<N = <Transitive s<N (<WellDefined (transitive *Commutative identIsIdent) (lemma r (succ N)) (ringCanMultiplyByPositive' (fromNPreservesOrder 0<1 (succIsPositive N)) 1<r))
+
+archFieldToGrp : ((x y : A) → .(0R < x) → (x * y) ∼ 1R → 0R < y) → ArchimedeanField → Archimedean
+archFieldToGrp reciprocalPositive a r s 0<r 0<s with allInvertible r (λ r=0 → irreflexive (<WellDefined reflexive r=0 0<r))
+... | inv , prInv with a inv (reciprocalPositive r inv 0<r (transitive *Commutative prInv))
+... | N , invBound with a s 0<s
+... | Ns , nSBound = (Ns *N N) , <WellDefined reflexive (symmetric (elementPowerMultiplies (nonneg Ns) (nonneg N) r)) (findBound (<WellDefined reflexive (transitive *Commutative prInv) (orderRespectsMultiplication 0<r (reciprocalPositive r inv 0<r (transitive *Commutative prInv)))) (positiveEltPower r N) s Ns m nSBound)
+  where
+    m : 1R < positiveEltPower r N
+    m = <WellDefined prInv (lemma r N) (ringCanMultiplyByPositive 0<r invBound)
+
+archToArchField : 0R < 1R → Archimedean → ArchimedeanField
+archToArchField 0<1 arch a 0<a with arch 1R a 0<1 0<a
+... | N , pr = N , pr
--- a/Fields/Orders/Total/Archimedean.agda
+++ b/Fields/Orders/Total/Archimedean.agda
@@ -14,11 +14,11 @@ open import Setoids.Setoids
 open import Functions
 open import Rings.Definition
 open import Fields.Fields
-open import Fields.Orders.Total.Definition
+open import Fields.Orders.Partial.Definition

 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

-module Fields.Orders.Total.Archimedean {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {_<_ : A → A → Set c} {pOrder : SetoidPartialOrder S _<_} {p : PartiallyOrderedRing R pOrder} {F : Field R} (t : TotallyOrderedField F p) where
+module Fields.Orders.Total.Archimedean {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {_<_ : A → A → Set c} {pOrder : SetoidPartialOrder S _<_} {F : Field R} (p : PartiallyOrderedField F pOrder) where

 open Setoid S
 open Equivalence eq
@@ -27,13 +27,11 @@ open Group additiveGroup
 open import Groups.Lemmas additiveGroup
 open import Groups.Cyclic.Definition additiveGroup
 open import Groups.Cyclic.DefinitionLemmas additiveGroup
-open import Groups.Orders.Archimedean (toGroup R p)
-open import Rings.Orders.Partial.Lemmas p
+open import Groups.Orders.Archimedean (toGroup R (PartiallyOrderedField.oRing p))
+open import Rings.Orders.Partial.Lemmas (PartiallyOrderedField.oRing p)
 open import Rings.InitialRing R
 open SetoidPartialOrder pOrder
-open PartiallyOrderedRing p
-open SetoidTotalOrder (TotallyOrderedRing.total (TotallyOrderedField.oRing t))
-open import Rings.Orders.Total.Lemmas (TotallyOrderedField.oRing t)
+open PartiallyOrderedRing (PartiallyOrderedField.oRing p)
 open Field F

 ArchimedeanField : Set (a ⊔ c)
@@ -44,22 +42,19 @@ private
  lemma r zero = timesZero'
  lemma r (succ n) = transitive *DistributesOver+' (+WellDefined identIsIdent (lemma r n))

-  findBound : (r s : A) (N : ℕ) → (1R < r) → (s < positiveEltPower 1R N) → s < positiveEltPower r N
-  findBound r s zero 1<r s<N = s<N
-  findBound r s (succ N) 1<r s<N = <Transitive s<N (<WellDefined (transitive *Commutative identIsIdent) (lemma r (succ N)) (ringCanMultiplyByPositive' (fromNPreservesOrder (0<1 (anyComparisonImpliesNontrivial 1<r)) (succIsPositive N)) 1<r))
+  findBound : (0<1 : 0R < 1R) → (r s : A) (N : ℕ) → (1R < r) → (s < positiveEltPower 1R N) → s < positiveEltPower r N
+  findBound _ r s zero 1<r s<N = s<N
+  findBound 0<1 r s (succ N) 1<r s<N = <Transitive s<N (<WellDefined (transitive *Commutative identIsIdent) (lemma r (succ N)) (ringCanMultiplyByPositive' (fromNPreservesOrder 0<1 (succIsPositive N)) 1<r))

-archFieldToGrp : ArchimedeanField → Archimedean
-archFieldToGrp a r s 0<r 0<s with totality r s
-archFieldToGrp a r s 0<r 0<s | inl (inr s<r) = 1 , <WellDefined reflexive (symmetric identRight) s<r
-archFieldToGrp a r s 0<r 0<s | inr r=s = 2 , <WellDefined (transitive identLeft r=s) (+WellDefined reflexive (symmetric identRight)) (orderRespectsAddition 0<r r)
-... | inl (inl r<s) with allInvertible r (λ r=0 → irreflexive (<WellDefined reflexive r=0 0<r))
+archFieldToGrp : ((x y : A) → 0R < x → (x * y) ∼ 1R → 0R < y) → ArchimedeanField → Archimedean
+archFieldToGrp reciprocalPositive a r s 0<r 0<s with allInvertible r (λ r=0 → irreflexive (<WellDefined reflexive r=0 0<r))
 ... | inv , prInv with a inv (reciprocalPositive r inv 0<r (transitive *Commutative prInv))
 ... | N , invBound with a s 0<s
-... | Ns , nSBound = (Ns *N N) , <WellDefined reflexive (symmetric (elementPowerMultiplies (nonneg Ns) (nonneg N) r)) (findBound (positiveEltPower r N) s Ns m nSBound)
+... | Ns , nSBound = (Ns *N N) , <WellDefined reflexive (symmetric (elementPowerMultiplies (nonneg Ns) (nonneg N) r)) (findBound (<WellDefined reflexive (transitive *Commutative prInv) (orderRespectsMultiplication 0<r (reciprocalPositive r inv 0<r (transitive *Commutative prInv)))) (positiveEltPower r N) s Ns m nSBound)
  where
    m : 1R < positiveEltPower r N
    m = <WellDefined prInv (lemma r N) (ringCanMultiplyByPositive 0<r invBound)

-archToArchField : Archimedean → ArchimedeanField
-archToArchField arch a 0<a with arch 1R a (0<1 (anyComparisonImpliesNontrivial 0<a)) 0<a
+archToArchField : 0R < 1R → Archimedean → ArchimedeanField
+archToArchField 0<1 arch a 0<a with arch 1R a 0<1 0<a
 ... | N , pr = N , pr
--- a/Groups/Definition.agda
+++ b/Groups/Definition.agda
@@ -1,5 +1,6 @@
 {-# OPTIONS --safe --warning=error --without-K #-}

+open import Sets.EquivalenceRelations
 open import Setoids.Setoids
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

@@ -16,3 +17,9 @@ record Group {lvl1 lvl2} {A : Set lvl1} (S : Setoid {lvl1} {lvl2} A) (_·_ : A
    identLeft : {a : A} → (0G · a) ∼ a
    invLeft : {a : A} → (inverse a) · a ∼ 0G
    invRight : {a : A} → a · (inverse a) ∼ 0G
+  +Associative' : {a b c : A} → ((a · b) · c) ∼ (a · (b · c))
+  +Associative' = Equivalence.symmetric (Setoid.eq S) +Associative
+  +WellDefinedLeft : {m x n : A} → (m ∼ n) → (m · x) ∼ (n · x)
+  +WellDefinedLeft m=n = +WellDefined m=n (Equivalence.reflexive (Setoid.eq S))
+  +WellDefinedRight : {m x y : A} → (x ∼ y) → (m · x) ∼ (m · y)
+  +WellDefinedRight x=y = +WellDefined (Equivalence.reflexive (Setoid.eq S)) x=y
--- a/Groups/FreeGroup/Definition.agda
+++ b/Groups/FreeGroup/Definition.agda
@@ -10,6 +10,7 @@ open import Sets.FinSet.Definition
 open import Groups.Definition
 open import Groups.SymmetricGroups.Definition
 open import Decidable.Sets
+open import Boolean.Definition

 module Groups.FreeGroup.Definition where

--- a/Groups/FreeGroup/Parity.agda
+++ b/Groups/FreeGroup/Parity.agda
@@ -11,6 +11,7 @@ open import LogicalFormulae
 open import Semirings.Definition
 open import Functions
 open import Groups.Isomorphisms.Definition
+open import Boolean.Definition

 module Groups.FreeGroup.Parity {a : _} {A : Set a} (decA : DecidableSet A) where

--- a/Groups/FreeGroup/Word.agda
+++ b/Groups/FreeGroup/Word.agda
@@ -7,6 +7,7 @@ open import Decidable.Sets
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import LogicalFormulae
+open import Boolean.Definition

 module Groups.FreeGroup.Word {a : _} {A : Set a} (decA : DecidableSet A) where

--- a/LectureNotes/MetAndTop/Chapter1.agda
+++ b/LectureNotes/MetAndTop/Chapter1.agda
@@ -2,6 +2,7 @@

 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω)

+open import Boolean.Definition
 open import Setoids.Setoids
 open import Setoids.Subset
 open import Setoids.Functions.Definition
--- a/Lists/Filter/AllTrue.agda
+++ b/Lists/Filter/AllTrue.agda
@@ -4,6 +4,7 @@ open import LogicalFormulae
 open import Functions
 open import Lists.Definition
 open import Lists.Monad
+open import Boolean.Definition

 module Lists.Filter.AllTrue where

--- a/Logic/PropositionalAxiomsTautology.agda
+++ b/Logic/PropositionalAxiomsTautology.agda
@@ -6,6 +6,7 @@ open import Logic.PropositionalLogic
 open import Functions
 open import Numbers.Naturals.Naturals
 open import Vectors
+open import Boolean.Definition

 module Logic.PropositionalAxiomsTautology where

--- a/Logic/PropositionalLogic.agda
+++ b/Logic/PropositionalLogic.agda
@@ -3,6 +3,7 @@
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import LogicalFormulae
 open import Functions
+open import Boolean.Definition

 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
--- a/Logic/PropositionalLogicExamples.agda
+++ b/Logic/PropositionalLogicExamples.agda
@@ -1,5 +1,6 @@
 {-# OPTIONS --safe --warning=error #-}

+open import Boolean.Definition
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import LogicalFormulae
 open import Logic.PropositionalLogic
--- a/LogicalFormulae.agda
+++ b/LogicalFormulae.agda
@@ -22,13 +22,6 @@ data _||_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inl : A → A || B
  inr : B → A || B

-data Bool : Set where
-  BoolTrue : Bool
-  BoolFalse : Bool
-{-# BUILTIN BOOL  Bool  #-}
-{-# BUILTIN TRUE  BoolTrue  #-}
-{-# BUILTIN FALSE BoolFalse #-}
-
 infix 15 _&&_
 record _&&_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,,_
@@ -94,22 +87,6 @@ lemConstructive (inr notP) = λ negnegP → exFalso (negnegP notP)
 lemConverse : {n : _} → {p : Set n} → p → ((p → False) → False)
 lemConverse p = λ notP → notP p

-if_then_else_ : {a : _} → {A : Set a} → Bool → A → A → A
-if BoolTrue then tr else fls = tr
-if BoolFalse then tr else fls = fls
-
-not : Bool → Bool
-not BoolTrue = BoolFalse
-not BoolFalse = BoolTrue
-
-boolAnd : Bool → Bool → Bool
-boolAnd BoolTrue y = y
-boolAnd BoolFalse y = BoolFalse
-
-boolOr : Bool → Bool → Bool
-boolOr BoolTrue y = BoolTrue
-boolOr BoolFalse y = y
-
 typeCast : {a : _} {A : Set a} {B : Set a} (el : A) (pr : A ≡ B) → B
 typeCast {a} {A} {.A} elt refl = elt

--- a/Modules/Examples.agda
+++ b/Modules/Examples.agda
@@ -1,5 +1,6 @@
 {-# OPTIONS --safe --warning=error --without-K #-}

+open import Boolean.Definition
 open import Sets.FinSet.Definition
 open import LogicalFormulae
 open import Groups.Abelian.Definition
--- a/Numbers/Naturals/Definition.agda
+++ b/Numbers/Naturals/Definition.agda
@@ -1,5 +1,6 @@
 {-# OPTIONS --warning=error --safe --without-K #-}

+open import Boolean.Definition
 open import LogicalFormulae
 open import Decidable.Lemmas

--- a/Numbers/Naturals/Naturals.agda
+++ b/Numbers/Naturals/Naturals.agda
@@ -98,14 +98,6 @@ lessImpliesNotEqual {a} {.a} prAB refl = TotalOrder.irreflexive ℕTotalOrder pr
 -NIsDecreasing {a} {b} prAB with (-N (inl prAB))
 -NIsDecreasing {a} {b} (le x proof) | record { result = result ; pr = pr } = record { x = a ; proof = pr }

-equalityN : (a b : ℕ) → Sg Bool (λ truth → if truth then a ≡ b else True)
-equalityN zero zero = ( BoolTrue , refl )
-equalityN zero (succ b) = ( BoolFalse , record {} )
-equalityN (succ a) zero = ( BoolFalse , record {} )
-equalityN (succ a) (succ b) with equalityN a b
-equalityN (succ a) (succ b) | BoolTrue , val = (BoolTrue , applyEquality succ val)
-equalityN (succ a) (succ b) | BoolFalse , val = (BoolFalse , record {})
-
 sumZeroImpliesSummandsZero : {a b : ℕ} → (a +N b ≡ zero) → ((a ≡ zero) && (b ≡ zero))
 sumZeroImpliesSummandsZero {zero} {zero} pr = record { fst = refl ; snd = refl }
 sumZeroImpliesSummandsZero {zero} {(succ b)} pr = record { fst = refl ; snd = pr }
--- a/Rings/Orders/Total/Lemmas.agda
+++ b/Rings/Orders/Total/Lemmas.agda
@@ -185,6 +185,9 @@ reciprocalPositive a 1/a 0<a ab=1 with totality 0G 1/a
 ... | inl (inr x) = exFalso (1<0False (<WellDefined (transitive *Commutative ab=1) timesZero' (ringCanMultiplyByPositive 0<a x)))
 ... | inr x = exFalso (anyComparisonImpliesNontrivial 0<a (transitive (transitive (symmetric timesZero) (*WellDefined reflexive x)) ab=1))

+reciprocalPositive' : (a b : A) → .(0<a : 0R < a) → (b * a ∼ 1R) → 0R < b
+reciprocalPositive' a 1/a 0<a ab=1 = reciprocalPositive a 1/a 0<a (transitive *Commutative ab=1)
+
 reciprocal<1 : (a b : A) → .(1<a : 1R < a) → (a * b ∼ 1R) → b < 1R
 reciprocal<1 a b 0<a ab=1 with totality b 1R
 ... | inl (inl x) = x
--- a/Setoids/Orders/Partial/Definition.agda
+++ b/Setoids/Orders/Partial/Definition.agda
@@ -1,5 +1,6 @@
 {-# OPTIONS --safe --warning=error --without-K #-}

+open import Sets.EquivalenceRelations
 open import LogicalFormulae
 open import Orders.Total.Definition
 open import Orders.Partial.Definition
@@ -18,6 +19,11 @@ record SetoidPartialOrder {a b c : _} {A : Set a} (S : Setoid {a} {b} A) (_<_ :
    <Transitive : {a b c : A} → (a < b) → (b < c) → (a < c)
  _<=_ : Rel {a} {b ⊔ c} A
  a <= b = (a < b) || (a ∼ b)
+  <=Transitive : {a b c : A} → (a <= b) → (b <= c) → (a <= c)
+  <=Transitive (inl a<b) (inl b<c) = inl (<Transitive a<b b<c)
+  <=Transitive (inl a<b) (inr b=c) = inl (<WellDefined (Equivalence.reflexive eq) b=c a<b)
+  <=Transitive (inr a=b) (inl b<c) = inl (<WellDefined (Equivalence.symmetric eq a=b) (Equivalence.reflexive eq) b<c)
+  <=Transitive (inr a=b) (inr b=c) = inr (Equivalence.transitive eq a=b b=c)

 partialOrderToSetoidPartialOrder : {a b : _} {A : Set a} (P : PartialOrder {a} A {b}) → SetoidPartialOrder (reflSetoid A) (PartialOrder._<_ P)
 SetoidPartialOrder.<WellDefined (partialOrderToSetoidPartialOrder P) a=b c=d a<c rewrite a=b | c=d = a<c
--- a/Setoids/Orders/Partial/Sequences.agda
+++ b/Setoids/Orders/Partial/Sequences.agda
@@ -0,0 +1,51 @@
+{-# OPTIONS --safe --warning=error --without-K --guardedness #-}
+
+open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Order
+open import LogicalFormulae
+open import Orders.Total.Definition
+open import Orders.Partial.Definition
+open import Setoids.Setoids
+open import Functions
+open import Sequences
+open import Setoids.Orders.Partial.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Setoids.Orders.Partial.Sequences {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_<_ : Rel {a} {c} A} (p : SetoidPartialOrder S _<_) where
+
+open SetoidPartialOrder p
+
+WeaklyIncreasing' : (Sequence A) → Set (b ⊔ c)
+WeaklyIncreasing' s = (m n : ℕ) → (m <N n) → (index s m) <= (index s n)
+
+WeaklyIncreasing : (Sequence A) → Set (b ⊔ c)
+WeaklyIncreasing s = (m : ℕ) → (index s m) <= index s (succ m)
+
+tailRespectsWeaklyIncreasing : (a : Sequence A) → WeaklyIncreasing a → WeaklyIncreasing (Sequence.tail a)
+tailRespectsWeaklyIncreasing a incr m = incr (succ m)
+
+weaklyIncreasingImplies' : (a : Sequence A) → WeaklyIncreasing a → WeaklyIncreasing' a
+weaklyIncreasingImplies' a x zero (succ zero) m<n = x 0
+weaklyIncreasingImplies' a x zero (succ (succ n)) m<n = <=Transitive (weaklyIncreasingImplies' a x zero (succ n) (succIsPositive n)) (x (succ n))
+weaklyIncreasingImplies' a x (succ m) (succ n) m<n = weaklyIncreasingImplies' (Sequence.tail a) (tailRespectsWeaklyIncreasing a x) m n (canRemoveSuccFrom<N m<n)
+
+weaklyIncreasing'Implies : (a : Sequence A) → WeaklyIncreasing' a → WeaklyIncreasing a
+weaklyIncreasing'Implies a incr m = incr m (succ m) (le 0 refl)
+
+StrictlyIncreasing' : (Sequence A) → Set (c)
+StrictlyIncreasing' s = (m n : ℕ) → (m <N n) → (index s m) < (index s n)
+
+StrictlyIncreasing : (Sequence A) → Set (c)
+StrictlyIncreasing s = (m : ℕ) → (index s m) < index s (succ m)
+
+tailRespectsStrictlyIncreasing : (a : Sequence A) → StrictlyIncreasing a → StrictlyIncreasing (Sequence.tail a)
+tailRespectsStrictlyIncreasing a incr m = incr (succ m)
+
+strictlyIncreasingImplies' : (a : Sequence A) → StrictlyIncreasing a → StrictlyIncreasing' a
+strictlyIncreasingImplies' a x zero (succ zero) m<n = x 0
+strictlyIncreasingImplies' a x zero (succ (succ n)) m<n = <Transitive (strictlyIncreasingImplies' a x zero (succ n) (succIsPositive n)) (x (succ n))
+strictlyIncreasingImplies' a x (succ m) (succ n) m<n = strictlyIncreasingImplies' (Sequence.tail a) (tailRespectsStrictlyIncreasing a x) m n (canRemoveSuccFrom<N m<n)
+
+strictlyIncreasing'Implies : (a : Sequence A) → StrictlyIncreasing' a → StrictlyIncreasing a
+strictlyIncreasing'Implies a incr m = incr m (succ m) (le 0 refl)