diff --git a/src/1Lab/Equiv.lagda.md b/src/1Lab/Equiv.lagda.md
index 89bff45ec..783681231 100644
--- a/src/1Lab/Equiv.lagda.md
+++ b/src/1Lab/Equiv.lagda.md
@@ -945,7 +945,7 @@ Lift-ap
Lift-ap (f , eqv) .fst (lift x) = lift (f x)
Lift-ap f .snd .is-eqv (lift y) .centre = lift (Equiv.from f y) , ap lift (Equiv.ε f y)
Lift-ap f .snd .is-eqv (lift y) .paths (lift x , q) i = lift (p i .fst) , λ j → lift (p i .snd j)
- where p = f .snd .is-eqv y .paths (x , ap Lift.lower q)
+ where p = f .snd .is-eqv y .paths (x , ap lower q)
```
### Involutions
@@ -1090,7 +1090,7 @@ syntax ≃⟨⟩-syntax x q p = x ≃⟨ p ⟩ q
lift-inj
: ∀ {ℓ ℓ'} {A : Type ℓ} {a b : A}
→ lift {ℓ = ℓ'} a ≡ lift {ℓ = ℓ'} b → a ≡ b
-lift-inj p = ap Lift.lower p
+lift-inj p = ap lower p
-- Fibres of composites are given by pairs of fibres.
fibre-∘-≃
diff --git a/src/1Lab/HLevel/Closure.lagda.md b/src/1Lab/HLevel/Closure.lagda.md
index 2c0a90224..d626fec0f 100644
--- a/src/1Lab/HLevel/Closure.lagda.md
+++ b/src/1Lab/HLevel/Closure.lagda.md
@@ -266,13 +266,13 @@ successor universe:
```agda
opaque
Lift-is-hlevel : ∀ n → is-hlevel A n → is-hlevel (Lift ℓ' A) n
- Lift-is-hlevel n a-hl = retract→is-hlevel n lift Lift.lower (λ _ → refl) a-hl
+ Lift-is-hlevel n a-hl = retract→is-hlevel n lift lower (λ _ → refl) a-hl
```
diff --git a/src/1Lab/HLevel/Universe.lagda.md b/src/1Lab/HLevel/Universe.lagda.md
index a7177e62f..2191c2a42 100644
--- a/src/1Lab/HLevel/Universe.lagda.md
+++ b/src/1Lab/HLevel/Universe.lagda.md
@@ -193,7 +193,7 @@ Prop ℓ = n-Type ℓ 1
```agda
¬Set-is-prop : ¬ is-prop (Set ℓ)
¬Set-is-prop prop =
- Lift.lower $
+ lower $
transport (ap ∣_∣ (prop (el (Lift _ ⊤) (hlevel 2)) (el (Lift _ ⊥) (hlevel 2)))) (lift tt)
```
-->
diff --git a/src/1Lab/Reflection/Deriving/Show.agda b/src/1Lab/Reflection/Deriving/Show.agda
index 99e9927b7..f3d740351 100644
--- a/src/1Lab/Reflection/Deriving/Show.agda
+++ b/src/1Lab/Reflection/Deriving/Show.agda
@@ -11,6 +11,7 @@ open import Data.Char.Base
open import Data.Fin.Base
open import Data.Vec.Base hiding (map)
open import Data.Nat.Base
+open import Data.Int.Base using (Int ; pos ; negsuc)
open import Meta.Foldable
open import Meta.Append
diff --git a/src/1Lab/Type.lagda.md b/src/1Lab/Type.lagda.md
index d0f4e1ad9..8543066e0 100644
--- a/src/1Lab/Type.lagda.md
+++ b/src/1Lab/Type.lagda.md
@@ -77,6 +77,8 @@ record Lift {a} ℓ (A : Type a) : Type (a ⊔ ℓ) where
@@ -93,9 +93,7 @@ give the unit, both on the left and on the right:
underlying-monoid = A , record
{ identity = unit ; _⋆_ = _*_ ; has-is-monoid = has-is-monoid }
- open Cat.Reasoning (B (underlying-monoid .snd))
- hiding (id ; assoc ; idl ; idr ; invr ; invl ; to ; from ; inverses ; _∘_)
- public
+ open Mon underlying-monoid public
```
-->
diff --git a/src/Algebra/Group/Ab/Sum.lagda.md b/src/Algebra/Group/Ab/Sum.lagda.md
index f2b0899cc..2d88deca7 100644
--- a/src/Algebra/Group/Ab/Sum.lagda.md
+++ b/src/Algebra/Group/Ab/Sum.lagda.md
@@ -3,10 +3,10 @@
open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
open import Algebra.Group.Ab
-open import Algebra.Prelude
open import Algebra.Group
open import Cat.Diagram.Product
+open import Cat.Prelude
```
-->
diff --git a/src/Algebra/Group/Action.lagda.md b/src/Algebra/Group/Action.lagda.md
index 62e949ddb..43a66ec19 100644
--- a/src/Algebra/Group/Action.lagda.md
+++ b/src/Algebra/Group/Action.lagda.md
@@ -3,13 +3,16 @@
open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
open import Algebra.Group.Solver
-open import Algebra.Prelude
open import Algebra.Group
open import Cat.Instances.Delooping
+open import Cat.Instances.Functor
open import Cat.Instances.Sets
+open import Cat.Diagram.Zero
+open import Cat.Prelude
import Cat.Functor.Reasoning as Functor-kit
+import Cat.Reasoning as Cat
```
-->
diff --git a/src/Algebra/Group/Cat/Base.lagda.md b/src/Algebra/Group/Cat/Base.lagda.md
index 2943014ab..722e70d41 100644
--- a/src/Algebra/Group/Cat/Base.lagda.md
+++ b/src/Algebra/Group/Cat/Base.lagda.md
@@ -1,7 +1,6 @@
diff --git a/src/Algebra/Group/Cat/Monadic.lagda.md b/src/Algebra/Group/Cat/Monadic.lagda.md
index 6c0df60e4..fa7af9e1f 100644
--- a/src/Algebra/Group/Cat/Monadic.lagda.md
+++ b/src/Algebra/Group/Cat/Monadic.lagda.md
@@ -2,7 +2,6 @@
```agda
open import Algebra.Group.Cat.Base
open import Algebra.Group.Free
-open import Algebra.Prelude
open import Algebra.Monoid
open import Algebra.Group
@@ -10,7 +9,9 @@ open import Cat.Functor.Adjoint.Monadic
open import Cat.Functor.Adjoint.Monad
open import Cat.Functor.Equivalence
open import Cat.Functor.Properties
+open import Cat.Functor.Adjoint
open import Cat.Diagram.Monad
+open import Cat.Prelude
import Algebra.Group.Cat.Base as Grp
diff --git a/src/Algebra/Group/Concrete/Semidirect.lagda.md b/src/Algebra/Group/Concrete/Semidirect.lagda.md
index c0d3e7787..d1545c260 100644
--- a/src/Algebra/Group/Concrete/Semidirect.lagda.md
+++ b/src/Algebra/Group/Concrete/Semidirect.lagda.md
@@ -4,9 +4,11 @@ open import Algebra.Group.Semidirect
open import Algebra.Group.Cat.Base
open import Algebra.Group.Concrete
open import Algebra.Group.Action
-open import Algebra.Prelude
open import Algebra.Group
+open import Cat.Univalent
+open import Cat.Prelude
+
open import Homotopy.Connectedness
open ConcreteGroup
diff --git a/src/Algebra/Group/Free/Product.lagda.md b/src/Algebra/Group/Free/Product.lagda.md
index f31e942f3..3075bc605 100644
--- a/src/Algebra/Group/Free/Product.lagda.md
+++ b/src/Algebra/Group/Free/Product.lagda.md
@@ -4,10 +4,13 @@ open import 1Lab.Reflection.Induction
open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
-open import Algebra.Prelude
open import Algebra.Group
open import Cat.Diagram.Colimit.Finite
+open import Cat.Diagram.Coproduct
+open import Cat.Diagram.Pushout
+open import Cat.Diagram.Zero
+open import Cat.Prelude
open Finitely-cocomplete
open is-group-hom
diff --git a/src/Algebra/Group/Instances/Cyclic.lagda.md b/src/Algebra/Group/Instances/Cyclic.lagda.md
index e45f16113..ec0aed61c 100644
--- a/src/Algebra/Group/Instances/Cyclic.lagda.md
+++ b/src/Algebra/Group/Instances/Cyclic.lagda.md
@@ -5,15 +5,16 @@ open import Algebra.Group.Instances.Integers
open import Algebra.Group.Cat.Base
open import Algebra.Group.Subgroup
open import Algebra.Group.Ab
-open import Algebra.Prelude
open import Algebra.Group
+open import Cat.Prelude
+
open import Data.Int.Divisible
open import Data.Int.Universal
open import Data.Fin.Closure
open import Data.Int.DivMod
open import Data.Fin
-open import Data.Int
+open import Data.Int hiding (Positive)
open import Data.Nat
open represents-subgroup
@@ -82,7 +83,7 @@ _·ℤ : ∀ (n : Nat) → normal-subgroup ℤ λ i → el (n ∣ℤ i) (∣ℤ-
where
x≡y+x-y : x ≡ y +ℤ (x -ℤ y)
x≡y+x-y =
- x ≡⟨ ℤ.insertl {h = y} (ℤ.inverser {x = y}) ⟩
+ x ≡⟨ ℤ.insertl {y} (ℤ.inverser {x = y}) ⟩
y +ℤ (negℤ y +ℤ x) ≡⟨ ap (y +ℤ_) (+ℤ-commutative (negℤ y) x) ⟩
y +ℤ (x -ℤ y) ∎
diff --git a/src/Algebra/Group/Instances/Dihedral.lagda.md b/src/Algebra/Group/Instances/Dihedral.lagda.md
index 436b5e0ee..ce6ae3c1b 100644
--- a/src/Algebra/Group/Instances/Dihedral.lagda.md
+++ b/src/Algebra/Group/Instances/Dihedral.lagda.md
@@ -6,7 +6,9 @@ open import Algebra.Group.Semidirect
open import Algebra.Group.Cat.Base
open import Algebra.Group.Action
open import Algebra.Group.Ab
-open import Algebra.Prelude
+
+open import Cat.Functor.Base
+open import Cat.Prelude
```
-->
diff --git a/src/Algebra/Group/Instances/Integers.lagda.md b/src/Algebra/Group/Instances/Integers.lagda.md
index 50718c63e..23df0c39e 100644
--- a/src/Algebra/Group/Instances/Integers.lagda.md
+++ b/src/Algebra/Group/Instances/Integers.lagda.md
@@ -2,14 +2,14 @@
```agda
open import Algebra.Group.Cat.Base
open import Algebra.Group.Ab
-open import Algebra.Prelude
open import Algebra.Group
open import Cat.Functor.Adjoint
+open import Cat.Prelude
open import Data.Int.Universal
open import Data.Nat.Order
-open import Data.Int
+open import Data.Int hiding (Positive)
open import Data.Nat
open is-group-hom
diff --git a/src/Algebra/Group/Semidirect.lagda.md b/src/Algebra/Group/Semidirect.lagda.md
index 97e1c7e2d..c79ae3b28 100644
--- a/src/Algebra/Group/Semidirect.lagda.md
+++ b/src/Algebra/Group/Semidirect.lagda.md
@@ -3,9 +3,10 @@
open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
open import Algebra.Group.Action
-open import Algebra.Prelude
open import Algebra.Group
+open import Cat.Prelude
+
open is-group-hom
open make-group
```
diff --git a/src/Algebra/Group/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md
index 06d14ac30..964e536b2 100644
--- a/src/Algebra/Group/Subgroup.lagda.md
+++ b/src/Algebra/Group/Subgroup.lagda.md
@@ -2,13 +2,13 @@
```agda
open import Algebra.Group.Cat.FinitelyComplete
open import Algebra.Group.Cat.Base
-open import Algebra.Prelude
open import Algebra.Group
open import Cat.Diagram.Equaliser.Kernel
open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Zero
+open import Cat.Prelude
open import Data.Power
diff --git a/src/Algebra/Magma.lagda.md b/src/Algebra/Magma.lagda.md
index c7a0e0cf3..21e49c610 100644
--- a/src/Algebra/Magma.lagda.md
+++ b/src/Algebra/Magma.lagda.md
@@ -64,7 +64,7 @@ binary operation `⋆`, on which no further laws are imposed.
underlying-set : Set ℓ
underlying-set = el _ has-is-set
- instance
+ opaque instance
magma-hlevel : ∀ {n} → H-Level A (2 + n)
magma-hlevel = basic-instance 2 has-is-set
diff --git a/src/Algebra/Magma/Unital/EckmannHilton.lagda.md b/src/Algebra/Magma/Unital/EckmannHilton.lagda.md
index 84d502ebc..5140eee04 100644
--- a/src/Algebra/Magma/Unital/EckmannHilton.lagda.md
+++ b/src/Algebra/Magma/Unital/EckmannHilton.lagda.md
@@ -5,6 +5,8 @@ open import 1Lab.Prelude
open import Algebra.Magma.Unital
open import Algebra.Semigroup
open import Algebra.Monoid
+
+open is-monoid
```
-->
diff --git a/src/Algebra/Monoid.lagda.md b/src/Algebra/Monoid.lagda.md
index fc71bf790..7b0fefe8f 100644
--- a/src/Algebra/Monoid.lagda.md
+++ b/src/Algebra/Monoid.lagda.md
@@ -46,7 +46,7 @@ record is-monoid (id : A) (_⋆_ : A → A → A) : Type (level-of A) where
idl : {x : A} → id ⋆ x ≡ x
idr : {x : A} → x ⋆ id ≡ x
-open is-monoid public
+open is-monoid
```
The condition of $(A, 0, \star)$ defining a monoid is a proposition, so
diff --git a/src/Algebra/Monoid/Category.lagda.md b/src/Algebra/Monoid/Category.lagda.md
index 20958c37d..f1b16ca9b 100644
--- a/src/Algebra/Monoid/Category.lagda.md
+++ b/src/Algebra/Monoid/Category.lagda.md
@@ -25,6 +25,7 @@ module Algebra.Monoid.Category where
```
open Precategory
open is-semigroup
+open is-monoid
open is-magma
open Monoid-hom
open Monoid-on
diff --git a/src/Algebra/Monoid/Reasoning.lagda.md b/src/Algebra/Monoid/Reasoning.lagda.md
new file mode 100644
index 000000000..d4ba9b81e
--- /dev/null
+++ b/src/Algebra/Monoid/Reasoning.lagda.md
@@ -0,0 +1,86 @@
+
+
+```agda
+module Algebra.Monoid.Reasoning {ℓ} (M : Monoid ℓ) where
+```
+
+# Reasoning combinators for monoids
+
+
+
+```agda
+id-comm : a * 1m ≡ 1m * a
+id-comm = idr ∙ sym idl
+
+id-comm-sym : 1m * a ≡ a * 1m
+id-comm-sym = idl ∙ sym idr
+
+module _ (p : x ≡ 1m) where
+ eliml : x * a ≡ a
+ eliml = ap₂ _*_ p refl ∙ idl
+
+ elimr : a * x ≡ a
+ elimr = ap₂ _*_ refl p ∙ idr
+
+ introl : a ≡ x * a
+ introl = sym eliml
+
+ intror : a ≡ a * x
+ intror = sym elimr
+
+module _ (p : x * y ≡ z) where
+ pulll : x * (y * a) ≡ z * a
+ pulll = associative ∙ ap₂ _*_ p refl
+
+ pullr : (a * x) * y ≡ a * z
+ pullr = sym associative ∙ ap₂ _*_ refl p
+
+module _ (p : z ≡ x * y) where
+ pushl : z * a ≡ x * (y * a)
+ pushl = sym (pulll (sym p))
+
+ pushr : a * z ≡ (a * x) * y
+ pushr = sym (pullr (sym p))
+
+module _ (p : w * x ≡ y * z) where
+ extendl : w * (x * a) ≡ y * (z * a)
+ extendl = pulll refl ∙ ap₂ _*_ p refl ∙ pullr refl
+
+ extendr : (a * w) * x ≡ (a * y) * z
+ extendr = pullr refl ∙ ap₂ _*_ refl p ∙ pulll refl
+
+module _ (p : x * y ≡ 1m) where
+ cancell : x * (y * a) ≡ a
+ cancell = pulll p ∙ idl
+
+ cancelr : (a * x) * y ≡ a
+ cancelr = pullr p ∙ idr
+
+ insertl : a ≡ x * (y * a)
+ insertl = sym cancell
+
+ insertr : a ≡ (a * x) * y
+ insertr = sym cancelr
+
+lswizzle : g ≡ h * i → f * h ≡ 1m → f * g ≡ i
+lswizzle p q = ap₂ _*_ refl p ∙ cancell q
+
+rswizzle : g ≡ i * h → h * f ≡ 1m → g * f ≡ i
+rswizzle p q = ap₂ _*_ p refl ∙ cancelr q
+
+swizzle : f * g ≡ h * i → g * g' ≡ 1m → h' * h ≡ 1m → h' * f ≡ i * g'
+swizzle p q r = lswizzle (sym (associative ∙ rswizzle (sym p) q)) r
+```
diff --git a/src/Algebra/Prelude.agda b/src/Algebra/Prelude.agda
deleted file mode 100644
index f43e9435d..000000000
--- a/src/Algebra/Prelude.agda
+++ /dev/null
@@ -1,31 +0,0 @@
-module Algebra.Prelude where
-
-open import Cat.Instances.Shape.Terminal public
-open import Cat.Functor.FullSubcategory public
-open import Cat.Instances.Product public
-open import Cat.Instances.Functor public
-open import Cat.Instances.Comma public
-open import Cat.Instances.Slice public
-open import Cat.Functor.Adjoint public
-open import Cat.Functor.Base public
-open import Cat.Functor.Hom public
-open import Cat.Univalent public
-open import Cat.Prelude hiding (_+_ ; _-_ ; _*_) public
-
-open import Cat.Diagram.Coequaliser public
-open import Cat.Diagram.Coproduct public
-open import Cat.Diagram.Equaliser public
-open import Cat.Diagram.Pullback public
-open import Cat.Diagram.Terminal public
-open import Cat.Diagram.Initial public
-open import Cat.Diagram.Pushout public
-open import Cat.Diagram.Product public
-open import Cat.Diagram.Image public
-open import Cat.Diagram.Zero public
-
-import Cat.Reasoning
-
-open import Cat.Displayed.Univalence.Thin public
-
-module Cat {o ℓ} (C : Precategory o ℓ) where
- open Cat.Reasoning C public
diff --git a/src/Algebra/Ring.lagda.md b/src/Algebra/Ring.lagda.md
index d3ebbfe8d..167777f48 100644
--- a/src/Algebra/Ring.lagda.md
+++ b/src/Algebra/Ring.lagda.md
@@ -1,18 +1,20 @@
@@ -72,7 +74,7 @@ record is-ring {ℓ} {R : Type ℓ} (1r : R) (_*_ _+_ : R → R → R) : Type
)
public
- additive-group : Group ℓ
+ additive-group : Σ (Set ℓ) (λ x → Group-on ⌞ x ⌟)
∣ additive-group .fst ∣ = R
additive-group .fst .is-tr = is-abelian-group.has-is-set +-group
additive-group .snd .Group-on._⋆_ = _+_
@@ -84,27 +86,13 @@ record is-ring {ℓ} {R : Type ℓ} (1r : R) (_*_ _+_ : R → R → R) : Type
group .snd .Abelian-group-on._*_ = _+_
group .snd .Abelian-group-on.has-is-ab = +-group
- Ringoid : Ab-category (B record { _⋆_ = _*_ ; has-is-monoid = *-monoid })
- Ringoid .Ab-category.Abelian-group-on-hom _ _ = record { has-is-ab = +-group }
- Ringoid .Ab-category.∘-linear-l f g h = sym *-distribr
- Ringoid .Ab-category.∘-linear-r f g h = sym *-distribl
-
- private
- module ringoid = Ab-category Ringoid
- using ( ∘-zero-l ; ∘-zero-r ; neg-∘-l ; neg-∘-r ; ∘-minus-l ; ∘-minus-r )
-
- open ringoid renaming
- ( ∘-zero-l to *-zerol
- ; ∘-zero-r to *-zeror
- ; neg-∘-l to neg-*-l
- ; neg-∘-r to neg-*-r
- ; ∘-minus-l to *-minus-l
- ; ∘-minus-r to *-minus-r
- )
- public
+ multiplicative-monoid : Monoid ℓ
+ multiplicative-monoid .fst = R
+ multiplicative-monoid .snd = record { has-is-monoid = *-monoid }
- module m = Cat.Reasoning (B record { _⋆_ = _*_ ; has-is-monoid = *-monoid })
+ module m = Mon multiplicative-monoid
module a = Abelian-group-on record { has-is-ab = +-group }
+ hiding (_*_ ; 1g ; _⁻¹)
record Ring-on {ℓ} (R : Type ℓ) : Type ℓ where
field
@@ -246,6 +234,7 @@ record make-ring {ℓ} (R : Type ℓ) : Type ℓ where
to-ring-on : Ring-on R
to-ring-on = ring where
open is-ring hiding (-_ ; +-invr ; +-invl ; *-distribl ; *-distribr ; *-idl ; *-idr ; +-idl ; +-idr)
+ open is-monoid
-- All in copatterns to prevent the unfolding from exploding on you
ring : Ring-on R
diff --git a/src/Algebra/Ring/Cat/Initial.lagda.md b/src/Algebra/Ring/Cat/Initial.lagda.md
index 0e77e0bf6..cf53b4bd0 100644
--- a/src/Algebra/Ring/Cat/Initial.lagda.md
+++ b/src/Algebra/Ring/Cat/Initial.lagda.md
@@ -1,14 +1,17 @@
@@ -69,13 +72,13 @@ prove...], so here it is:
```agda
Int-is-initial : is-initial (Rings ℓ) Liftℤ
Int-is-initial R = contr z→r λ x → ext (lemma x) where
- module R = Ring-on (R .snd)
+ module R = Kit R
```
Note that we treat 1 with care: we could have this map 1 to `1r + 0r`,
-but this results in worse definitional behaviour when actually using the embedding.
-This will result in a bit more work right now, but is work worth doing.
-
+but this results in worse definitional behaviour when actually using the
+embedding. This will result in a bit more work right now, but is work
+worth doing.
```agda
e : Nat → ⌞ R ⌟
@@ -142,78 +145,60 @@ this is a ring homomorphism... which involves a mountain of annoying
algebra, so I won't comment on it too much: it can be worked out on
paper, following the ring laws.
-Note that we special case `diff x 0` here for better definitional
-behaviour of the embedding.
-
```agda
-
ℤ↪R : Int → ⌞ R ⌟
- ℤ↪R (diff x zero) = e x
- ℤ↪R (diff x (suc y)) = e x R.- e (suc y)
- ℤ↪R (Int.quot m zero i) = along i $
- e m ≡⟨ R.intror R.+-invr ⟩
- e m R.+ (R.1r R.- R.1r) ≡⟨ R.+-associative ⟩
- (e m R.+ R.1r) R.- R.1r ≡⟨ ap (R._- R.1r) R.+-commutes ⟩
- (R.1r R.+ e m) R.- R.1r ≡˘⟨ ap (R._- R.1r) (e-suc m) ⟩
- e (suc m) R.- R.1r ∎
- ℤ↪R (Int.quot m (suc n) i) = e-tr m (suc n) i
+ ℤ↪R (pos x) = e x
+ ℤ↪R (negsuc x) = R.- (e (suc x))
open is-ring-hom
- ℤ↪R-diff : ∀ m n → ℤ↪R (diff m n) ≡ e m R.- e n
- ℤ↪R-diff m zero = R.intror R.inv-unit
- ℤ↪R-diff m (suc n) = refl
+ z-natdiff : ∀ x y → ℤ↪R (x ℕ- y) ≡ e x R.- e y
+ z-natdiff x zero = R.intror R.inv-unit
+ z-natdiff zero (suc y) = R.introl refl
+ z-natdiff (suc x) (suc y) = z-natdiff x y ∙ e-tr x y
+
+ z-add : ∀ x y → ℤ↪R (x +ℤ y) ≡ ℤ↪R x R.+ ℤ↪R y
+ z-add (pos x) (pos y) = e-add x y
+ z-add (pos x) (negsuc y) = z-natdiff x (suc y)
+ z-add (negsuc x) (pos y) = z-natdiff y (suc x) ∙ R.+-commutes
+ z-add (negsuc x) (negsuc y) =
+ R.- (e 1 R.+ e (suc x Nat.+ y)) ≡⟨ ap R.-_ (ap₂ R._+_ refl (e-add (suc x) y) ∙ R.extendl R.+-commutes) ⟩
+ R.- (e (suc x) R.+ (e 1 R.+ e y)) ≡⟨ R.a.inv-comm ⟩
+ (R.- (e 1 R.+ e y)) R.+ (R.- e (suc x)) ≡⟨ R.+-commutes ⟩
+ (R.- e (suc x)) R.+ (R.- (e 1 R.+ e y)) ≡⟨ ap₂ R._+_ refl (ap R.-_ (sym (e-add 1 y))) ⟩
+ (R.- e (suc x)) R.+ (R.- e (1 Nat.+ y)) ∎
+
+ z-mul : ∀ x y → ℤ↪R (x *ℤ y) ≡ ℤ↪R x R.* ℤ↪R y
+ z-mul (pos x) (pos y) =
+ ℤ↪R (assign pos (x Nat.* y)) ≡⟨ ap ℤ↪R (assign-pos (x Nat.* y)) ⟩
+ e (x Nat.* y) ≡⟨ e-mul x y ⟩
+ (e x R.* e y) ∎
+ z-mul (posz) (negsuc y) = sym R.*-zerol
+ z-mul (possuc x) (negsuc y) =
+ R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
+ R.- (e (suc x) R.* e (suc y)) ≡˘⟨ R.*-negater ⟩
+ e (suc x) R.* (R.- e (suc y)) ∎
+ z-mul (negsuc x) (posz) =
+ ℤ↪R (assign neg (x Nat.* 0)) ≡⟨ ap ℤ↪R (ap (assign neg) (Nat.*-zeror x)) ⟩
+ ℤ↪R 0 ≡⟨ sym R.*-zeror ⟩
+ ℤ↪R (negsuc x) R.* R.0r ∎
+ z-mul (negsuc x) (possuc y) =
+ R.- e (suc x Nat.* suc y) ≡⟨ ap R.-_ (e-mul (suc x) (suc y)) ⟩
+ R.- (e (suc x) R.* e (suc y)) ≡⟨ sym R.*-negatel ⟩
+ (R.- e (suc x)) R.* e (suc y) ∎
+ z-mul (negsuc x) (negsuc y) =
+ e (suc x Nat.* suc y) ≡⟨ e-mul (suc x) (suc y) ⟩
+ e (suc x) R.* e (suc y) ≡˘⟨ R.inv-inv ⟩
+ R.- (R.- (e (suc x) R.* e (suc y))) ≡˘⟨ ap R.-_ R.*-negater ⟩
+ R.- (e (suc x) R.* ℤ↪R (negsuc y)) ≡˘⟨ R.*-negatel ⟩
+ ℤ↪R (negsuc x) R.* ℤ↪R (negsuc y) ∎
z→r : Rings.Hom Liftℤ R
z→r .hom (lift x) = ℤ↪R x
-```
-
The last thing we must show is that this is the _unique_ ring
homomorphism from the integers to $R$. This, again, is slightly
@@ -232,44 +217,14 @@ and that last expression is pretty exactly what our canonical map
evaluates to on $n$. So we're done!
```agda
- lemma : ∀ (f : Rings.Hom Liftℤ R) i → z→r # lift i ≡ f # lift i
- lemma f =
- Int-elim-prop (λ _ → hlevel 1) λ a b → sym $
- f # lift (diff a b) ≡⟨ ap (f #_) (ap lift (p a b)) ⟩
- f # lift (diff a 0 +ℤ diff 0 b) ≡⟨ f .preserves .pres-+ (lift (diff a 0)) (lift (diff 0 b)) ⟩
- f # lift (diff a 0) R.+ f # lift (diff 0 b) ≡⟨ ap₂ R._+_ (q a) (is-group-hom.pres-inv gh {x = lift (diff b 0)} ∙ ap R.-_ (q b)) ⟩
- (e a) R.+ (R.- e b) ≡˘⟨ ℤ↪R-diff a b ⟩
- z→r # lift (diff a b) ∎
- where
- p : ∀ a b → diff a b ≡ diff a 0 +ℤ diff 0 b
- p a b = ap (λ e → diff e b) (sym (Nat.+-zeror a))
-
- gh : is-group-hom
- (Ring-on.additive-group (Liftℤ .snd) .snd)
- (Ring-on.additive-group (R .snd) .snd)
- _
- gh = record { pres-⋆ = f .preserves .pres-+ }
-
- q : ∀ a → f # lift (diff a 0) ≡ e a
- q zero = is-group-hom.pres-id gh
- q (suc n) =
- f # lift (diff (suc n) 0) ≡⟨ f .preserves .pres-+ (lift (diff 1 0)) (lift (diff n 0)) ⟩
- f # lift 1 R.+ f # lift (diff n 0) ≡⟨ ap₂ R._+_ (f .preserves .pres-id) (q n) ⟩
- R.1r R.+ (e n) ≡˘⟨ e-suc n ⟩
- e (suc n) ∎
-```
-
-## Abelian groups as Z-modules
+ module _ (f : Rings.Hom Liftℤ R) where
+ private module f = is-ring-hom (f .preserves)
-A fun consequence of $\ZZ$ being the initial ring is that every
-[[abelian group]] admits a unique $\ZZ$-module structure. This is, if
-you ask me, rather amazing! The correspondence is as follows: Because of
-the delooping-endomorphism ring adjunction, we have a correspondence
-between "$R$-module structures on G" and "ring homomorphisms $R \to
-\rm{Endo}(G)$" --- and since the latter is contractible, so is the
-former!
+ f-pos : ∀ x → e x ≡ f .hom (lift (pos x))
+ f-pos zero = sym f.pres-0
+ f-pos (suc x) = e-suc x ∙ sym (f.pres-+ (lift 1) (lift (pos x)) ∙ ap₂ R._+_ f.pres-id (sym (f-pos x)))
-```agda
-ℤ-module-unique : ∀ (G : Abelian-group ℓ) → is-contr (Ring-action Liftℤ (G .snd))
-ℤ-module-unique G = Equiv→is-hlevel 0 (Action≃Hom Liftℤ G) (Int-is-initial _)
+ lemma : (i : Int) → z→r # lift i ≡ f # lift i
+ lemma (pos x) = f-pos x
+ lemma (negsuc x) = sym (f.pres-neg {lift (possuc x)} ∙ ap R.-_ (sym (f-pos (suc x))))
```
diff --git a/src/Algebra/Ring/Commutative.lagda.md b/src/Algebra/Ring/Commutative.lagda.md
index e9efe38d8..033866bae 100644
--- a/src/Algebra/Ring/Commutative.lagda.md
+++ b/src/Algebra/Ring/Commutative.lagda.md
@@ -2,8 +2,15 @@
```agda
open import 1Lab.Function.Embedding
-open import Algebra.Prelude
open import Algebra.Ring
+
+open import Cat.Displayed.Univalence.Thin
+open import Cat.Prelude hiding (_*_ ; _+_)
+
+open import Data.Int.Properties
+open import Data.Int.Base
+
+import Algebra.Ring.Reasoning as Kit
```
-->
@@ -33,7 +40,7 @@ record CRing-on {ℓ} (R : Type ℓ) : Type ℓ where
CRing-structure : ∀ ℓ → Thin-structure ℓ CRing-on
CRing-structure ℓ = Full-substructure ℓ CRing-on Ring-on emb (Ring-structure ℓ) where
- open CRing-on hiding (_↪_)
+ open CRing-on
emb : ∀ X → CRing-on X ↪ Ring-on X
emb X .fst = has-ring-on
emb X .snd y (r , p) (s , q) =
@@ -56,9 +63,17 @@ CRing : ∀ ℓ → Type (lsuc ℓ)
CRing ℓ = CRings ℓ .Precategory.Ob
module CRing {ℓ} (R : CRing ℓ) where
- open CRing-on (R .snd) public
+ ring : Ring ℓ
+ ring .fst = R .fst
+ ring .snd = record { CRing-on (R .snd) }
+
+ open CRing-on (R .snd) using (*-commutes ; _+_ ; _*_ ; -_ ; _-_ ; 1r ; 0r) public
+ open Kit ring hiding (_+_ ; _*_ ; -_ ; _-_ ; 1r ; 0r) public
is-commutative-ring : ∀ {ℓ} (R : Ring ℓ) → Type _
is-commutative-ring R = ∀ {x y} → x R.* y ≡ y R.* x where
module R = Ring-on (R .snd)
+
+ℤ-comm : CRing lzero
+ℤ-comm = record { fst = el! Int ; snd = record { has-ring-on = ℤ .snd ; *-commutes = λ {x y} → *ℤ-commutative x y } }
```
diff --git a/src/Algebra/Ring/Ideal.lagda.md b/src/Algebra/Ring/Ideal.lagda.md
index d04510500..d5bc464b9 100644
--- a/src/Algebra/Ring/Ideal.lagda.md
+++ b/src/Algebra/Ring/Ideal.lagda.md
@@ -4,11 +4,16 @@ open import Algebra.Ring.Module.Action
open import Algebra.Group.Subgroup
open import Algebra.Ring.Module
open import Algebra.Group.Ab
-open import Algebra.Prelude
open import Algebra.Group
open import Algebra.Ring
+open import Cat.Displayed.Univalence.Thin
+open import Cat.Displayed.Total
+open import Cat.Prelude
+
open import Data.Power
+
+import Algebra.Ring.Reasoning as Ringr
```
-->
@@ -42,7 +47,7 @@ multiplication and addition.
```agda
module _ {ℓ} (R : Ring ℓ) where
- private module R = Ring-on (R .snd)
+ private module R = Ringr R
record is-ideal (𝔞 : ℙ ⌞ R ⌟) : Type (lsuc ℓ) where
no-eta-equality
@@ -131,15 +136,15 @@ injective.
Note that, since our ideals are all two-sided (for simplicity) but our
rings may not be commutative (for expressiveness), if we want the ideal
-generated by an element to be two-sided, then our ring must be
-commutative.
+generated by an element to be two-sided, this element must be *central*:
+it must commute with every element of the ring.
```agda
principal-ideal
- : (∀ x y → x R.* y ≡ y R.* x)
- → (a : ⌞ R ⌟)
+ : (a : ⌞ R ⌟)
+ → (central : ∀ x → a R.* x ≡ x R.* a)
→ is-ideal λ b → elΩ (Σ _ λ c → b ≡ c R.* a)
- principal-ideal comm a = record
+ principal-ideal a comm = record
{ has-rep-subgroup = record
{ has-unit = pure (_ , sym R.*-zerol)
; has-⋆ = λ x y → do
@@ -148,15 +153,14 @@ commutative.
pure (xi R.+ yi , ap₂ R._+_ p q ∙ sym R.*-distribr)
; has-inv = λ x → do
(xi , p) ← x
- pure (R.- xi , ap R.-_ p ∙ R.neg-*-l)
+ pure (R.- xi , ap R.-_ p ∙ sym R.*-negatel)
}
; has-*ₗ = λ x y → do
(yi , q) ← y
- pure (x R.* yi , ap (x R.*_) q ∙ R.*-associative)
+ pure (x R.* yi , R.m.pushr q)
; has-*ᵣ = λ x y → do
(yi , q) ← y
pure ( yi R.* x
- , ap (R._* x) q ·· sym R.*-associative ·· ap (yi R.*_) (comm a x)
- ∙ R.*-associative)
+ , ap (R._* x) q ∙ R.m.extendr (comm x))
}
```
diff --git a/src/Algebra/Ring/Localisation.lagda.md b/src/Algebra/Ring/Localisation.lagda.md
new file mode 100644
index 000000000..4814a97b4
--- /dev/null
+++ b/src/Algebra/Ring/Localisation.lagda.md
@@ -0,0 +1,431 @@
+
+
+```agda
+module Algebra.Ring.Localisation where
+```
+
+# Localisations of commutative rings {defines="localisation-of-a-ring"}
+
+The **localisation** $R\loc{S}$ of a commutative [[ring]] $R$ at a set
+of elements $S$ is the universal solution to forcing the elements of $S$
+to become invertible, analogously to how [[localisations of a
+category||localisation]] $\cC$ universally invert a class of maps in
+$\cC$. Explicitly, it is a commutative ring $R\loc{S}$, equipped with a
+homomorphism $-/1 : R \to R\loc{S}$ which sends elements $s \in S$ to
+*invertible* elements $s/1 : R\loc{S}$, and which is initial among
+these.
+
+The elements of $R\loc{S}$ are given by formal *fractions*, which we
+will write $r/s$, with $r, s : R$ and $s \in S$. Type-theoretically,
+such a fraction is really a *triple*, since we must also consider the
+witness $w : s \in S$ that the denominator belongs to $S$; but, since
+these proofs do not matter for identity of fractions, we will generally
+omit them in the prose.
+
+```agda
+record Fraction {ℓ ℓ'} {R : Type ℓ} (S : R → Type ℓ') : Type (ℓ ⊔ ℓ') where
+ no-eta-equality ; pattern
+ constructor _/_[_]
+ field
+ num : R
+ denom : R
+ has-denom : denom ∈ S
+```
+
+
+
+
+
+To ensure that we have a well-behaved theory of fractions, we will
+require that $S$ is a **multiplicatively closed** subset of $R$. In
+particular, the presence of $1 \in S$ allows us to form the fractions
+$r/1$ for any $r : R$, thus ensuring we have a map $R \to R\loc{S}$. We
+also require that, if $s \in S$ and $s' \in S$, then also $ss' \in S$.
+This will be important to define both multiplication *and identity* of
+fractions.
+
+```agda
+ record is-multiplicative {ℓ'} (S : ⌞ R ⌟ → Type ℓ') : Type (ℓ ⊔ ℓ') where
+ field
+ has-1 : 1r ∈ S
+ has-* : ∀ {x y} → x ∈ S → y ∈ S → (x * y) ∈ S
+```
+
+Under the assumption that $S$ is multiplicatively closed, we could
+attempt to mimic the usual operations on integer-valued fractions on our
+fractions, for example, defining the sum $x/s + y/t$ to be $(xt+ys)/st$.
+This turns out not to work too well: for example, if we then also define
+$-x/s = (-x)/s$, we would have $x/s + -x/s$ equal to
+
+$$
+\frac{xs + (-x)s}{s^2} = \frac{(x - x)s}{s^2} = \frac{0}{s^2}
+$$
+
+which is not *literally* the zero fraction $0/1$. However, we still have
+$0s^2 = 0*1$, so these fractions "represent the same quantity" --- they
+both stand for *zero times* the formal inverse of something. We could
+then try to identify fractions $x/s$ and $y/t$ whenever $xt = ys$, but,
+in a general ring $R$, this relation fails to be transitive, so it can
+not be equality in a set. Therefore, we allow an "adjustment" by one of
+our formal denominators: the equivalence relation we will impose on
+fractions identifies $x/s \approx y/t$ whenever there exists $u \in S$
+with $uxt = uys$.
+
+```agda
+ data _≈_ {ℓ'} {S : ⌞ R ⌟ → Type ℓ'} (x y : Fraction S) : Type (ℓ ⊔ ℓ') where
+ inc : (u : ⌞ R ⌟) (u∈S : u ∈ S) → u * ↑ x * ↓ y ≡ u * ↑ y * ↓ x → x ≈ y
+ squash : is-prop (x ≈ y)
+```
+
+
+
+In the literature, this is more commonly phrased as $u(xt - ys) = 0$,
+but the equivalence between that and our definition is routine.
+
+```agda
+ _≈'_ : ∀ {ℓ'} {S : ⌞ R ⌟ → Type ℓ'} → Fraction S → Fraction S → Type _
+ _≈'_ {S = S} (x / s) (y / t) = ∃[ u ∈ R ] (u ∈ S × u * (x * t - y * s) ≡ 0r)
+```
+
+
+The calculation can be found in this ``{.html} block.
+
+```agda
+ ≈→≈' : ∀ {ℓ'} {S : ⌞ R ⌟ → Type ℓ'} {x y : Fraction S} → x ≈ y → x ≈' y
+ ≈→≈' {x = x / s} {y = y / t} = elim! λ u u∈S p →
+ let
+ prf =
+ u * (x * t - y * s) ≡⟨ solve 5 (λ u x t y s → u :* (x :* t :- y :* s) ≔ u :* x :* t :- u :* y :* s) u x t y s refl ⟩
+ u * x * t - u * y * s ≡⟨ ap₂ _-_ refl (sym p) ⟩
+ u * x * t - u * x * t ≡⟨ solve 1 (λ x → x :- x ≔ 0) (u * x * t) refl ⟩
+ 0r ∎
+ in inc (u , u∈S , prf)
+
+ ≈'→≈ : ∀ {ℓ'} {S : ⌞ R ⌟ → Type ℓ'} {x y : Fraction S} → x ≈' y → x ≈ y
+ ≈'→≈ {x = x / s} {y = y / t} = elim! λ u u∈S p →
+ let
+ prf =
+ u * x * t - u * y * s ≡⟨ solve 5 (λ u x t y s → u :* x :* t :- u :* y :* s ≔ u :* (x :* t :- y :* s)) u x t y s refl ⟩
+ u * (x * t - y * s) ≡⟨ p ⟩
+ 0r ∎
+ in inc u u∈S (zero-diff prf)
+```
+
+
+
+
+
+Our next step is showing that this relation is actually an equivalence
+relation. The proof of transitivity is the most interesting step: we
+assume that $vxt = vys$ and $wyu = wzt$, with "adjustments" by $v, w \in
+S$ respectively, but we produce the equation $(wvt)xu = (wvt)zs$ --- we
+must consider the denominator of the middle fraction $y/t$ to relate the
+two endpoints $x/s$ and $z/u$.
+
+```agda
+ Fraction-congruence : Congruence (Fraction (_∈ S)) _
+ Fraction-congruence ._∼_ = _≈_
+ Fraction-congruence .has-is-prop (_ / _) (_ / _) = hlevel 1
+ Fraction-congruence .reflᶜ {x / s} = inc 1r has-1 refl
+ Fraction-congruence .symᶜ {x / s} {y / t} = rec! λ u u∈S p → inc u u∈S (sym p)
+ Fraction-congruence ._∙ᶜ_ {x / s} {y / t [ r ]} {z / u} = elim!
+ λ v v∈S p w w∈S q →
+ let
+ prf =
+ w * v * t * x * u ≡⟨ cring! R ⟩
+ w * u * (v * x * t) ≡⟨ ap (w * u *_) p ⟩
+ w * u * (v * y * s) ≡⟨ cring! R ⟩
+ (w * y * u) * (v * s) ≡⟨ ap₂ _*_ q refl ⟩
+ (w * z * t) * (v * s) ≡⟨ cring! R ⟩
+ w * v * t * z * s ∎
+ in
+ inc (w * v * t) (has-* (has-* w∈S v∈S) r) prf
+```
+
+
+
+We then define $R\loc{S}$ to be the set of fractions $r/s$, identified
+according to this relation. Since $1 \in S$, we can immediately cough up
+the function $x \mapsto x/1$, mapping $R \to R\loc{S}$.
+
+```agda
+ _/1 : ⌞ R ⌟ → Fr.quotient
+ x /1 = inc (x / 1r [ has-1 ])
+```
+
+To define the operations of a ring on $R\loc{S}$, we first define them
+at the level of fractions:
+
+::: mathpar
+
+$$
+\frac{x}{s} + \frac{y}{t} = \frac{xt + ys}{st}
+$$
+
+$$
+-\frac{x}{s} = \frac{-x}{s}
+$$
+
+$$
+\frac{x}{s}\frac{y}{t} = \frac{xy}{st}
+$$
+
+:::
+
+As mentioned above, these operations do not satisfy the laws of a ring
+*on the set of fractions*. We must therefore prove that they respect the
+quotient we've taken, and then prove that they satisfy the ring laws *on
+the quotient*.
+
+```agda
+ +f : Fraction (_∈ S) → Fraction (_∈ S) → Fraction (_∈ S)
+ +f (x / s [ p ]) (y / t [ q ]) = (x * t + y * s) / (s * t) [ has-* p q ]
+
+ -f : Fraction (_∈ S) → Fraction (_∈ S)
+ -f (x / s [ p ]) = (- x) / s [ p ]
+
+ *f : Fraction (_∈ S) → Fraction (_∈ S) → Fraction (_∈ S)
+ *f (x / s [ p ]) (y / t [ q ]) = (x * y) / (s * t) [ has-* p q ]
+```
+
+
+Showing that these operations descend to the quotient is
+entirely routine algebra; However, the calculations *do* get pretty
+long, so we'll leave them in this ``{.html} block.
+
+```agda
+ -ₗ_ : Fr.quotient → Fr.quotient
+ -ₗ_ = Quot-elim (λ _ → hlevel 2) (λ x → inc (-f x)) -f-resp where abstract
+ -f-resp : ∀ x y → x ≈ y → Path Fr.quotient (inc (-f x)) (inc (-f y))
+ -f-resp (x / s) (y / t) = elim! λ u u∈S p →
+ let
+ prf =
+ u * (- x) * t ≡⟨ ap (_* t) *-negater ∙ *-negatel ⟩
+ - (u * x * t) ≡⟨ ap -_ p ⟩
+ - (u * y * s) ≡⟨ sym *-negatel ∙ ap (_* s) (sym *-negater) ⟩
+ u * (- y) * s ∎
+ in quot (inc u u∈S prf)
+
+ _+ₗ_ : Fr.quotient → Fr.quotient → Fr.quotient
+ _+ₗ_ = Fr.op₂-comm +f (λ a b → Fr.reflᶜ' (+f-comm a b)) +f-resp where abstract
+ +f-comm : ∀ u v → +f u v ≡ +f v u
+ +f-comm (x / s) (y / t) = Fraction-path +-commutes *-commutes
+
+ +f-resp : ∀ x u v → u ≈ v → +f x u ≈ +f x v
+ +f-resp (x / s) (u / y) (v / z) = rec! λ w w∈S p →
+ let
+ prf =
+ w * (x * y + u * s) * (s * z) ≡⟨ cring! R ⟩
+ w * x * y * s * z + s * s * ⌜ w * u * z ⌝ ≡⟨ ap! p ⟩
+ w * x * y * s * z + s * s * ⌜ w * v * y ⌝ ≡⟨ cring! R ⟩
+ w * (x * z + v * s) * (s * y) ∎
+ in inc w w∈S prf
+
+ _*ₗ_ : Fr.quotient → Fr.quotient → Fr.quotient
+ _*ₗ_ = Fr.op₂-comm *f *f-comm *f-resp where abstract
+ *f-comm : ∀ u v → *f u v ≈ *f v u
+ *f-comm (x / s) (y / t) = inc 1r has-1 (solve 4 (λ x y t s → 1 :* (x :* y) :* (t :* s) ≔ 1 :* (y :* x) :* (s :* t)) x y t s refl)
+
+ *f-resp : ∀ x u v → u ≈ v → *f x u ≈ *f x v
+ *f-resp (x / s) (u / y) (v / z) = rec! λ w w∈S p →
+ let
+ prf =
+ w * (x * u) * (s * z) ≡⟨ cring! R ⟩
+ s * x * (w * u * z) ≡⟨ ap (s * x *_) p ⟩
+ s * x * (w * v * y) ≡⟨ cring! R ⟩
+ w * (x * v) * (s * y) ∎
+ in inc w w∈S prf
+```
+
+
+```agda
+ infixl 8 _+ₗ_
+ infixl 9 _*ₗ_
+ infix 10 -ₗ_ _/1
+
+ 0ₗ 1ₗ : Fr.quotient
+ 0ₗ = 0r /1
+ 1ₗ = 1r /1
+```
+
+We choose the zero and identity elements for $R\loc{S}$ so that the
+localising map $R \to R\loc{S}$ preserves them definitionally. We're
+almost done with the construction; while there's quite a bit of algebra
+left to do to show that we have a ring, this is almost entirely
+automatic. As a warm-up, we can prove that $x/1$ is inverted by $1/x$
+whenever $x \in S$.
+
+```agda
+ /1-inverts : ∀ x (p : x ∈ S) → inc (1r / x [ p ]) *ₗ (x /1) ≡ 1ₗ
+ /1-inverts x p = quot (inc 1r has-1
+ (solve 1 (λ x → 1 :* (1 :* x) :* 1 ≔ 1 :* 1 :* (x :* 1)) x refl))
+```
+
+The actual proof obligation is shown above: we have to establish that $1
+* (1 * x) * 1 = 1 * 1 * (x * 1)$, which can be shown by a naïve solver.
+The equations for each of the ring laws are similarly boring:
+
+```agda
+ abstract
+ +ₗ-idl : ∀ x → 0ₗ +ₗ x ≡ x
+ +ₗ-idl = elim! λ x s _ → /-ap
+ (solve 2 (λ s x → 0 :* s :+ x :* 1 ≔ x) s x refl)
+ *-idl
+
+ +ₗ-invr : ∀ x → x +ₗ (-ₗ x) ≡ 0ₗ
+ +ₗ-invr = elim! λ x s _ → quot (inc 1r has-1 (solve 2
+ (λ x s → 1 :* (x :* s :+ (:- x) :* s) :* 1 ≔ 1 :* 0 :* (s :* s)) x s refl))
+
+ +ₗ-assoc : ∀ x y z → x +ₗ (y +ₗ z) ≡ (x +ₗ y) +ₗ z
+ +ₗ-assoc = elim! λ x s _ y t _ z u _ → /-ap
+ (solve 6 (λ x y z s t u →
+ x :* (t :* u) :+ (y :* u :+ z :* t) :* s
+ ≔ (x :* t :+ y :* s) :* u :+ z :* (s :* t)) x y z s t u refl)
+ *-associative
+
+ +ₗ-comm : ∀ x y → x +ₗ y ≡ y +ₗ x
+ +ₗ-comm = elim! λ x s _ y t _ → /-ap +-commutes *-commutes
+
+ *ₗ-idl : ∀ x → 1ₗ *ₗ x ≡ x
+ *ₗ-idl = elim! λ x s s∈S → quot (inc s s∈S (solve 2
+ (λ x s → s :* (1 :* x) :* s ≔ s :* x :* (1 :* s)) x s refl))
+
+ *ₗ-comm : ∀ x y → x *ₗ y ≡ y *ₗ x
+ *ₗ-comm = elim! λ x s _ y t _ → /-ap *-commutes *-commutes
+
+ *ₗ-assoc : ∀ x y z → x *ₗ (y *ₗ z) ≡ (x *ₗ y) *ₗ z
+ *ₗ-assoc = elim! λ x s _ y t _ z u _ → /-ap *-associative *-associative
+
+ *ₗ-distribl : ∀ x y z → x *ₗ (y +ₗ z) ≡ (x *ₗ y) +ₗ (x *ₗ z)
+ *ₗ-distribl = elim! λ x s _ y t _ z u _ →
+ let
+ prf : 1r * (x * (y * u + z * t)) * (s * t * (s * u))
+ ≡ 1r * (x * y * (s * u) + x * z * (s * t)) * (s * (t * u))
+ prf = cring! R
+ in quot (inc 1r has-1 prf)
+```
+
+Finally, these fit together to make a commutative ring.
+
+```agda
+ private
+ module mr = make-ring
+ open make-ring
+
+ mk-loc : make-ring Fr.quotient
+ mk-loc .ring-is-set = hlevel 2
+ mk-loc .0R = 0ₗ
+ mk-loc ._+_ = _+ₗ_
+ mk-loc .-_ = -ₗ_
+ mk-loc .1R = 1ₗ
+ mk-loc ._*_ = _*ₗ_
+ mk-loc .+-idl = +ₗ-idl
+ mk-loc .+-invr = +ₗ-invr
+ mk-loc .+-assoc = +ₗ-assoc
+ mk-loc .+-comm = +ₗ-comm
+ mk-loc .*-idl = *ₗ-idl
+ mk-loc .*-idr x = *ₗ-comm x 1ₗ ∙ *ₗ-idl x
+ mk-loc .*-assoc = *ₗ-assoc
+ mk-loc .*-distribl = *ₗ-distribl
+ mk-loc .*-distribr x y z =
+ *ₗ-comm (y +ₗ z) x ∙ *ₗ-distribl x y z ∙ ap₂ _+ₗ_ (*ₗ-comm x y) (*ₗ-comm x z)
+
+ S⁻¹R : CRing ℓ
+ S⁻¹R .fst = el! Fr.quotient
+ S⁻¹R .snd .CRing-on.has-ring-on = to-ring-on mk-loc
+ S⁻¹R .snd .CRing-on.*-commutes {x} {y} = *ₗ-comm x y
+```
diff --git a/src/Algebra/Ring/Module/Action.lagda.md b/src/Algebra/Ring/Module/Action.lagda.md
index 952e7f871..e91cb6e04 100644
--- a/src/Algebra/Ring/Module/Action.lagda.md
+++ b/src/Algebra/Ring/Module/Action.lagda.md
@@ -1,5 +1,6 @@
@@ -19,7 +22,7 @@ module Algebra.Ring.Quotient {ℓ} (R : Ring ℓ) where
@@ -54,7 +57,7 @@ comprehensibility's sake).
private
quot-grp : Group _
quot-grp = R.additive-group /ᴳ I.ideal→normal
- module R/I = Group-on (quot-grp .snd)
+ module R/I = Group-on (quot-grp .snd) hiding (magma-hlevel)
```
-->
@@ -75,12 +78,12 @@ thing: Since $(x - y) \in I$, also $(xa - ya) \in I$, so $[xa] = [ya]$.
```agda
p1 : ∀ a {x y} (r : (x R.- y) ∈ I) → inc (x R.* a) ≡ inc (y R.* a)
p1 a {x} {y} x-y∈I = quot $ subst (_∈ I)
- (R.*-distribr ∙ ap (x R.* a R.+_) (sym R.neg-*-l))
+ (R.*-distribr ∙ ap (x R.* a R.+_) R.*-negatel)
(I.has-*ᵣ a x-y∈I)
p2 : ∀ a {x y} (r : (x R.- y) ∈ I) → inc (a R.* x) ≡ inc (a R.* y)
p2 a {x} {y} x-y∈I = quot $ subst (_∈ I)
- (R.*-distribl ∙ ap (a R.* x R.+_) (sym R.neg-*-r))
+ (R.*-distribl ∙ ap (a R.* x R.+_) R.*-negater)
(I.has-*ₗ a x-y∈I)
```
diff --git a/src/Algebra/Ring/Reasoning.lagda.md b/src/Algebra/Ring/Reasoning.lagda.md
new file mode 100644
index 000000000..34c90751c
--- /dev/null
+++ b/src/Algebra/Ring/Reasoning.lagda.md
@@ -0,0 +1,51 @@
+
+
+```agda
+module Algebra.Ring.Reasoning {ℓ} (R : Ring ℓ) where
+```
+
+# Reasoning combinators for rings
+
+
+
+```agda
+*-zerol : 0r * x ≡ 0r
+*-zerol {x} =
+ 0r * x ≡⟨ a.introl a.inversel ⟩
+ (- 0r * x) + 0r * x + 0r * x ≡⟨ a.pullr (sym *-distribr) ⟩
+ (- 0r * x) + (0r + 0r) * x ≡⟨ ap₂ _+_ refl (ap (_* x) a.idl) ⟩
+ (- 0r * x) + 0r * x ≡⟨ a.inversel ⟩
+ 0r ∎
+
+*-zeror : x * 0r ≡ 0r
+*-zeror {x} =
+ x * 0r ≡⟨ a.intror a.inverser ⟩
+ x * 0r + (x * 0r - x * 0r) ≡⟨ a.pulll (sym *-distribl) ⟩
+ x * (0r + 0r) - x * 0r ≡⟨ ap₂ _-_ (ap (x *_) a.idl) refl ⟩
+ x * 0r - x * 0r ≡⟨ a.inverser ⟩
+ 0r ∎
+
+*-negatel : (- x) * y ≡ - (x * y)
+*-negatel {x} {y} = monoid-inverse-unique a.has-is-monoid (x * y) ((- x) * y) (- (x * y))
+ (sym *-distribr ·· ap (_* y) a.inversel ·· *-zerol)
+ a.inverser
+
+*-negater : x * (- y) ≡ - (x * y)
+*-negater {x} {y} = monoid-inverse-unique a.has-is-monoid (x * y) (x * (- y)) (- (x * y))
+ (sym *-distribl ·· ap (x *_) a.inversel ·· *-zeror)
+ a.inverser
+```
diff --git a/src/Algebra/Ring/Solver.agda b/src/Algebra/Ring/Solver.agda
index bf1107915..8999382b8 100644
--- a/src/Algebra/Ring/Solver.agda
+++ b/src/Algebra/Ring/Solver.agda
@@ -16,25 +16,40 @@ open import 1Lab.Reflection
open import Algebra.Ring.Cat.Initial
open import Algebra.Ring.Commutative
open import Algebra.Group.Ab
-open import Algebra.Prelude
open import Algebra.Group
open import Algebra.Ring
+open import Cat.Displayed.Total
+open import Cat.Prelude hiding (_+_ ; _*_ ; _-_)
+
+open import Data.Fin.Product
open import Data.Fin.Base
-open import Data.Int.HIT
-open import Data.List hiding (lookup)
+open import Data.Int.Base
+open import Data.List hiding (lookup ; tabulate)
open import Data.Dec
open import Data.Nat
+import Algebra.Ring.Reasoning as Kit
+
+import Data.Int.Base as B
+
+open Total-hom
+
module Algebra.Ring.Solver where
module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
private
- module R = CRing-on cring
- ℤ↪R-rh = Int-is-initial (el _ R.has-is-set , R.has-ring-on) .centre
+ R' : Ring _
+ R' = record { fst = el _ (CRing-on.has-is-set cring) ; snd = CRing-on.has-ring-on cring }
+
+ module R = Kit R'
+
+ ℤ↪R-rh = Int-is-initial R' .centre
module ℤ↪R = is-ring-hom (ℤ↪R-rh .preserves)
embed-coe = ℤ↪R-rh .hom
+ open CRing-on cring using (*-commutes)
+
data Poly : Nat → Type ℓ
data Normal : Nat → Type ℓ
@@ -137,7 +152,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
-ₙ_ : ∀ {n} → Normal n → Normal n
-ₚ_ : ∀ {n} → Poly (suc n) → Poly (suc n)
- -ₙ con x = con (negate x)
+ -ₙ con x = con (negℤ x)
-ₙ poly x = poly (-ₚ x)
-ₚ x = (-ₙ 1n) *ₙₚ x
@@ -154,8 +169,8 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
-- Short-hand notation.
- infix 40 _:-_
- infix 30 _:*_
+ infixl 30 _:-_ _:+_
+ infixl 40 _:*_
_:+_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n
_:+_ = op [+]
@@ -180,6 +195,10 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
⟦⟧-Polynomial : ∀ {n} → ⟦⟧-notation (Polynomial n)
⟦⟧-Polynomial = brackets _ eval
+ Number-Polynomial : ∀ {n} → Number (Polynomial n)
+ Number-Polynomial .Number.Constraint x = Lift _ ⊤
+ Number-Polynomial .Number.fromNat n = con (pos n)
+
eval (op o p₁ p₂) ρ = sem o (⟦ p₁ ⟧ ρ) (⟦ p₂ ⟧ ρ)
eval (con c) ρ = embed-coe (lift c)
eval (var x) ρ = lookup ρ x
@@ -307,7 +326,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
where
lem₁' =
a R.* c R.* x ≡˘⟨ R.*-associative ⟩
- a R.* ⌜ c R.* x ⌝ ≡⟨ ap! R.*-commutes ⟩
+ a R.* ⌜ c R.* x ⌝ ≡⟨ ap! *-commutes ⟩
a R.* (x R.* c) ≡⟨ R.*-associative ⟩
a R.* x R.* c ∎
@@ -319,7 +338,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
lem₂ =
(a R.* d R.+ b R.* c) R.* x ≡⟨ R.*-distribr ⟩
a R.* d R.* x R.+ b R.* c R.* x ≡˘⟨ ap₂ R._+_ R.*-associative R.*-associative ⟩
- a R.* ⌜ d R.* x ⌝ R.+ b R.* (c R.* x) ≡⟨ ap! R.*-commutes ⟩
+ a R.* ⌜ d R.* x ⌝ R.+ b R.* (c R.* x) ≡⟨ ap! *-commutes ⟩
a R.* (x R.* d) R.+ b R.* (c R.* x) ≡⟨ ap₂ R._+_ R.*-associative refl ⟩
a R.* x R.* d R.+ b R.* (c R.* x) ∎
@@ -337,7 +356,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
*ₚₙ-hom c (p *x+ d) x ρ with c ==ₙ 0n
... | just c=0 = sym (ap₂ R._*_ refl (ap (λ e → En e ρ) c=0 ∙ 0n-hom ρ) ∙ R.*-zeror)
... | nothing =
- ap₂ R._+_ (ap (R._* x) (*ₚₙ-hom c p x ρ) ·· sym R.*-associative ·· ap₂ R._*_ refl R.*-commutes ∙ R.*-associative)
+ ap₂ R._+_ (ap (R._* x) (*ₚₙ-hom c p x ρ) ·· sym R.*-associative ·· ap₂ R._*_ refl *-commutes ∙ R.*-associative)
(*ₙ-hom d c ρ)
∙ sym R.*-distribr
@@ -347,7 +366,7 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
-ₚ-hom p (x ∷ ρ) =
*ₙₚ-hom (-ₙ 1n) p x ρ
∙ ap₂ R._*_ (-ₙ-hom 1n ρ ∙ ap R.-_ (1n-hom ρ)) refl
- ∙ sym R.neg-*-l ∙ ap R.-_ R.*-idl
+ ∙ R.*-negatel ∙ ap R.-_ R.*-idl
-ₙ-hom (con x) ρ = ℤ↪R.pres-neg {x = lift x}
-ₙ-hom (poly x) ρ = -ₚ-hom x ρ
@@ -388,6 +407,30 @@ module Impl {ℓ} {R : Type ℓ} (cring : CRing-on R) where
test-identities x =
solve (var 0 :+ (con 0 :* con 1)) ((con 1 :+ con 0) :* var 0) (x ∷ []) refl
+module Explicit {ℓ} (R : CRing ℓ) where
+ private module I = Impl (R .snd)
+
+ open I renaming (solve to solve-impl)
+ open I public using (Polynomial ; _:+_ ; _:-_ ; :-_ ; _:*_ ; con ; Number-Polynomial)
+
+ _≔_ : ∀ {n} → Polynomial n → Polynomial n → Polynomial n × Polynomial n
+ x ≔ y = x , y
+
+ private
+ variables : ∀ {n} → Πᶠ {n = n} λ i → Polynomial n
+ variables = tabulateₚ var
+
+ abstract
+ solve
+ : (n : Nat) (f : Arrᶠ {n = n} (λ i → Polynomial n) (Polynomial n × Polynomial n))
+ → (let (lhs , rhs) = applyᶠ {n = n} f variables)
+ → ∀ᶠ n (λ i → ⌞ R ⌟) λ vs
+ → (let rs = tabulate (indexₚ vs))
+ → En (normal lhs) rs ≡ En (normal rhs) rs
+ → ⟦ lhs ⟧ rs ≡ ⟦ rhs ⟧ rs
+ solve n f = curry-∀ᶠ {n = n} (λ a → solve-impl lhs rhs (tabulate (indexₚ a)))
+ where open Σ (applyᶠ {n = n} f variables) renaming (fst to lhs ; snd to rhs)
+
module Reflection where
private
pattern ring-args cring args = (_ hm∷ _ hm∷ cring v∷ args)
@@ -421,11 +464,11 @@ module Reflection where
build-expr : ∀ {ℓ} {A : Type ℓ} → Term → Variables A → Term → TC (Term × Variables A)
build-expr cring vs (“0” cring') = do
unify cring cring'
- z ← quoteTC (diff 0 0)
+ z ← quoteTC (Int.pos 0)
pure $ con (quote Impl.Polynomial.con) (z v∷ []) , vs
build-expr cring vs (“1” cring') = do
unify cring cring'
- o ← quoteTC (diff 1 0)
+ o ← quoteTC (Int.pos 1)
pure $ con (quote Impl.Polynomial.con) (o v∷ []) , vs
build-expr cring vs (“*” cring' t1 t2) = do
unify cring cring'
@@ -496,3 +539,14 @@ private module TestCRing {ℓ} (R : CRing ℓ) where
test-identities : ∀ x → x R.+ (R.0r R.* R.1r) ≡ (R.1r R.+ R.0r) R.* x
test-identities x = cring! R
+
+ test-negation : ∀ x y → x R.* (R.- y) ≡ R.- (x R.* y)
+ test-negation x y = cring! R
+
+private module TestExplicit where
+ open Explicit ℤ-comm
+
+ _ : ∀ x y u v → (x B.*ℤ y) B.*ℤ (u B.*ℤ v) ≡ (x B.*ℤ u) B.*ℤ (y B.*ℤ v)
+ _ = λ x y u v → solve 4
+ (λ x y u v → (x :* y) :* (u :* v) ≔ (x :* u) :* (y :* v))
+ x y u v refl
diff --git a/src/Cat/Abelian/Base.lagda.md b/src/Cat/Abelian/Base.lagda.md
index 8ba3339bf..a6f364d38 100644
--- a/src/Cat/Abelian/Base.lagda.md
+++ b/src/Cat/Abelian/Base.lagda.md
@@ -2,8 +2,7 @@
```agda
open import Algebra.Group.Ab.Tensor
open import Algebra.Group.Ab
-open import Algebra.Prelude
-open import Algebra.Monoid hiding (idl; idr)
+open import Algebra.Monoid
open import Algebra.Group
open import Cat.Diagram.Equaliser.Kernel
@@ -12,12 +11,17 @@ open import Cat.Diagram.Biproduct
open import Cat.Diagram.Coproduct
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
+open import Cat.Displayed.Total
+open import Cat.Instances.Slice
open import Cat.Diagram.Zero
+open import Cat.Prelude hiding (_+_ ; _*_ ; _-_)
import Algebra.Group.Cat.Base as Grp
import Algebra.Group.Ab.Hom as Ab
-import Cat.Reasoning
+import Cat.Reasoning as Cat
+
+open Total-hom
```
-->
@@ -114,17 +118,17 @@ $-ab = (-a)b = a(-b)$, etc.
Hom.inverse (0m ∘ f) + (0m ∘ f) ≡⟨ Hom.inversel ⟩
0m ∎
- neg-∘-l
+ ∘-negatel
: ∀ {A B C} {g : Hom B C} {h : Hom A B}
→ Hom.inverse (g ∘ h) ≡ Hom.inverse g ∘ h
- neg-∘-l {g = g} {h} = monoid-inverse-unique Hom.has-is-monoid (g ∘ h) _ _
+ ∘-negatel {g = g} {h} = monoid-inverse-unique Hom.has-is-monoid (g ∘ h) _ _
Hom.inversel
(∘-linear-l _ _ _ ∙ ap (_∘ h) Hom.inverser ∙ ∘-zero-l)
- neg-∘-r
+ ∘-negater
: ∀ {A B C} {g : Hom B C} {h : Hom A B}
→ Hom.inverse (g ∘ h) ≡ g ∘ Hom.inverse h
- neg-∘-r {g = g} {h} = monoid-inverse-unique Hom.has-is-monoid (g ∘ h) _ _
+ ∘-negater {g = g} {h} = monoid-inverse-unique Hom.has-is-monoid (g ∘ h) _ _
Hom.inversel
(∘-linear-r _ _ _ ∙ ap (g ∘_) Hom.inverser ∙ ∘-zero-r)
@@ -132,7 +136,7 @@ $-ab = (-a)b = a(-b)$, etc.
: ∀ {A B C} (f g : Hom B C) (h : Hom A B)
→ (f ∘ h) - (g ∘ h) ≡ (f - g) ∘ h
∘-minus-l f g h =
- f ∘ h - g ∘ h ≡⟨ ap (f ∘ h +_) neg-∘-l ⟩
+ f ∘ h - g ∘ h ≡⟨ ap (f ∘ h +_) ∘-negatel ⟩
f ∘ h + (Hom.inverse g ∘ h) ≡⟨ ∘-linear-l _ _ _ ⟩
(f - g) ∘ h ∎
@@ -140,7 +144,7 @@ $-ab = (-a)b = a(-b)$, etc.
: ∀ {A B C} (f : Hom B C) (g h : Hom A B)
→ (f ∘ g) - (f ∘ h) ≡ f ∘ (g - h)
∘-minus-r f g h =
- f ∘ g - f ∘ h ≡⟨ ap (f ∘ g +_) neg-∘-r ⟩
+ f ∘ g - f ∘ h ≡⟨ ap (f ∘ g +_) ∘-negater ⟩
f ∘ g + (f ∘ Hom.inverse h) ≡⟨ ∘-linear-r _ _ _ ⟩
f ∘ (g - h) ∎
```
@@ -333,7 +337,7 @@ each $\hom$-monoid becomes a $\hom$-*group*.
diff --git a/src/Cat/Abelian/Instances/Functor.lagda.md b/src/Cat/Abelian/Instances/Functor.lagda.md
index 30519aa53..9a3524738 100644
--- a/src/Cat/Abelian/Instances/Functor.lagda.md
+++ b/src/Cat/Abelian/Instances/Functor.lagda.md
@@ -97,9 +97,9 @@ natural.
grp .inv f .η x = B.Hom.inverse (f .η x)
grp .inv f .is-natural x y g =
- B.Hom.inverse (f .η y) B.∘ F.₁ g ≡˘⟨ B.neg-∘-l ⟩
+ B.Hom.inverse (f .η y) B.∘ F.₁ g ≡˘⟨ B.∘-negatel ⟩
B.Hom.inverse ⌜ f .η y B.∘ F.₁ g ⌝ ≡⟨ ap! (f .is-natural x y g) ⟩
- B.Hom.inverse (G.₁ g B.∘ f .η x) ≡⟨ B.neg-∘-r ⟩
+ B.Hom.inverse (G.₁ g B.∘ f .η x) ≡⟨ B.∘-negater ⟩
G.₁ g B.∘ B.Hom.inverse (f .η x) ∎
grp .assoc _ _ _ = ext λ _ → B.Hom.associative
diff --git a/src/Cat/CartesianClosed/Instances/PSh.agda b/src/Cat/CartesianClosed/Instances/PSh.agda
index ebf830d35..84fbf92d5 100644
--- a/src/Cat/CartesianClosed/Instances/PSh.agda
+++ b/src/Cat/CartesianClosed/Instances/PSh.agda
@@ -1,8 +1,12 @@
open import Cat.Instances.Functor.Limits
open import Cat.Instances.Sets.Complete
+open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Exponential
-open import Cat.Diagram.Everything
+open import Cat.Diagram.Coproduct
open import Cat.Instances.Functor
+open import Cat.Diagram.Pullback
+open import Cat.Diagram.Terminal
+open import Cat.Diagram.Product
open import Cat.Functor.Adjoint
open import Cat.Instances.Sets
open import Cat.Functor.Hom
diff --git a/src/Cat/Diagram/Coproduct/Indexed.lagda.md b/src/Cat/Diagram/Coproduct/Indexed.lagda.md
index 5e0b4cbee..369cd971d 100644
--- a/src/Cat/Diagram/Coproduct/Indexed.lagda.md
+++ b/src/Cat/Diagram/Coproduct/Indexed.lagda.md
@@ -92,7 +92,7 @@ Indexed-coproduct-≃ e {F} p = λ where
Lift-Indexed-coproduct
: ∀ {ℓ} ℓ' → {I : Type ℓ} → {F : I → C.Ob}
- → Indexed-coproduct {Idx = Lift ℓ' I} (F ⊙ Lift.lower)
+ → Indexed-coproduct {Idx = Lift ℓ' I} (F ⊙ lower)
→ Indexed-coproduct F
Lift-Indexed-coproduct _ = Indexed-coproduct-≃ (Lift-≃ e⁻¹)
diff --git a/src/Cat/Diagram/Everything.agda b/src/Cat/Diagram/Everything.agda
deleted file mode 100644
index d0cb929b9..000000000
--- a/src/Cat/Diagram/Everything.agda
+++ /dev/null
@@ -1,30 +0,0 @@
-module Cat.Diagram.Everything where
-open import Cat.Diagram.Coequaliser public
-open import Cat.Diagram.Coequaliser.RegularEpi public
-open import Cat.Diagram.Colimit.Base public
-open import Cat.Diagram.Congruence public
-open import Cat.Diagram.Coproduct.Indexed public
-open import Cat.Diagram.Coproduct public
-open import Cat.Diagram.Duals public
-open import Cat.Diagram.Equaliser.Kernel public
-open import Cat.Diagram.Equaliser public
-open import Cat.Diagram.Equaliser.RegularMono public
-open import Cat.Diagram.Idempotent public
-open import Cat.Diagram.Image public
-open import Cat.Diagram.Initial public
-open import Cat.Diagram.Limit.Base public
-open import Cat.Diagram.Limit.Equaliser public
-open import Cat.Diagram.Limit.Finite public
-open import Cat.Diagram.Limit.Product public
-open import Cat.Diagram.Limit.Pullback public
-open import Cat.Diagram.Monad public
-open import Cat.Diagram.Monad.Limits public
-open import Cat.Diagram.Product.Indexed public
-open import Cat.Diagram.Product public
-open import Cat.Diagram.Pullback public
-open import Cat.Diagram.Pullback.Properties public
-open import Cat.Diagram.Pushout public
-open import Cat.Diagram.Pushout.Properties public
-open import Cat.Diagram.Sieve public
-open import Cat.Diagram.Terminal public
-open import Cat.Diagram.Zero public
diff --git a/src/Cat/Diagram/Product/Indexed.lagda.md b/src/Cat/Diagram/Product/Indexed.lagda.md
index bad06d9ab..acd51be3a 100644
--- a/src/Cat/Diagram/Product/Indexed.lagda.md
+++ b/src/Cat/Diagram/Product/Indexed.lagda.md
@@ -103,7 +103,7 @@ Indexed-product-≃ e {F} p = λ where
Lift-Indexed-product
: ∀ {ℓ} ℓ' → {I : Type ℓ} → {F : I → C.Ob}
- → Indexed-product {Idx = Lift ℓ' I} (F ⊙ Lift.lower)
+ → Indexed-product {Idx = Lift ℓ' I} (F ⊙ lower)
→ Indexed-product F
Lift-Indexed-product _ = Indexed-product-≃ (Lift-≃ e⁻¹)
diff --git a/src/Cat/Displayed/Cartesian/Indexing.lagda.md b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
index a650cc837..d691ab1f7 100644
--- a/src/Cat/Displayed/Cartesian/Indexing.lagda.md
+++ b/src/Cat/Displayed/Cartesian/Indexing.lagda.md
@@ -1,6 +1,5 @@
@@ -260,12 +264,12 @@ into an identification.
F : Displayed-functor Mon[ Setsₓ ] Mon Id
F .F₀' o .identity = o .η (lift tt)
F .F₀' o ._⋆_ x y = o .μ (x , y)
- F .F₀' o .has-is-monoid .Mon.has-is-semigroup =
+ F .F₀' o .has-is-monoid .has-is-semigroup =
record { has-is-magma = record { has-is-set = hlevel 2 }
; associative = o .μ-assoc $ₚ _
}
- F .F₀' o .has-is-monoid .Mon.idl = o .μ-unitl $ₚ _
- F .F₀' o .has-is-monoid .Mon.idr = o .μ-unitr $ₚ _
+ F .F₀' o .has-is-monoid .idl = o .μ-unitl $ₚ _
+ F .F₀' o .has-is-monoid .idr = o .μ-unitr $ₚ _
F .F₁' wit .pres-id = wit .pres-η $ₚ _
F .F₁' wit .pres-⋆ x y = wit .pres-μ $ₚ _
F .F-id' = prop!
diff --git a/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md b/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md
index acd55af48..370ca9a92 100644
--- a/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md
+++ b/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md
@@ -2,7 +2,7 @@
```agda
open import Algebra.Monoid.Category
open import Algebra.Semigroup
-open import Algebra.Monoid renaming (idr to mon-idr; idl to mon-idl)
+open import Algebra.Monoid
open import Algebra.Magma
open import Cat.Monoidal.Instances.Cartesian
@@ -22,6 +22,8 @@ open import Cat.Functor.Hom
open import Cat.Prelude
import Cat.Reasoning
+
+open is-monoid renaming (idl to mon-idl ; idr to mon-idr)
```
-->
diff --git a/src/Data/Dec/Base.lagda.md b/src/Data/Dec/Base.lagda.md
index 79b0b0b8a..e4bf2476b 100644
--- a/src/Data/Dec/Base.lagda.md
+++ b/src/Data/Dec/Base.lagda.md
@@ -224,3 +224,11 @@ from-dec-is-equiv = is-iso→is-equiv (iso to-dec p q) where
q (yes x) = refl
q (no x) = refl
```
+
+
diff --git a/src/Data/Fin/Closure.lagda.md b/src/Data/Fin/Closure.lagda.md
index 126de3e2f..12b460aaf 100644
--- a/src/Data/Fin/Closure.lagda.md
+++ b/src/Data/Fin/Closure.lagda.md
@@ -4,8 +4,8 @@ open import 1Lab.Prelude
open import Data.Set.Coequaliser
open import Data.Fin.Properties
-open import Data.Nat.Prime
open import Data.Fin.Base
+open import Data.Nat.Base
open import Data.Dec
open import Data.Sum
diff --git a/src/Data/Fin/Product.lagda.md b/src/Data/Fin/Product.lagda.md
index e5cdb90e3..a0d1403c7 100644
--- a/src/Data/Fin/Product.lagda.md
+++ b/src/Data/Fin/Product.lagda.md
@@ -57,6 +57,17 @@ tabulateₚ {n = zero} f = tt
tabulateₚ {n = suc n} f = f fzero , tabulateₚ λ i → f (fsuc i)
```
+
+
Elements of $\Pi^f$ for sequences with a known length enjoy strong
extensionality properties, since they are iterated types with
$\eta$-expansion. As an example:
@@ -108,6 +119,25 @@ mapₚ {0} f xs = xs
mapₚ {suc n} f xs = f fzero (xs .fst) , mapₚ (λ i → f (fsuc i)) (xs .snd)
```
+
+
More generically, we can characterise the entries of an updated product
type.
@@ -145,6 +175,27 @@ Arrᶠ {0} P x = x
Arrᶠ {suc n} P x = P fzero → Arrᶠ (λ i → P (fsuc i)) x
```
+
+
In the generic case, a finitary curried function can be eliminated using
a finitary dependent product; Moreover, curried functions are
"extensional" with respect to this application.
diff --git a/src/Data/Int/Base.lagda.md b/src/Data/Int/Base.lagda.md
index 157aa2073..771c9af79 100644
--- a/src/Data/Int/Base.lagda.md
+++ b/src/Data/Int/Base.lagda.md
@@ -2,12 +2,13 @@
```
open import 1Lab.Path.IdentitySystem
open import 1Lab.HLevel.Closure
+open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type
open import Data.Dec.Base
-open import Data.Nat.Base
+open import Data.Nat.Base hiding (Positive)
```
-->
@@ -303,7 +304,8 @@ sign× pos neg = neg
sign× neg pos = neg
_*ℤ_ : Int → Int → Int
-i *ℤ j = assign (sign× (sign i) (sign j)) (abs i * abs j)
+i@(pos _) *ℤ j = assign (sign× pos (sign j)) (abs i * abs j)
+i@(negsuc _) *ℤ j = assign (sign× neg (sign j)) (abs i * abs j)
```
There are actually alternative definitions of addition and
@@ -346,3 +348,38 @@ minℤ (pos _) (negsuc y) = negsuc y
minℤ (negsuc x) (pos _) = negsuc x
minℤ (negsuc x) (negsuc y) = negsuc (max x y)
```
+
+
diff --git a/src/Data/Int/DivMod.lagda.md b/src/Data/Int/DivMod.lagda.md
index a6fa2f9ff..ab758f8ad 100644
--- a/src/Data/Int/DivMod.lagda.md
+++ b/src/Data/Int/DivMod.lagda.md
@@ -10,7 +10,7 @@ open import Data.Int.Divisible
open import Data.Nat.DivMod
open import Data.Dec.Base
open import Data.Fin hiding (_<_)
-open import Data.Int
+open import Data.Int hiding (Positive)
open import Data.Nat as Nat
```
-->
@@ -85,7 +85,7 @@ $b - (-a)\%b$ as the remainder.
lemma =
assign neg (q * b + suc r) ≡⟨ ap (assign neg) (+-commutative (q * b) _) ⟩
negsuc (r + q * b) ≡˘⟨ negℤ-+ℤ-negsuc r (q * b) ⟩
- negℤ (pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (ℤ.insertl {h = negℤ (pos b')} (+ℤ-invl (pos b')) {f = negℤ (pos r)}) ⟩
+ negℤ (pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (ℤ.insertl {negℤ (pos b')} (+ℤ-invl (pos b')) {negℤ (pos r)}) ⟩
⌜ negℤ (pos b') ⌝ +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b) ≡˘⟨ ap¡ (assign-neg b') ⟩
assign neg b' +ℤ (pos b' -ℤ pos r) +ℤ negsuc (q * b) ≡⟨ ap (_+ℤ negsuc (q * b)) (+ℤ-commutative (assign neg b') (pos b' -ℤ pos r)) ⟩
(pos b' -ℤ pos r) +ℤ assign neg b' +ℤ negsuc (q * b) ≡˘⟨ +ℤ-assoc (pos b' -ℤ pos r) _ _ ⟩
@@ -186,7 +186,7 @@ divides-diff→same-rem n x y n∣x-y
p' : y ≡ (q -ℤ k) *ℤ pos n +ℤ pos r
p' =
y ≡˘⟨ negℤ-negℤ y ⟩
- negℤ (negℤ y) ≡⟨ ℤ.insertr (ℤ.inversel {x}) {f = negℤ (negℤ y)} ⟩
+ negℤ (negℤ y) ≡⟨ ℤ.insertr (ℤ.inversel {x}) {negℤ (negℤ y)} ⟩
⌜ negℤ (negℤ y) +ℤ negℤ x ⌝ +ℤ x ≡⟨ ap! (+ℤ-commutative (negℤ (negℤ y)) _) ⟩
⌜ negℤ x -ℤ negℤ y ⌝ +ℤ x ≡˘⟨ ap¡ (negℤ-distrib x (negℤ y)) ⟩
negℤ ⌜ x -ℤ y ⌝ +ℤ x ≡˘⟨ ap¡ z ⟩
diff --git a/src/Data/Int/Order.lagda.md b/src/Data/Int/Order.lagda.md
index c6cd5b2c9..2a101b4d2 100644
--- a/src/Data/Int/Order.lagda.md
+++ b/src/Data/Int/Order.lagda.md
@@ -57,6 +57,12 @@ for the ordering on natural numbers.
≤-refl {x = pos x} = pos≤pos Nat.≤-refl
≤-refl {x = negsuc x} = neg≤neg Nat.≤-refl
+≤-refl' : ∀ {x y} → x ≡ y → x ≤ y
+≤-refl' {pos x} {pos y} p = pos≤pos (Nat.≤-refl' (pos-injective p))
+≤-refl' {pos x} {negsuc y} p = absurd (pos≠negsuc p)
+≤-refl' {negsuc x} {pos y} p = absurd (negsuc≠pos p)
+≤-refl' {negsuc x} {negsuc y} p = neg≤neg (Nat.≤-refl' (negsuc-injective (sym p)))
+
≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
≤-trans (neg≤neg p) (neg≤neg q) = neg≤neg (Nat.≤-trans q p)
≤-trans (neg≤neg p) neg≤pos = neg≤pos
@@ -66,6 +72,18 @@ for the ordering on natural numbers.
≤-antisym : ∀ {x y} → x ≤ y → y ≤ x → x ≡ y
≤-antisym (neg≤neg p) (neg≤neg q) = ap negsuc (Nat.≤-antisym q p)
≤-antisym (pos≤pos p) (pos≤pos q) = ap pos (Nat.≤-antisym p q)
+
+unpos≤pos : ∀ {x y} → pos x ≤ pos y → x Nat.≤ y
+unpos≤pos (pos≤pos p) = p
+
+unneg≤neg : ∀ {x y} → negsuc x ≤ negsuc y → y Nat.≤ x
+unneg≤neg (neg≤neg p) = p
+
+apos≤apos : ∀ {x y} → x Nat.≤ y → assign pos x ≤ assign pos y
+apos≤apos {x} {y} p = ≤-trans (≤-refl' (assign-pos x)) (≤-trans (pos≤pos p) (≤-refl' (sym (assign-pos y))))
+
+unapos≤apos : ∀ {x y} → assign pos x ≤ assign pos y → x Nat.≤ y
+unapos≤apos {x} {y} p = unpos≤pos (≤-trans (≤-refl' (sym (assign-pos x))) (≤-trans p (≤-refl' (assign-pos y))))
```
## Totality
@@ -187,15 +205,15 @@ rotℤ≤l (negsuc zero) x y p = pred-≤ _ _ p
rotℤ≤l (negsuc (suc k)) x y p = pred-≤ _ _ (rotℤ≤l (negsuc k) x y p)
abstract
- +ℤ-mono-l : ∀ k x y → x ≤ y → (k +ℤ x) ≤ (k +ℤ y)
- +ℤ-mono-l k x y p = transport
+ +ℤ-preserves-≤l : ∀ k x y → x ≤ y → (k +ℤ x) ≤ (k +ℤ y)
+ +ℤ-preserves-≤l k x y p = transport
(sym (ap₂ _≤_ (rot-is-add k x) (rot-is-add k y)))
(rotℤ≤l k x y p)
- +ℤ-mono-r : ∀ k x y → x ≤ y → (x +ℤ k) ≤ (y +ℤ k)
- +ℤ-mono-r k x y p = transport
+ +ℤ-preserves-≤r : ∀ k x y → x ≤ y → (x +ℤ k) ≤ (y +ℤ k)
+ +ℤ-preserves-≤r k x y p = transport
(ap₂ _≤_ (+ℤ-commutative k x) (+ℤ-commutative k y))
- (+ℤ-mono-l k x y p)
+ (+ℤ-preserves-≤l k x y p)
negℤ-anti : ∀ x y → x ≤ y → negℤ y ≤ negℤ x
negℤ-anti posz posz x≤y = x≤y
@@ -211,4 +229,20 @@ abstract
negℤ-anti-full (possuc x) (possuc y) (neg≤neg x≤y) = pos≤pos (Nat.s≤s x≤y)
negℤ-anti-full (negsuc x) (pos y) _ = neg≤pos
negℤ-anti-full (negsuc x) (negsuc y) (pos≤pos (Nat.s≤s y≤x)) = neg≤neg y≤x
+
+ *ℤ-cancel-≤r : ∀ {x y z} ⦃ _ : Positive x ⦄ → (y *ℤ x) ≤ (z *ℤ x) → y ≤ z
+ *ℤ-cancel-≤r {possuc x} {y = pos y} {pos z} ⦃ pos _ ⦄ p = pos≤pos
+ (Nat.*-cancel-≤r (suc x) (unapos≤apos p))
+ *ℤ-cancel-≤r {possuc x} {y = pos y} {negsuc z} ⦃ pos _ ⦄ p = absurd (¬pos≤neg (≤-trans (≤-refl' (sym (assign-pos (y * suc x)))) p))
+ *ℤ-cancel-≤r {possuc x} {y = negsuc y} {pos z} ⦃ pos _ ⦄ p = neg≤pos
+ *ℤ-cancel-≤r {possuc x} {y = negsuc y} {negsuc z} ⦃ pos _ ⦄ p = neg≤neg
+ (Nat.*-cancel-≤r (suc x) (Nat.+-reflects-≤l (z * suc x) (y * suc x) x (unneg≤neg p)))
+
+ *ℤ-preserves-≤r : ∀ {x y} z ⦃ _ : Positive z ⦄ → x ≤ y → (x *ℤ z) ≤ (y *ℤ z)
+ *ℤ-preserves-≤r {pos x} {pos y} (possuc z) ⦃ pos z ⦄ p = apos≤apos {x * suc z} {y * suc z} (Nat.*-preserves-≤r x y (suc z) (unpos≤pos p))
+ *ℤ-preserves-≤r {negsuc x} {pos y} (possuc z) ⦃ pos z ⦄ p = ≤-trans neg≤pos (≤-refl' (sym (assign-pos (y * suc z))))
+ *ℤ-preserves-≤r {negsuc x} {negsuc y} (possuc z) ⦃ pos z ⦄ p = neg≤neg (Nat.+-preserves-≤l (y * suc z) (x * suc z) z (Nat.*-preserves-≤r y x (suc z) (unneg≤neg p)))
+
+ *ℤ-nonnegative : ∀ {x y} → 0 ≤ x → 0 ≤ y → 0 ≤ (x *ℤ y)
+ *ℤ-nonnegative {pos x} {pos y} (pos≤pos p) (pos≤pos q) = ≤-trans (pos≤pos Nat.0≤x) (≤-refl' (sym (assign-pos (x * y))))
```
diff --git a/src/Data/Int/Properties.lagda.md b/src/Data/Int/Properties.lagda.md
index ced6cc3c2..08985f55e 100644
--- a/src/Data/Int/Properties.lagda.md
+++ b/src/Data/Int/Properties.lagda.md
@@ -6,7 +6,8 @@ open import Data.Nat.Properties
open import Data.Nat.Solver
open import Data.Nat.Order
open import Data.Int.Base
-open import Data.Nat.Base
+open import Data.Nat.Base hiding (Positive)
+open import Data.Sum.Base
```
-->
@@ -358,19 +359,14 @@ no further comments.
lemma : ∀ x y z → z + y * suc z + x * suc (z + y * suc z) ≡ z + (y + x * suc y) * suc z
lemma x y z = nat!
+ -- *ℤ-def : ∀ x y → x *ℤ y ≡ assign (sign× (sign x) (sign y)) (abs x * abs y)
+
*ℤ-associative : ∀ x y z → x *ℤ (y *ℤ z) ≡ (x *ℤ y) *ℤ z
*ℤ-associative posz y z = refl
- *ℤ-associative x posz z =
- ap (λ e → assign (sign× (sign x) pos) e) (*-zeror (abs x)) ∙ sym (ap
- (λ e → assign
- (sign× (sign (assign (sign× (sign x) pos) e)) (sign z))
- (abs (assign (sign× (sign x) pos) e) * abs z)) (*-zeror (abs x)))
- *ℤ-associative x y posz =
- ap (λ e →
- assign (sign× (sign x) (sign (assign (sign× (sign y) pos) e)))
- (abs x * abs (assign (sign× (sign y) pos) e))) (*-zeror (abs y))
- ∙ ap₂ assign refl (*-zeror (abs x))
- ∙ sym (ap₂ assign refl (*-zeror (abs (assign (sign× (sign x) (sign y)) (abs x * abs y)))))
+ *ℤ-associative (pos x@(suc _)) posz z = ap (assign pos) (*-zeror x) ∙ sym (ap₂ _*ℤ_ (ap (assign pos) (*-zeror x)) refl)
+ *ℤ-associative (negsuc x) posz z = ap (assign neg) (*-zeror x) ∙ sym (ap₂ _*ℤ_ (ap (assign neg) (*-zeror x)) refl)
+ *ℤ-associative x (pos y) posz = ap₂ _*ℤ_ (λ i → x) (ap (assign pos) (*-zeror y)) ∙ *ℤ-zeror x ∙ sym (*ℤ-zeror (x *ℤ pos y))
+ *ℤ-associative x (negsuc y) posz = ap₂ _*ℤ_ (λ i → x) (ap (assign neg) (*-zeror y)) ∙ *ℤ-zeror x ∙ sym (*ℤ-zeror (x *ℤ negsuc y))
*ℤ-associative (possuc x) (possuc y) (possuc z) = ap possuc (lemma x y z)
*ℤ-associative (possuc x) (possuc y) (negsuc z) = ap negsuc (lemma x y z)
*ℤ-associative (possuc x) (negsuc y) (possuc z) = ap negsuc (lemma x y z)
@@ -404,7 +400,10 @@ no further comments.
sign×-commutative neg neg = refl
*ℤ-commutative : ∀ x y → x *ℤ y ≡ y *ℤ x
- *ℤ-commutative x y = ap₂ assign (sign×-commutative _ _) (*-commutative (abs x) (abs y))
+ *ℤ-commutative (pos x) (pos y) = ap (assign pos) (*-commutative x y)
+ *ℤ-commutative (pos x) (negsuc y) = ap (assign neg) (*-commutative x (suc y))
+ *ℤ-commutative (negsuc x) (pos y) = ap (assign neg) (*-commutative (suc x) y)
+ *ℤ-commutative (negsuc x) (negsuc y) = ap (assign pos) (*-commutative (suc x) (suc y))
dot-is-mul : ∀ x y → (dotℤ x y) ≡ (x *ℤ y)
dot-is-mul posz y = refl
@@ -468,4 +467,68 @@ no further comments.
*ℤ-injectiver posz x y k≠0 p = absurd (k≠0 refl)
*ℤ-injectiver (possuc k) x y k≠0 p = *ℤ-injectiver-possuc k x y p
*ℤ-injectiver (negsuc k) x y k≠0 p = *ℤ-injectiver-negsuc k x y p
+
+ *ℤ-is-zero : ∀ x y → (x *ℤ y) ≡ 0 → (x ≡ 0) ⊎ (y ≡ 0)
+ *ℤ-is-zero posz (pos _) _ = inl refl
+ *ℤ-is-zero (negsuc _) posz _ = inr refl
+ *ℤ-is-zero posz (negsuc _) _ = inl refl
+ *ℤ-is-zero (possuc _) posz _ = inr refl
+ *ℤ-is-zero (possuc _) (possuc _) p = absurd (suc≠zero (pos-injective p))
+ *ℤ-is-zero (possuc _) (negsuc _) p = absurd (negsuc≠pos p)
+ *ℤ-is-zero (negsuc _) (possuc _) p = absurd (negsuc≠pos p)
+ *ℤ-is-zero (negsuc _) (negsuc _) p = absurd (suc≠zero (pos-injective p))
+
+ abs-assign : ∀ s n → abs (assign s n) ≡ n
+ abs-assign pos zero = refl
+ abs-assign pos (suc n) = refl
+ abs-assign neg zero = refl
+ abs-assign neg (suc n) = refl
+
+ abs-*ℤ : ∀ x y → abs (x *ℤ y) ≡ abs x * abs y
+ abs-*ℤ (pos x) (pos y) = abs-assign pos (x * y)
+ abs-*ℤ (pos x) (negsuc y) = abs-assign neg (x * suc y)
+ abs-*ℤ (negsuc x) (pos y) = abs-assign neg (y + x * y)
+ abs-*ℤ (negsuc x) (negsuc y) = refl
+
+ sign-*ℤ-positive : ∀ x t → Positive t → sign (x *ℤ t) ≡ sign x
+ sign-*ℤ-positive (pos x) (possuc y) (pos _) = ap sign (assign-pos (x * suc y))
+ sign-*ℤ-positive (negsuc x) (possuc y) (pos _) = refl
+
+ assign-sign : ∀ x → assign (sign x) (abs x) ≡ x
+ assign-sign posz = refl
+ assign-sign (possuc _) = refl
+ assign-sign (negsuc _) = refl
+
+ assign-pos-positive : ∀ x → Positive x → assign pos (abs x) ≡ x
+ assign-pos-positive x@(possuc _) (pos _) = refl
+
+ divides-*ℤ : ∀ {n k m} → k * n ≡ abs m → pos k *ℤ assign (sign m) n ≡ m
+ divides-*ℤ {zero} {k} {pos x} p = ap (assign pos) (*-zeror k) ∙ ap Int.pos (sym (*-zeror k) ∙ p)
+ divides-*ℤ {suc n} {k} {posz} p = ap (assign pos) p
+ divides-*ℤ {suc n} {zero} {possuc x} p = ap pos p
+ divides-*ℤ {suc n} {suc k} {possuc x} p = ap pos p
+ divides-*ℤ {zero} {k} {negsuc x} p = absurd (zero≠suc (sym (*-zeror k) ∙ p))
+ divides-*ℤ {suc n} {zero} {negsuc x} p = absurd (zero≠suc p)
+ divides-*ℤ {suc n} {suc k} {negsuc x} p = ap negsuc (suc-inj p)
+```
+
+## Positivity
+
+```agda
+*ℤ-positive : ∀ {x y} → Positive x → Positive y → Positive (x *ℤ y)
+*ℤ-positive (pos x) (pos y) = pos (y + x * suc y)
+
++ℤ-positive : ∀ {x y} → Positive x → Positive y → Positive (x +ℤ y)
++ℤ-positive (pos x) (pos y) = pos (x + suc y)
+
+pos-positive : ∀ {x} → x ≠ 0 → Positive (pos x)
+pos-positive {zero} 0≠0 = absurd (0≠0 refl)
+pos-positive {suc n} _ = pos n
+
+positive→nonzero : ∀ {x} → Positive x → x ≠ 0
+positive→nonzero .{possuc x} (pos x) p = suc≠zero (pos-injective p)
+
+*ℤ-positive-cancel : ∀ {x y} → Positive x → Positive (x *ℤ y) → Positive y
+*ℤ-positive-cancel {pos .(suc x)} {posz} (pos x) q = absurd (positive→nonzero q (ap (assign pos) (*-zeror x)))
+*ℤ-positive-cancel {pos .(suc x)} {possuc y} (pos x) q = pos y
```
diff --git a/src/Data/List/Properties.lagda.md b/src/Data/List/Properties.lagda.md
index 7354da83c..1e876b92c 100644
--- a/src/Data/List/Properties.lagda.md
+++ b/src/Data/List/Properties.lagda.md
@@ -92,8 +92,8 @@ We use this to prove that lists preserve h-levels for $n \ge 2$, i.e. if
List-is-hlevel n ahl x y = Equiv→is-hlevel (suc n) Code≃Path Code-is-hlevel where
Code-is-hlevel : {x y : List A} → is-hlevel (Code x y) (suc n)
Code-is-hlevel {[]} {[]} = is-prop→is-hlevel-suc λ x y → refl
- Code-is-hlevel {[]} {x ∷ y} = is-prop→is-hlevel-suc λ x → absurd (Lift.lower x)
- Code-is-hlevel {x ∷ x₁} {[]} = is-prop→is-hlevel-suc λ x → absurd (Lift.lower x)
+ Code-is-hlevel {[]} {x ∷ y} = is-prop→is-hlevel-suc λ x → absurd (lower x)
+ Code-is-hlevel {x ∷ x₁} {[]} = is-prop→is-hlevel-suc λ x → absurd (lower x)
Code-is-hlevel {x ∷ x₁} {x₂ ∷ y} = ×-is-hlevel (suc n) (ahl _ _) Code-is-hlevel
instance
diff --git a/src/Data/Nat/Base.lagda.md b/src/Data/Nat/Base.lagda.md
index ae1de2e0f..55df78a59 100644
--- a/src/Data/Nat/Base.lagda.md
+++ b/src/Data/Nat/Base.lagda.md
@@ -219,6 +219,10 @@ instance
{-# INCOHERENT x≤x x≤sucy #-}
+factorial : Nat → Nat
+factorial zero = 1
+factorial (suc n) = suc n * factorial n
+
Positive : Nat → Type
Positive n = 1 ≤ n
```
diff --git a/src/Data/Nat/Divisible.lagda.md b/src/Data/Nat/Divisible.lagda.md
index 266ae70b5..203d9f929 100644
--- a/src/Data/Nat/Divisible.lagda.md
+++ b/src/Data/Nat/Divisible.lagda.md
@@ -150,6 +150,9 @@ expect a number to divide its multiples. Fortunately, this is the case:
|-*l-pres : ∀ {n a b} → n ∣ b → n ∣ a * b
|-*l-pres {n} {a} {b} p1 with (q , α) ← ∣→fibre p1 = fibre→∣ (a * q , *-associative a q n ∙ ap (a *_) α)
+
+∣-*-cancelr : ∀ {n a b} .⦃ _ : Positive n ⦄ → a * n ∣ b * n → a ∣ b
+∣-*-cancelr {n} {a} {b} p1 with (q , α) ← ∣→fibre p1 = fibre→∣ (q , *-injr n (q * a) b (*-associative q a n ∙ α))
```
If two numbers are multiples of $k$, then so is their sum.
diff --git a/src/Data/Nat/Divisible/GCD.lagda.md b/src/Data/Nat/Divisible/GCD.lagda.md
index 5eb910793..8d3ca1bbc 100644
--- a/src/Data/Nat/Divisible/GCD.lagda.md
+++ b/src/Data/Nat/Divisible/GCD.lagda.md
@@ -193,6 +193,24 @@ is-gcd-graphs-gcd {m = m} {n} {d} = prop-ext!
(λ p → subst (is-gcd m n) p (Euclid.euclid m n .snd))
```
+
+
## Euclid's lemma
```agda
diff --git a/src/Data/Nat/Prime.lagda.md b/src/Data/Nat/Prime.lagda.md
index 68f1d668a..4c6ff0f25 100644
--- a/src/Data/Nat/Prime.lagda.md
+++ b/src/Data/Nat/Prime.lagda.md
@@ -256,18 +256,6 @@ factorisation-worker n@(suc (suc m)) ind with is-prime-or-composite n (s≤s (s
; is-primes = composite .p-prime ∷ primes
}
-factorial : Nat → Nat
-factorial zero = 1
-factorial (suc n) = suc n * factorial n
-
-factorial-positive : ∀ n → Positive (factorial n)
-factorial-positive zero = s≤s 0≤x
-factorial-positive (suc n) = *-preserves-≤ 1 (suc n) 1 (factorial n) (s≤s 0≤x) (factorial-positive n)
-
-≤-factorial : ∀ n → n ≤ factorial n
-≤-factorial zero = 0≤x
-≤-factorial (suc n) = subst (_≤ factorial (suc n)) (*-oner (suc n)) (*-preserves-≤ (suc n) (suc n) 1 (factorial n) ≤-refl (factorial-positive n))
-
∣-factorial : ∀ n {m} → m < n → suc m ∣ factorial n
∣-factorial (suc n) {m} m≤n with suc m ≡? suc n
... | yes m=n = subst (_∣ factorial (suc n)) (sym m=n) (∣-*l {suc n} {factorial n})
diff --git a/src/Data/Nat/Properties.lagda.md b/src/Data/Nat/Properties.lagda.md
index a4b941330..2cb328a9d 100644
--- a/src/Data/Nat/Properties.lagda.md
+++ b/src/Data/Nat/Properties.lagda.md
@@ -6,6 +6,7 @@ open import 1Lab.Type
open import Data.Nat.Order
open import Data.Dec.Base
open import Data.Nat.Base
+open import Data.Sum.Base
open import Data.Bool
```
-->
@@ -134,6 +135,21 @@ numbers]. Since they're mostly simple inductive arguments written in
*-is-oner : ∀ x n → x * n ≡ 1 → n ≡ 1
*-is-oner x n p = *-is-onel n x (*-commutative n x ∙ p)
+
+*-is-zero : ∀ x y → x * y ≡ 0 → (x ≡ 0) ⊎ (y ≡ 0)
+*-is-zero zero y p = inl refl
+*-is-zero (suc x) zero p = inr refl
+*-is-zero (suc x) (suc y) p = absurd (suc≠zero p)
+
+*-is-zerol : ∀ x y ⦃ _ : Positive y ⦄ → x * y ≡ 0 → x ≡ 0
+*-is-zerol x (suc y) p with *-is-zero x (suc y) p
+... | inl p = p
+... | inr q = absurd (suc≠zero q)
+
+*-is-zeror : ∀ x y ⦃ _ : Positive x ⦄ → x * y ≡ 0 → y ≡ 0
+*-is-zeror (suc x) y p with *-is-zero (suc x) y p
+... | inl p = absurd (suc≠zero p)
+... | inr q = q
```
## Exponentiation
@@ -252,9 +268,14 @@ difference→≤ {suc x} {suc z} (suc y) p = s≤s (difference→≤ (suc y) (su
nonzero→positive : ∀ {x} → x ≠ 0 → 0 < x
nonzero→positive {zero} p = absurd (p refl)
nonzero→positive {suc x} p = s≤s 0≤x
+
+*-cancel-≤r : ∀ x {y z} .⦃ _ : Positive x ⦄ → (y * x) ≤ (z * x) → y ≤ z
+*-cancel-≤r (suc x) {zero} {z} p = 0≤x
+*-cancel-≤r (suc x) {suc y} {suc z} (s≤s p) = s≤s
+ (*-cancel-≤r (suc x) {y} {z} (+-reflects-≤l (y * suc x) (z * suc x) x p))
```
-### Monus
+## Monus
```agda
monus-zero : ∀ a → 0 - a ≡ 0
@@ -294,7 +315,7 @@ monus-swapr : ∀ x y z → x + y ≡ z → x ≡ z - y
monus-swapr x y z p = sym (monus-cancelr x 0 y) ∙ ap (_- y) p
```
-### Maximum
+## Maximum
```agda
max-assoc : (x y z : Nat) → max x (max y z) ≡ max (max x y) z
@@ -334,7 +355,7 @@ max-zeror zero = refl
max-zeror (suc x) = refl
```
-### Minimum
+## Minimum
```agda
min-assoc : (x y z : Nat) → min x (min y z) ≡ min (min x y) z
@@ -371,3 +392,15 @@ min-zeror : (x : Nat) → min x 0 ≡ 0
min-zeror zero = refl
min-zeror (suc x) = refl
```
+
+## The factorial function
+
+```agda
+factorial-positive : ∀ n → Positive (factorial n)
+factorial-positive zero = s≤s 0≤x
+factorial-positive (suc n) = *-preserves-≤ 1 (suc n) 1 (factorial n) (s≤s 0≤x) (factorial-positive n)
+
+≤-factorial : ∀ n → n ≤ factorial n
+≤-factorial zero = 0≤x
+≤-factorial (suc n) = subst (_≤ factorial (suc n)) (*-oner (suc n)) (*-preserves-≤ (suc n) (suc n) 1 (factorial n) ≤-refl (factorial-positive n))
+```
diff --git a/src/Data/Rational/Base.lagda.md b/src/Data/Rational/Base.lagda.md
new file mode 100644
index 000000000..40bc1a12f
--- /dev/null
+++ b/src/Data/Rational/Base.lagda.md
@@ -0,0 +1,626 @@
+
+
+```agda
+module Data.Rational.Base where
+```
+
+# Rational numbers {defines="rational-numbers"}
+
+The ring of **rational numbers**, $\bQ$, is the
+[[localisation|localisation of a ring]] of the ring of [[integers]]
+$\bZ$, inverting every positive element. We've already done most of the
+work while implementing localisations:
+
+```agda
+PositiveΩ : Int → Ω
+PositiveΩ x .∣_∣ = Positive x
+PositiveΩ x .is-tr = hlevel 1
+
+private
+ module L = Loc ℤ-comm PositiveΩ record { has-1 = pos 0 ; has-* = *ℤ-positive }
+```
+
+
+
+Strictly speaking, we are done: we could simply define $\bQ$ to be the
+ring we just constructed. However, for the sake of implementation
+hiding, we wrap it as a distinct type constructor. This lets consumers
+of the type $\bQ$ forget that it's implemented as a localisation.
+
+```agda
+data ℚ : Type where
+ inc : ⌞ L.S⁻¹R ⌟ → ℚ
+
+toℚ : Fraction → ℚ
+toℚ x = inc (inc x)
+
+_+ℚ_ : ℚ → ℚ → ℚ
+_+ℚ_ (inc x) (inc y) = inc (x L.+ₗ y)
+
+_*ℚ_ : ℚ → ℚ → ℚ
+_*ℚ_ (inc x) (inc y) = inc (x L.*ₗ y)
+
+-ℚ_ : ℚ → ℚ
+-ℚ_ (inc x) = inc (L.-ₗ x)
+```
+
+
+
+However, clients of this module *will* need the fact that $\bQ$ is a
+quotient of the type of integer fractions. Therefore, we expose an
+elimination principle, saying that to show a [[proposition]] everywhere
+over $\bQ$, it suffices to do so at the fractions.
+
+```agda
+ℚ-elim-prop
+ : ∀ {ℓ} {P : ℚ → Type ℓ} (pprop : ∀ x → is-prop (P x))
+ → (f : ∀ x → P (toℚ x))
+ → ∀ x → P x
+ℚ-elim-prop pprop f (inc (inc x)) = f x
+ℚ-elim-prop pprop f (inc (glue r@(x , y , _) i)) = is-prop→pathp (λ i → pprop (inc (glue r i))) (f x) (f y) i
+ℚ-elim-prop pprop f (inc (squash x y p q i j)) =
+ is-prop→squarep
+ (λ i j → pprop (inc (squash x y p q i j)))
+ (λ i → go (inc x)) (λ i → go (inc (p i))) (λ i → go (inc (q i))) (λ i → go (inc y))
+ i j
+ where go = ℚ-elim-prop pprop f
+```
+
+
+
+Next, we show that sameness of fractions implies identity in $\bQ$, and
+the converse is true as well:
+
+```agda
+abstract
+ quotℚ : ∀ {x y} → x ≈ y → toℚ x ≡ toℚ y
+ quotℚ p = ap ℚ.inc (quot p)
+
+ unquotℚ : ∀ {x y} → toℚ x ≡ toℚ y → x ≈ y
+ unquotℚ p = ≈.effective (ap unℚ p)
+```
+
+Finally, we want to show that the type of rational numbers is discrete.
+To do this, we have to show that sameness of integer fractions is
+decidable, i.e. that, given fractions $x/s$ and $y/t$, we can decide
+whether there exists a $u \ne 0$ with $uxt = uys$. This is not automatic
+since $u$ can range over all integers! However, recall that this is
+equivalent to $u(xt - ys) = 0$. Since we know that $\bZ$ has no
+zerodivisors, if this is true, then either $u = 0$ or $xt - ys = 0$; by
+assumption, it can not be $u$. But if $xt - ys = 0$, then $xt = ys$!
+Conversely, if $xt = ys$, then we can take $u = 1$. Therefore, checking
+sameness of fractions boils down to checking whether they
+"cross-multiply" to the same thing.
+
+```agda
+from-same-rational : {x y : Fraction} → x ≈ y → x .↑ *ℤ y .↓ ≡ y .↑ *ℤ x .↓
+from-same-rational {x / s [ s≠0 ]} {y / t [ t≠0 ]} p = case L.≈→≈' p of λ where
+ u@(possuc u') (pos u') p → case *ℤ-is-zero u _ p of λ where
+ (inl u=0) → absurd (suc≠zero (pos-injective u=0))
+ (inr xt-ys=0) → ℤ.zero-diff xt-ys=0
+
+to-same-rational : {x y : Fraction} → x .↑ *ℤ y .↓ ≡ y .↑ *ℤ x .↓ → x ≈ y
+to-same-rational {x / s [ s≠0 ]} {y / t [ t≠0 ]} p = L.inc 1 (pos 0) (recover (sym (*ℤ-associative 1 x t) ·· ap (1 *ℤ_) p ·· *ℤ-associative 1 y s))
+
+Dec-same-rational : (x y : Fraction) → Dec (x ≈ y)
+Dec-same-rational f@(x / s [ _ ]) f'@(y / t [ _ ]) with x *ℤ t ≡? y *ℤ s
+... | yes p = yes (to-same-rational p)
+... | no xt≠ys = no λ p → xt≠ys (from-same-rational p)
+```
+
+
+
+
+
+There are a number of other properties of $\bZ{\loc{\ne 0}}$ that we can
+export as properties of $\bQ$; however, these are all trivial as above,
+so we do not remark on them any further.
+
+
+```agda
+_-ℚ_ : ℚ → ℚ → ℚ
+x -ℚ y = x +ℚ (-ℚ y)
+
+infixl 8 _+ℚ_ _-ℚ_
+infixl 9 _*ℚ_
+infix 10 -ℚ_
+
+_/_ : (x y : Int) ⦃ _ : Positive y ⦄ → ℚ
+_/_ x y ⦃ p ⦄ = toℚ (x / y [ p ])
+
+infix 11 _/_
+
+{-# DISPLAY ℚ.inc (Coeq.inc (_/_[_] x y p)) = x / y #-}
+
+_/1 : Int → ℚ
+x /1 = x / 1
+
+instance
+ H-Level-ℚ : ∀ {n} → H-Level ℚ (2 + n)
+ H-Level-ℚ = basic-instance 2 (Discrete→is-set auto)
+
+ Number-ℚ : Number ℚ
+ Number-ℚ .Number.Constraint _ = ⊤
+ Number-ℚ .Number.fromNat x = pos x /1
+
+ Negative-ℚ : Negative ℚ
+ Negative-ℚ .Negative.Constraint _ = ⊤
+ Negative-ℚ .Negative.fromNeg 0 = 0
+ Negative-ℚ .Negative.fromNeg (suc x) = negsuc x /1
+
+ Inductive-ℚ
+ : ∀ {ℓ ℓm} {P : ℚ → Type ℓ}
+ → ⦃ _ : Inductive ((x : Fraction) → P (toℚ x)) ℓm ⦄
+ → ⦃ _ : ∀ {x} → H-Level (P x) 1 ⦄
+ → Inductive (∀ x → P x) ℓm
+ Inductive-ℚ ⦃ r ⦄ .Inductive.methods = r .Inductive.methods
+ Inductive-ℚ ⦃ r ⦄ .Inductive.from f = ℚ-elim-prop (λ x → hlevel 1) (r .Inductive.from f)
+
+abstract
+ +ℚ-idl : ∀ x → 0 +ℚ x ≡ x
+ +ℚ-idl (inc x) = ap inc (L.+ₗ-idl x)
+
+ +ℚ-idr : ∀ x → x +ℚ 0 ≡ x
+ +ℚ-idr (inc x) = ap ℚ.inc (CRing.+-idr L.S⁻¹R)
+
+ +ℚ-associative : ∀ x y z → x +ℚ (y +ℚ z) ≡ (x +ℚ y) +ℚ z
+ +ℚ-associative (inc x) (inc y) (inc z) = ap inc (L.+ₗ-assoc x y z)
+
+ +ℚ-commutative : ∀ x y → x +ℚ y ≡ y +ℚ x
+ +ℚ-commutative (inc x) (inc y) = ap inc (L.+ₗ-comm x y)
+
+ *ℚ-idl : ∀ x → 1 *ℚ x ≡ x
+ *ℚ-idl (inc x) = ap inc (L.*ₗ-idl x)
+
+ *ℚ-idr : ∀ x → x *ℚ 1 ≡ x
+ *ℚ-idr (inc x) = ap ℚ.inc (CRing.*-idr L.S⁻¹R)
+
+ *ℚ-associative : ∀ x y z → x *ℚ (y *ℚ z) ≡ (x *ℚ y) *ℚ z
+ *ℚ-associative (inc x) (inc y) (inc z) = ap inc (L.*ₗ-assoc x y z)
+
+ *ℚ-commutative : ∀ x y → x *ℚ y ≡ y *ℚ x
+ *ℚ-commutative (inc x) (inc y) = ap inc (L.*ₗ-comm x y)
+
+ *ℚ-zerol : ∀ x → 0 *ℚ x ≡ 0
+ *ℚ-zerol (inc x) = ap ℚ.inc (CRing.*-zerol L.S⁻¹R {x})
+
+ *ℚ-zeror : ∀ x → x *ℚ 0 ≡ 0
+ *ℚ-zeror (inc x) = ap ℚ.inc (CRing.*-zeror L.S⁻¹R {x})
+
+ *ℚ-distribl : ∀ x y z → x *ℚ (y +ℚ z) ≡ x *ℚ y +ℚ x *ℚ z
+ *ℚ-distribl (inc x) (inc y) (inc z) = ap ℚ.inc (L.*ₗ-distribl x y z)
+
++ℚ-monoid : is-monoid 0 _+ℚ_
++ℚ-monoid = record { has-is-semigroup = record { has-is-magma = record { has-is-set = hlevel 2 } ; associative = λ {x} {y} {z} → +ℚ-associative x y z } ; idl = +ℚ-idl _ ; idr = +ℚ-idr _ }
+
+*ℚ-monoid : is-monoid 1 _*ℚ_
+*ℚ-monoid = record { has-is-semigroup = record { has-is-magma = record { has-is-set = hlevel 2 } ; associative = λ {x} {y} {z} → *ℚ-associative x y z } ; idl = *ℚ-idl _ ; idr = *ℚ-idr _ }
+```
+
+
+
+## As a field
+
+An important property of the ring $\bQ$ is that any nonzero rational
+number is invertible. Since inverses are unique when they exist --- the
+type of inverses is a proposition --- it suffices to show this at the
+more concrete level of integer fractions.
+
+```agda
+inverseℚ : (x : ℚ) → x ≠ 0 → Σ[ y ∈ ℚ ] (x *ℚ y ≡ 1)
+inverseℚ = ℚ-elim-prop is-p go where
+ abstract
+ is-p : (x : ℚ) → is-prop (x ≠ 0 → Σ[ y ∈ ℚ ] (x *ℚ y ≡ 1))
+ is-p x = Π-is-hlevel 1 λ _ (y , p) (z , q) → Σ-prop-path! (monoid-inverse-unique *ℚ-monoid x y z (*ℚ-commutative y x ∙ p) q)
+
+ rem₁ : ∀ x y → 1 *ℤ (x *ℤ y) *ℤ 1 ≡ 1 *ℤ (y *ℤ x)
+ rem₁ x y = ap (_*ℤ 1) (*ℤ-onel (x *ℤ y))
+ ∙ *ℤ-oner (x *ℤ y) ∙ *ℤ-commutative x y ∙ sym (*ℤ-onel (y *ℤ x))
+```
+
+This leaves us with three cases: either the fraction $x/y$ had a
+denominator of zero, contradicting our assumption, or its numerator is
+also nonzero (either positive or negative), so that we can form the
+fraction $y/x$. It's then routine to show that $(x/y)(y/x) = 1$ holds in
+$\bQ$.
+
+```agda
+ go : (x : Fraction) → toℚ x ≠ 0 → Σ[ y ∈ ℚ ] (toℚ x *ℚ y ≡ 1)
+ go (posz / y [ _ ]) nz = absurd (nz (quotℚ (L.inc 1 decide! refl)))
+ go (x@(possuc x') / y [ _ ]) nz = y / x , quotℚ (L.inc 1 decide! (rem₁ x y))
+ go (x@(negsuc x') / y [ p ]) nz with y | p
+ ... | possuc y | _ = negsuc y / possuc x' , quotℚ (L.inc 1 decide! (rem₁ (negsuc x') (negsuc y)))
+ ... | negsuc y | _ = possuc y / possuc x' , quotℚ (L.inc 1 decide! (rem₁ x (possuc y)))
+```
+
+## Reduced fractions
+
+We now show that the quotient defining $\bQ$ is [[*split*|split
+quotient]]: integer fractions have a well-defined notion of *normal
+form*, and similarity of fractions is equivalent to equality under
+normalisation. The procedure we formalise is the familiar one, sending a
+fraction $x/y$ to
+
+$$
+\frac{x \ndiv \gcd(x, y)}{y \ndiv \gcd(x, y)}
+$$.
+
+What remains is proving that this is actually a normalisation procedure,
+which takes up the remainder of this module.
+
+```agda
+reduce-fraction : Fraction → Fraction
+reduce-fraction (x / y [ p ]) = reduced module reduce where
+ gcd[x,y] : GCD (abs x) (abs y)
+ gcd[x,y] = Euclid.euclid (abs x) (abs y)
+```
+
+
+
+Our first obligation, to form the reduced fraction at all, is showing
+that the denominator is non-zero. This is pretty easy: we know that $y$
+is nonzero, so if $y \ndiv \gcd(x,y)$ were zero, we would have
+$$y = \gcd(x, y) * (y \ndiv \gcd(x,y)) = \gcd(x,y) * 0 = 0$$,
+which is a contradiction. A similar argument shows that $\gcd(x,y)$ is
+itself nonzero, a fact we'll need later.
+
+```agda
+ rem₁ : y/g ≠ 0
+ rem₁ y/g=0 with y/g | y/g=0 | y/g*g=y
+ ... | zero | y/g=0 | q = positive→nonzero p (abs-positive y (sym q))
+ ... | suc n | y/g=0 | q = absurd (suc≠zero y/g=0)
+
+ rem₂ : g ≠ 0
+ rem₂ g=0 = positive→nonzero p (abs-positive y (sym (sym (*-zeror y/g) ∙ ap (y/g *_) (sym g=0) ∙ y/g*g=y)))
+```
+
+Finally, we must quickly mention the issue of signs. Since `gcd`{.Agda}
+produces a natural number, we have to multiply it by the sign $\sgn(x)$
+of $x$, to make sure signs are preserved. Note that the denominator must
+be positive.
+
+```agda
+ reduced : Fraction
+ reduced = assign (sign x) x/g / pos y/g [ pos-positive rem₁ ]
+```
+
+Finally, we can calculate that these fractions are similar.
+
+```agda
+ related : (x / y [ p ]) ≈ reduced
+ related = L.inc (pos g) (pos-positive rem₂) $
+ pos g *ℤ x *ℤ pos y/g ≡⟨ solve 3 (λ x y z → x :* y :* z ≔ (z :* x) :* y) (pos g) x (pos y/g) refl ⟩
+ (pos y/g *ℤ pos g) *ℤ x ≡⟨ ap (_*ℤ x) (ap (assign pos) y/g*g=y) ⟩
+ assign pos (abs y) *ℤ x ≡⟨ ap₂ _*ℤ_ (assign-pos-positive y p) (sym (divides-*ℤ {n = x/g} {g} {x} (*-commutative g x/g ∙ x/g*g=x))) ⟩
+ y *ℤ (pos g *ℤ assign (sign x) x/g) ≡⟨ solve 3 (λ y g x → y :* (g :* x) ≔ g :* x :* y) y (pos g) (assign (sign x) x/g) refl ⟩
+ pos g ℤ.* assign (sign x) x/g ℤ.* y ∎
+```
+
+
+
+We'll now show that `reduce-fraction`{.Agda} respects similarity of
+fractions. We show this by an intermediate lemma, which says that, given
+a non-zero $s$ and a fraction $x/y$, we have
+$$
+\frac{xs \ndiv \gcd(xs, ys)}{ys \ndiv \gcd(xs, ys)} = \frac{x \ndiv \gcd(x, y)}{y \ndiv \gcd(x, y)}
+$$,
+as integer fractions (rather than rational numbers).
+
+```agda
+reduce-*r
+ : ∀ x y s (p : Positive y) (q : Positive s)
+ → reduce-fraction ((x *ℤ s) / (y *ℤ s) [ *ℤ-positive p q ])
+ ≡ reduce-fraction (x / y [ p ])
+reduce-*r x y s p q = Fraction-path (ap₂ assign sgn num) (ap Int.pos denom) where
+```
+
+
+
+The first observation is that $\gcd(xs, ys) = \gcd(x,y)s$, even when
+absolute values are involved.^[Keep in mind that the `gcd`{.Agda}
+function is defined over the naturals, and we're extending it to
+integers by $\gcd(x,y) = \gcd(\abs{x}, \abs{y})$.]
+
+```agda
+ p1 : gcdℤ (x *ℤ s) (y *ℤ s) ≡ gcdℤ x y * abs s
+ p1 = ap₂ gcd (abs-*ℤ x s) (abs-*ℤ y s) ∙ gcd-factor (abs x) (abs y) (abs s)
+```
+
+This implies that $$(xs \ndiv \gcd(xs, ys)) \gcd(x,y) s = x s$$, and,
+because multiplication by $s$ is injective, this in turn implies that
+$(xs \ndiv \gcd(xs, ys))\gcd(x, y)$ is also $x$. We conclude $(xs \ndiv
+\gcd(xs, ys)) = (x \ndiv \gcd(x, y))$, since both sides multiply with
+$\gcd(x, y)$ to $x$, and this multiplication is *also* injective.
+Therefore, our numerators have the same absolute value.
+
+```agda
+ num' : xs/gcd * gcdℤ x y ≡ abs x
+ num' = *-injr (abs s) (xs/gcd * m.g) (abs x) $
+ xs/gcd * gcdℤ x y * abs s ≡⟨ *-associative xs/gcd m.g (abs s) ⟩
+ xs/gcd * (gcdℤ x y * abs s) ≡˘⟨ ap (xs/gcd *_) p1 ⟩
+ xs/gcd * gcdℤ (x *ℤ s) (y *ℤ s) ≡⟨ n.x/g*g=x ⟩
+ abs (x *ℤ s) ≡⟨ abs-*ℤ x s ⟩
+ abs x * abs s ∎
+
+ num : xs/gcd ≡ x/gcd
+ num = *-injr (gcdℤ x y) xs/gcd x/gcd (num' ∙ sym m.x/g*g=x)
+```
+
+We must still show that the resulting numerators have the same sign.
+Fortunately, this boils down to a bit of algebra, plus the
+hyper-specific fact that $\sgn(ab^2) = \sgn(a)$, whenever $b$ is
+nonzero.^[Here, we're applying this lemma with $a = xy$ and $b = s$, and
+we have assumed $s$ nonzero. The $\sgn$ function is not fun.]
+
+```agda
+ sgn : sign (x *ℤ s) ≡ sign x
+ sgn = sign-*ℤ-positive x s q
+```
+
+A symmetric calculation shows that the denominators also have the same
+absolute value, and, since they're both positive in the resulting
+fraction, we're done.
+
+```agda
+ denom' : ys/gcd * gcdℤ x y ≡ abs y
+ denom' = *-injr (abs s) (ys/gcd * m.g) (abs y) (*-associative ys/gcd m.g (abs s) ∙ sym (ap (ys/gcd *_) p1) ∙ n.y/g*g=y ∙ abs-*ℤ y s)
+
+ denom : ys/gcd ≡ y/gcd
+ denom = *-injr (gcdℤ x y) ys/gcd y/gcd (denom' ∙ sym m.y/g*g=y)
+```
+
+We can use this to show that `reduce-fraction`{.Agda} sends similar
+fractions to *equal* normal forms: If $x/s \approx y/t$, we have $xt =
+ys$, and we can calculate
+$$
+\frac{x \ndiv \gcd(x, s)}{s \ndiv \gcd(x, s)}
+= \frac{xt \ndiv \gcd(xt, st)}{st \ndiv \gcd(xt, st)}
+= \frac{ys \ndiv \gcd(ys, ts)}{ts \ndiv \gcd(ys, ts)}
+= \frac{y \ndiv \gcd(y, t)}{t \ndiv \gcd(y, t)}
+$$
+using the previous lemma. Thus, by the general logic of [[split
+quotients]], we conclude that $\bQ$ is equivalent to the set of reduced
+integer fractions.
+
+```agda
+reduce-resp : (x y : Fraction) → x ≈ y → reduce-fraction x ≡ reduce-fraction y
+reduce-resp f@(x / s [ s≠0 ]) f'@(y / t [ t≠0 ]) p =
+ reduce-fraction (x / s [ s≠0 ]) ≡⟨ sym (reduce-*r x s t s≠0 t≠0) ⟩
+ reduce-fraction ((x *ℤ t) / (s *ℤ t) [ _ ]) ≡⟨ ap reduce-fraction (Fraction-path {x = _ / _ [ *ℤ-positive s≠0 t≠0 ]} {_ / _ [ *ℤ-positive t≠0 s≠0 ]} (from-same-rational p) (*ℤ-commutative s t)) ⟩
+ reduce-fraction ((y *ℤ s) / (t *ℤ s) [ _ ]) ≡⟨ reduce-*r y t s t≠0 s≠0 ⟩
+ reduce-fraction (y / t [ t≠0 ]) ∎
+
+integer-frac-splits : is-split-congruence L.Fraction-congruence
+integer-frac-splits = record
+ { has-is-set = hlevel 2
+ ; normalise = reduce-fraction
+ ; represents = elim! reduce.related
+ ; respects = reduce-resp
+ }
+```
+
+
diff --git a/src/Data/Rational/Order.lagda.md b/src/Data/Rational/Order.lagda.md
new file mode 100644
index 000000000..120af8de6
--- /dev/null
+++ b/src/Data/Rational/Order.lagda.md
@@ -0,0 +1,239 @@
+
+
+```agda
+module Data.Rational.Order where
+```
+
+
+
+# Ordering on rationals
+
+The field $\bQ$ of [[rational numbers]] inherits a [[partial order]]
+from the ring of integers $\bZ$, defining the relation
+$$
+\frac{x}{s} \le \frac{y}{t}
+$$
+to be $xt \le ys$. As usual, we define this first at the level of
+fractions, then prove that it extends to the quotient $\bQ$.
+
+```agda
+_≤ᶠ_ : Fraction → Fraction → Type
+(x / s [ _ ]) ≤ᶠ (y / t [ _ ]) = (x *ℤ t) ℤ.≤ (y *ℤ s)
+```
+
+The easiest way to show this is transitivity at the level of fractions,
+since it will follow directly from the definition that $q \approx q'$
+implies $q \le q'$. We can then prove that $q \le q'$ is invariant under
+$\approx$, on either side, by appealing to transitivity. The proof is
+not complicated, just annoying:
+
+```agda
+≤ᶠ-refl' : ∀ {x y} → x ≈ y → x ≤ᶠ y
+≤ᶠ-refl' {x@record{}} {y@record{}} p = ℤ.≤-refl' (from-same-rational p)
+
+≤ᶠ-trans : ∀ x y z → x ≤ᶠ y → y ≤ᶠ z → x ≤ᶠ z
+≤ᶠ-trans (x / s [ pos s' ]) (y / t [ pos t' ]) (z / u [ pos u' ]) α β =
+ (ℤ.*ℤ-cancel-≤r {t} $
+ x *ℤ u *ℤ t =⟨ solve 3 (λ x u t → x :* u :* t ≔ x :* t :* u) x u t refl ⟩
+ x *ℤ t *ℤ u ≤⟨ ℤ.*ℤ-preserves-≤r u α ⟩
+ y *ℤ s *ℤ u =⟨ solve 3 (λ y s u → y :* s :* u ≔ y :* u :* s) y s u refl ⟩
+ y *ℤ u *ℤ s ≤⟨ ℤ.*ℤ-preserves-≤r s β ⟩
+ z *ℤ t *ℤ s =⟨ solve 3 (λ z t s → z :* t :* s ≔ z :* s :* t) z t s refl ⟩
+ z *ℤ s *ℤ t ≤∎)
+```
+
+
+
+We can then lift this to a family of [[propositions]] over $\bQ \times
+\bQ$. The strategy for showing it respects the quotient is as outlined
+above, so we'll leave this in a ``{.html} block.
+
+
+```agda
+private
+ leℚ : ℚ → ℚ → Prop lzero
+ leℚ (inc x) (inc y) =
+ Coeq-rec₂ (hlevel 2) work
+ (λ a (x , y , r) → r2 x y a r)
+ (λ a (x , y , r) → r1 a x y r) x y
+ where
+ work : Fraction → Fraction → Prop lzero
+ ∣ work x y ∣ = x ≤ᶠ y
+ work record{} record{} .is-tr = hlevel 1
+
+ r1 : ∀ u x y → x ≈ y → work u x ≡ work u y
+ r1 u@record{} x@record{} y@record{} p' = n-ua (prop-ext!
+ (λ α → ≤ᶠ-trans u x y α (≤ᶠ-refl' p'))
+ (λ α → ≤ᶠ-trans u y x α (≤ᶠ-refl' (≈.symᶜ p'))))
+
+ r2 : ∀ x y u → x ≈ y → work x u ≡ work y u
+ r2 u@record{} x@record{} y@record{} p' = n-ua (prop-ext!
+ (λ α → ≤ᶠ-trans x u y (≤ᶠ-refl' (≈.symᶜ p')) α)
+ (λ α → ≤ᶠ-trans u x y (≤ᶠ-refl' p') α))
+```
+
+
+
+We define the type family `_≤_`{.Agda} as a record type, wrapping
+`orderℚ`{.Agda}, to help out type inference: `orderℚ`{.Agda} is a pretty
+nasty definition, whereas an application of a record name is always a
+normal form.
+
+```agda
+record _≤_ (x y : ℚ) : Type where
+ constructor inc
+ field
+ lower : ⌞ leℚ x y ⌟
+```
+
+
+
+By lifting our proofs about `_≤ᶠ_`{.Agda} through this record type, we
+can prove that the ordering on the rational numbers is decidable,
+reflexive, transitive, and antisymmetric.
+
+```agda
+≤-dec : ∀ x y → Dec (x ≤ y)
+≤-dec = elim! go where
+ go : ∀ x y → Dec (toℚ x ≤ toℚ y)
+ go x@record{} y@record{} with holds? ((↑ x *ℤ ↓ y) ℤ.≤ (↑ y *ℤ ↓ x))
+ ... | yes p = yes (inc p)
+ ... | no ¬p = no (¬p ∘ lower)
+
+instance
+ Dec-≤ : ∀ {x y} → Dec (x ≤ y)
+ Dec-≤ {x} {y} = ≤-dec x y
+
+abstract
+ toℚ≤ : ∀ {x y} → (↑ x *ℤ ↓ y) ℤ.≤ (↑ y *ℤ ↓ x) → toℚ x ≤ toℚ y
+ toℚ≤ {record{}} {record{}} p = inc p
+
+ ≤-refl : ∀ {x} → x ≤ x
+ ≤-refl {x} = work x where
+ work : ∀ x → x ≤ x
+ work = elim! λ f → toℚ≤ ℤ.≤-refl
+
+ ≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
+ ≤-trans {x} {y} {z} = work x y z where
+ work : ∀ x y z → x ≤ y → y ≤ z → x ≤ z
+ work = elim! λ x y z p q → inc (≤ᶠ-trans x y z (p .lower) (q .lower))
+
+ ≤-antisym : ∀ {x y} → x ≤ y → y ≤ x → x ≡ y
+ ≤-antisym {x} {y} = work x y where
+ work : ∀ x y → x ≤ y → y ≤ x → x ≡ y
+ work = elim! λ where
+ x@record{} y@record{} p q → quotℚ (to-same-rational (ℤ.≤-antisym (p .lower) (q .lower)))
+```
+
+## Algebraic properties
+
+We can also show that the ordering on $\bQ$ behaves well with respect to
+its algebraic structure. For example, the addition function is monotone
+in both arguments, and division by a positive integer preserves the
+order.
+
+```agda
+ common-denominator-≤ : ∀ {x y d} (p : ℤ.Positive d) → x ℤ.≤ y → toℚ (x / d [ p ]) ≤ toℚ (y / d [ p ])
+ common-denominator-≤ {d = d} (pos _) p = inc (ℤ.*ℤ-preserves-≤r d p)
+
+ +ℚ-preserves-≤ : ∀ x y a b → x ≤ y → a ≤ b → (x +ℚ a) ≤ (y +ℚ b)
+ +ℚ-preserves-≤ = ℚ-elim-propⁿ 4 λ d d≠0 x y a b (inc p) (inc q) →
+ common-denominator-≤ (ℤ.*ℤ-positive d≠0 d≠0) $
+ x *ℤ d +ℤ a *ℤ d ≤⟨ ℤ.+ℤ-preserves-≤r (a *ℤ d) _ _ p ⟩
+ y *ℤ d +ℤ a *ℤ d ≤⟨ ℤ.+ℤ-preserves-≤l (y *ℤ d) _ _ q ⟩
+ y *ℤ d +ℤ b *ℤ d ≤∎
+
+ *ℚ-nonnegative : ∀ x y → 0 ≤ x → 0 ≤ y → 0 ≤ (x *ℚ y)
+ *ℚ-nonnegative = ℚ-elim-propⁿ 2 λ d d≠0 x y (inc p) (inc q) → inc (ℤ.≤-trans
+ (ℤ.*ℤ-nonnegative
+ (ℤ.≤-trans p (ℤ.≤-refl' (ℤ.*ℤ-oner x)))
+ (ℤ.≤-trans q (ℤ.≤-refl' (ℤ.*ℤ-oner y))))
+ (ℤ.≤-refl' (sym (ℤ.*ℤ-oner (x *ℤ y)))))
+```
+
+## Positivity
+
+We can also lift the notion of positivity from the integers to the
+rational numbers. A fraction is positive if its numerator is positive.
+
+```agda
+private
+ positiveℚ : ℚ → Prop lzero
+ positiveℚ (inc x) = Coeq-rec (λ f → el! (ℤ.Positive (↑ f))) (λ (x , y , p) → r x y p) x where
+ r : ∀ x y → x ≈ y → el! (ℤ.Positive (↑ x)) ≡ el! (ℤ.Positive (↑ y))
+ r (x / s [ ps ]) (y / t [ pt ]) r with r ← from-same-rational r = n-ua (prop-ext!
+ (λ px → ℤ.*ℤ-positive-cancel ps (subst ℤ.Positive (r ∙ ℤ.*ℤ-commutative y s) (ℤ.*ℤ-positive px pt)))
+ λ py → ℤ.*ℤ-positive-cancel pt (subst ℤ.Positive (sym r ∙ ℤ.*ℤ-commutative x t) (ℤ.*ℤ-positive py ps)))
+
+record Positive (q : ℚ) : Type where
+ constructor inc
+ field
+ lower : ⌞ positiveℚ q ⌟
+```
+
+
+
+This has the expected interaction with the ordering and the algebraic
+operations.
+
+```agda
+nonnegative-nonzero→positive : ∀ {x} → 0 ≤ x → x ≠ 0 → Positive x
+nonnegative-nonzero→positive = work _ where
+ work : ∀ x → 0 ≤ x → x ≠ 0 → Positive x
+ work = ℚ-elim-propⁿ 1 λ where
+ d p posz (inc q) r → absurd (r (ext refl))
+ d p (possuc x) (inc q) r → inc (pos x)
+
+*ℚ-positive : ∀ {x y} → Positive x → Positive y → Positive (x *ℚ y)
+*ℚ-positive = work _ _ where
+ work : ∀ x y → Positive x → Positive y → Positive (x *ℚ y)
+ work = ℚ-elim-propⁿ 2 λ d p a b (inc x) (inc y) → inc (ℤ.*ℤ-positive x y)
+
++ℚ-positive : ∀ {x y} → Positive x → Positive y → Positive (x +ℚ y)
++ℚ-positive = work _ _ where
+ work : ∀ x y → Positive x → Positive y → Positive (x +ℚ y)
+ work = ℚ-elim-propⁿ 2 λ d p a b (inc x) (inc y) → inc (ℤ.+ℤ-positive (ℤ.*ℤ-positive x p) (ℤ.*ℤ-positive y p))
+```
diff --git a/src/Data/Set/Coequaliser.lagda.md b/src/Data/Set/Coequaliser.lagda.md
index c50a763da..bc82ad9d7 100644
--- a/src/Data/Set/Coequaliser.lagda.md
+++ b/src/Data/Set/Coequaliser.lagda.md
@@ -348,6 +348,16 @@ inc-is-surjective (squash x y p q i j) = is-prop→squarep
(λ j → inc-is-surjective (p j))
(λ j → inc-is-surjective (q j))
(λ i → inc-is-surjective y) i j
+
+Quot-op₂ : ∀ {C : Type ℓ} {T : C → C → Type ℓ'}
+ → (∀ x → R x x) → (∀ y → S y y)
+ → (_⋆_ : A → B → C)
+ → ((a b : A) (x y : B) → R a b → S x y → T (a ⋆ x) (b ⋆ y))
+ → A / R → B / S → C / T
+Quot-op₂ Rr Sr op resp =
+ Coeq-rec₂ squash (λ x y → inc (op x y))
+ (λ { z (x , y , r) → quot (resp x y z z r (Sr z)) })
+ λ { z (x , y , r) → quot (resp z z x y (Rr z) r) }
```
-->
@@ -427,21 +437,27 @@ proof that equivalence relations are `effective`{.Agda}.
```agda
effective : ∀ {x y : A} → Path quotient (inc x) (inc y) → x ∼ y
effective = equiv→inverse is-effective
+
+ reflᶜ' : ∀ {x y : A} → x ≡ y → x ∼ y
+ reflᶜ' {x = x} p = transport (λ i → x ∼ p i) reflᶜ
+
+ op₂
+ : (f : A → A → A)
+ → (∀ x y u v → x ∼ u → y ∼ v → f x y ∼ f u v)
+ → quotient → quotient → quotient
+ op₂ f r = Quot-op₂ (λ x → reflᶜ) (λ x → reflᶜ) f (λ a b x y → r a x b y)
+
+ op₂-comm
+ : (f : A → A → A)
+ → (∀ a b → f a b ∼ f b a)
+ → (∀ x u v → u ∼ v → f x u ∼ f x v)
+ → quotient → quotient → quotient
+ op₂-comm f c r = op₂ f (λ x y u v p q → r x y v q ∙ᶜ c x v ∙ᶜ r v x u p ∙ᶜ c v u)
```
-->
+
+```agda
+module Data.Set.Coequaliser.Split where
+```
+
+# Split quotients {defines="split-quotient"}
+
+Recall that a [[quotient]] of a set $A$ by an equivalence relation $x
+\sim y$ allows us to "replace" the identity type of $A$ by the relation
+$R$, by means of a [[surjection]] $[-] : A \epi A/\sim$ having $[x] =
+[y]$ equivalent to $x \sim y$. However, depending on the specifics of
+$R$, we may not need to actually take a quotient after all! It may be
+the case that $A/\sim$ is equivalent to a particular *subset* of $A$.
+When this is the case, we say that the quotient is **split**. This
+module outlines sufficient conditions for a quotient to split, by
+appealing to our intuition about *normal forms*.
+
+
+
+```agda
+record is-split-congruence (R : Congruence A ℓ') : Type (level-of A ⊔ ℓ') where
+ open Congruence R
+
+ field
+ has-is-set : is-set A
+```
+
+A normalisation function $n : A \to A$, for an equivalence relation $x
+\sim y$, is one that is the identity "up to $\sim$", i.e., we have $x
+\sim n(x)$, and which respects the relation, in that, if we have $x \sim
+y$, then $n(x) = n(y)$.
+
+```agda
+ normalise : A → A
+
+ represents : ∀ x → x ∼ normalise x
+ respects : ∀ x y → x ∼ y → normalise x ≡ normalise y
+```
+
+
+
+It turns out that this is just enough to asking for a splitting of the
+quotient map $[-]$: We can define a function sending each $x : A/\sim$
+to a fibre of the quotient map over it, by induction. At the points of
+$A$, we take the fibre over $[x]$ to be $n(x)$, and we have $[n(x)] =
+[x]$ by the first assumption. By the second assumption, this procedure
+respects the quotient.
+
+```agda
+ splitting : (x : Congruence.quotient R) → fibre inc x
+ splitting (inc x) = record { fst = normalise x ; snd = quot (symᶜ (represents x)) }
+ splitting (glue (x , y , r) i) = record
+ { fst = respects x y r i
+ ; snd = is-prop→pathp (λ i → Coeq.squash (inc (respects x y r i)) (quot r i))
+ (quot (symᶜ (represents x))) (quot (symᶜ (represents y))) i
+ }
+ splitting (squash x y p q i j) = is-set→squarep
+ (λ i j → hlevel {T = fibre inc (squash x y p q i j)} 2)
+ (λ i → splitting x) (λ i → splitting (p i)) (λ i → splitting (q i)) (λ i → splitting y) i j
+```
+
+
+
+Two other consequences of these assumptions are that the normalisation
+function is literally idempotent, and that it additionally *reflects*
+the quotient relation, in that $x \sim y$ is *equivalent to* $n(x) =
+n(y)$.
+
+```agda
+ normalises : ∀ x → normalise (normalise x) ≡ normalise x
+ normalises x = respects (normalise x) x (symᶜ (represents x))
+
+ reflects : ∀ x y → normalise x ≡ normalise y → x ∼ y
+ reflects x y p = represents x ∙ᶜ reflᶜ' p ∙ᶜ symᶜ (represents y)
+```
+
+Finally, we show that any splitting of the quotient map generates a
+normalisation procedure in the above sense: if we have a map $c : A/\sim
+\to A$, we define the normalisation procedure to be $n(x) = c[x]$.
+
+```agda
+split-surjection→is-split-congruence
+ : ⦃ _ : H-Level A 2 ⦄ (R : Congruence A ℓ)
+ → (∀ x → fibre {B = Congruence.quotient R} inc x)
+ → is-split-congruence R
+split-surjection→is-split-congruence R split = record
+ { has-is-set = hlevel 2
+ ; normalise = λ x → split (inc x) .fst
+ ; represents = λ x → effective (sym (split (inc x) .snd))
+ ; respects = λ x y p → ap (fst ∘ split) (quot p)
+ } where open Congruence R
+```
diff --git a/src/Data/Set/Material.lagda.md b/src/Data/Set/Material.lagda.md
index c4544b8ca..a02f35809 100644
--- a/src/Data/Set/Material.lagda.md
+++ b/src/Data/Set/Material.lagda.md
@@ -520,7 +520,7 @@ constructor to the successor set.
```agda
ℕV : V ℓ
- ℕV = set (Lift ℓ Nat) λ x → go (Lift.lower x) where
+ ℕV = set (Lift ℓ Nat) λ x → go (lower x) where
go : Nat → V ℓ
go zero = ∅V
go (suc x) = suc-V (go x)
@@ -558,7 +558,7 @@ set.
(inr w) → do
(pred , ix , w) ← w
(ix , x) ← ix
- pure (lift (suc (ix .Lift.lower)) , ap₂ _∪V_ x (ap singleton x) ∙ sym w))
+ pure (lift (suc (ix .lower)) , ap₂ _∪V_ x (ap singleton x) ∙ sym w))
```
## Replacement
diff --git a/src/Data/Sum/Properties.lagda.md b/src/Data/Sum/Properties.lagda.md
index bab379dec..7a50bccd2 100644
--- a/src/Data/Sum/Properties.lagda.md
+++ b/src/Data/Sum/Properties.lagda.md
@@ -73,8 +73,8 @@ the `Code`{.Agda} computes to `the empty type`{.Agda ident=⊥}.
```agda
decode : {x y : A ⊎ B} → Code x y → x ≡ y
- decode {x = inl x} {y = inl x₁} code = ap inl (Lift.lower code)
- decode {x = inr x} {y = inr x₁} code = ap inr (Lift.lower code)
+ decode {x = inl x} {y = inl x₁} code = ap inl (lower code)
+ decode {x = inr x} {y = inr x₁} code = ap inr (lower code)
```
In the inverse direction, we have a procedure for turning paths into
diff --git a/src/Order/DCPO/Free.lagda.md b/src/Order/DCPO/Free.lagda.md
index 89334d4bd..9f6558174 100644
--- a/src/Order/DCPO/Free.lagda.md
+++ b/src/Order/DCPO/Free.lagda.md
@@ -281,7 +281,7 @@ $$.
```agda
part-counit : ↯ Ob → Ob
- part-counit x = ⋃-prop (x .elt ⊙ Lift.lower) def-prop where abstract
+ part-counit x = ⋃-prop (x .elt ⊙ lower) def-prop where abstract
def-prop : is-prop (Lift o ⌞ x ⌟)
def-prop = hlevel 1
```
@@ -298,7 +298,7 @@ And if $x$ is undefined, then this is the bottom element.
part-counit-¬elt : (x : ↯ Ob) → (⌞ x ⌟ → ⊥) → part-counit x ≡ bottom
part-counit-¬elt x ¬def = ≤-antisym
- (⋃-prop-least _ _ _ (λ p → absurd (¬def (Lift.lower p))))
+ (⋃-prop-least _ _ _ (λ p → absurd (¬def (lower p))))
(bottom≤x _)
```
@@ -324,7 +324,7 @@ curious reader.
part-counit-⊑ {x = x} {y = y} p = ⋃-prop-least _ _ (part-counit y) λ (lift i) →
x .elt i =˘⟨ p .refines i ⟩
y .elt (p .implies i) ≤⟨ ⋃-prop-le _ _ (lift (p .implies i)) ⟩
- ⋃-prop (y .elt ⊙ Lift.lower) _ ≤∎
+ ⋃-prop (y .elt ⊙ lower) _ ≤∎
part-counit-lub s sdir .is-lub.fam≤lub i =
⋃-prop-least _ _ _ λ (lift p) →
@@ -358,10 +358,10 @@ Free-Pointed-dcpo⊣Forget-Pointed-dcpo .counit .is-natural D E f = ext λ x →
sym $ Strict-scott.pres-⋃-prop f _ _ _
Free-Pointed-dcpo⊣Forget-Pointed-dcpo .zig {A} = ext λ x → part-ext
- (A?.⋃-prop-least _ _ x (λ p → always-⊒ (Lift.lower p , refl)) .implies)
+ (A?.⋃-prop-least _ _ x (λ p → always-⊒ (lower p , refl)) .implies)
(λ p → A?.⋃-prop-le _ _ (lift p) .implies tt)
(λ p q →
- sym (A?.⋃-prop-least _ _ x (λ p → always-⊒ (Lift.lower p , refl)) .refines p)
+ sym (A?.⋃-prop-least _ _ x (λ p → always-⊒ (lower p , refl)) .refines p)
∙ ↯-indep x)
where module A? = Pointed-dcpo (Parts-pointed-dcpo A)
diff --git a/src/Order/DCPO/Pointed.lagda.md b/src/Order/DCPO/Pointed.lagda.md
index a4f4df9a5..aa373fee2 100644
--- a/src/Order/DCPO/Pointed.lagda.md
+++ b/src/Order/DCPO/Pointed.lagda.md
@@ -530,7 +530,7 @@ Scott-continuous.
pres-bot : ∀ x → is-bottom D.poset x → is-bottom E.poset (f x)
pres-bot x x-bot y =
f x E.≤⟨ monotone (x-bot _) ⟩
- f (D.⋃-semi _ _) E.≤⟨ is-lub.least (pres-⋃-semi (λ x → absurd (x .Lift.lower)) (λ ())) y (λ ()) ⟩
+ f (D.⋃-semi _ _) E.≤⟨ is-lub.least (pres-⋃-semi (λ x → absurd (x .lower)) (λ ())) y (λ ()) ⟩
y E.≤∎
```
@@ -567,6 +567,6 @@ families, then $f$ must be monotonic, and thus strictly Scott-continuous.
(to-scott-directed f
(λ s dir x lub → pres s (is-directed-family.semidirected dir) x lub))
(λ x x-bot y → is-lub.least
- (pres _ (λ x → absurd (x .Lift.lower)) x (lift-is-lub (is-bottom→is-lub D.poset {f = λ ()} x-bot)))
+ (pres _ (λ x → absurd (x .lower)) x (lift-is-lub (is-bottom→is-lub D.poset {f = λ ()} x-bot)))
y (λ ()))
```
diff --git a/src/Order/Diagram/Glb.lagda.md b/src/Order/Diagram/Glb.lagda.md
index 3d1deddd5..38c58654a 100644
--- a/src/Order/Diagram/Glb.lagda.md
+++ b/src/Order/Diagram/Glb.lagda.md
@@ -92,25 +92,25 @@ module _ {o ℓ} {P : Poset o ℓ} where
lift-is-glb
: ∀ {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I → Ob} {glb}
- → is-glb P F glb → is-glb P (F ⊙ Lift.lower {ℓ = ℓᵢ'}) glb
+ → is-glb P F glb → is-glb P (F ⊙ lower {ℓ = ℓᵢ'}) glb
lift-is-glb is .glb≤fam (lift ix) = is .glb≤fam ix
lift-is-glb is .greatest ub' le = is .greatest ub' (le ⊙ lift)
lift-glb
: ∀ {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I → Ob}
- → Glb P F → Glb P (F ⊙ Lift.lower {ℓ = ℓᵢ'})
+ → Glb P F → Glb P (F ⊙ lower {ℓ = ℓᵢ'})
lift-glb glb .Glb.glb = Glb.glb glb
lift-glb glb .Glb.has-glb = lift-is-glb (Glb.has-glb glb)
lower-is-glb
: ∀ {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I → Ob} {glb}
- → is-glb P (F ⊙ Lift.lower {ℓ = ℓᵢ'}) glb → is-glb P F glb
+ → is-glb P (F ⊙ lower {ℓ = ℓᵢ'}) glb → is-glb P F glb
lower-is-glb is .glb≤fam ix = is .glb≤fam (lift ix)
- lower-is-glb is .greatest ub' le = is .greatest ub' (le ⊙ Lift.lower)
+ lower-is-glb is .greatest ub' le = is .greatest ub' (le ⊙ lower)
lower-glb
: ∀ {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I → Ob}
- → Glb P (F ⊙ Lift.lower {ℓ = ℓᵢ'}) → Glb P F
+ → Glb P (F ⊙ lower {ℓ = ℓᵢ'}) → Glb P F
lower-glb glb .Glb.glb = Glb.glb glb
lower-glb glb .Glb.has-glb = lower-is-glb (Glb.has-glb glb)
```
diff --git a/src/Order/Diagram/Lub.lagda.md b/src/Order/Diagram/Lub.lagda.md
index 96f1c7967..78f03be20 100644
--- a/src/Order/Diagram/Lub.lagda.md
+++ b/src/Order/Diagram/Lub.lagda.md
@@ -90,25 +90,25 @@ module _ {o ℓ} {P : Poset o ℓ} where
lift-is-lub
: ∀ {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I → Ob} {lub}
- → is-lub P F lub → is-lub P (F ⊙ Lift.lower {ℓ = ℓᵢ'}) lub
+ → is-lub P F lub → is-lub P (F ⊙ lower {ℓ = ℓᵢ'}) lub
lift-is-lub is .fam≤lub (lift ix) = is .fam≤lub ix
lift-is-lub is .least ub' le = is .least ub' (le ⊙ lift)
lift-lub
: ∀ {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I → Ob}
- → Lub P F → Lub P (F ⊙ Lift.lower {ℓ = ℓᵢ'})
+ → Lub P F → Lub P (F ⊙ lower {ℓ = ℓᵢ'})
lift-lub lub .Lub.lub = Lub.lub lub
lift-lub lub .Lub.has-lub = lift-is-lub (Lub.has-lub lub)
lower-is-lub
: ∀ {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I → Ob} {lub}
- → is-lub P (F ⊙ Lift.lower {ℓ = ℓᵢ'}) lub → is-lub P F lub
+ → is-lub P (F ⊙ lower {ℓ = ℓᵢ'}) lub → is-lub P F lub
lower-is-lub is .fam≤lub ix = is .fam≤lub (lift ix)
- lower-is-lub is .least ub' le = is .least ub' (le ⊙ Lift.lower)
+ lower-is-lub is .least ub' le = is .least ub' (le ⊙ lower)
lower-lub
: ∀ {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I → Ob}
- → Lub P (F ⊙ Lift.lower {ℓ = ℓᵢ'}) → Lub P F
+ → Lub P (F ⊙ lower {ℓ = ℓᵢ'}) → Lub P F
lower-lub lub .Lub.lub = Lub.lub lub
lower-lub lub .Lub.has-lub = lower-is-lub (Lub.has-lub lub)
```
diff --git a/src/Order/Instances/Lift.lagda.md b/src/Order/Instances/Lift.lagda.md
index b60cbc6d9..caf76276f 100644
--- a/src/Order/Instances/Lift.lagda.md
+++ b/src/Order/Instances/Lift.lagda.md
@@ -20,7 +20,7 @@ Fortunately you can uniformly lift the poset to this bigger universe.
```agda
Liftᵖ : ∀ {o r} o′ r′ → Poset o r → Poset (o ⊔ o′) (r ⊔ r′)
Liftᵖ o' r' X .Poset.Ob = Lift o' ⌞ X ⌟
-Liftᵖ o' r' X .Poset._≤_ x y = Lift r' $ (X .Poset._≤_) (Lift.lower x) (Lift.lower y)
+Liftᵖ o' r' X .Poset._≤_ x y = Lift r' $ (X .Poset._≤_) (lower x) (lower y)
Liftᵖ o' r' X .Poset.≤-thin = Lift-is-hlevel 1 $ X .Poset.≤-thin
Liftᵖ o' r' X .Poset.≤-refl = lift $ X .Poset.≤-refl
Liftᵖ o' r' X .Poset.≤-trans (lift p) (lift q) = lift (X .Poset.≤-trans p q)
diff --git a/src/Order/Semilattice/Join/Reasoning.lagda.md b/src/Order/Semilattice/Join/Reasoning.lagda.md
index a6ae3a657..a2b1210de 100644
--- a/src/Order/Semilattice/Join/Reasoning.lagda.md
+++ b/src/Order/Semilattice/Join/Reasoning.lagda.md
@@ -11,6 +11,8 @@ open import Order.Base
import Cat.Reasoning
import Order.Reasoning
+
+open is-monoid
```
-->
diff --git a/src/Order/Semilattice/Meet/Reasoning.lagda.md b/src/Order/Semilattice/Meet/Reasoning.lagda.md
index 438e79baf..e8daf4581 100644
--- a/src/Order/Semilattice/Meet/Reasoning.lagda.md
+++ b/src/Order/Semilattice/Meet/Reasoning.lagda.md
@@ -11,6 +11,8 @@ open import Order.Base
import Cat.Reasoning
import Order.Reasoning
+
+open is-monoid
```
-->
diff --git a/src/Topoi/Base.lagda.md b/src/Topoi/Base.lagda.md
index cb971faed..9cc78ae50 100644
--- a/src/Topoi/Base.lagda.md
+++ b/src/Topoi/Base.lagda.md
@@ -1,26 +1,34 @@