ring localisations and rational numbers (#429)

numbers 👎
the1lab · Sep 8, 2024 · afcf848 · afcf848
1 parent a122947
commit afcf848
Show file tree

Hide file tree

Showing 79 changed files with 2,208 additions and 378 deletions.
diff --git 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
@@ -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
 ```
 
 <!--
 ```agda
   Lift-is-hlevel' : ∀ n → is-hlevel (Lift ℓ' A) n → is-hlevel A n
-  Lift-is-hlevel' n lift-hl = retract→is-hlevel n Lift.lower lift (λ _ → refl) lift-hl
+  Lift-is-hlevel' n lift-hl = retract→is-hlevel n lower lift (λ _ → refl) lift-hl
 ```
 -->
 

diff --git 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
@@ -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
@@ -77,6 +77,8 @@ record Lift {a} ℓ (A : Type a) : Type (a ⊔ ℓ) where
 
 <!--
 ```agda
+open Lift public
+
 instance
   Lift-instance : ∀ {ℓ ℓ'} {A : Type ℓ} → ⦃ A ⦄ → Lift ℓ' A
   Lift-instance ⦃ x ⦄ = lift x

diff --git a/src/1Lab/Underlying.agda b/src/1Lab/Underlying.agda
@@ -54,7 +54,7 @@ instance
     : ∀ {ℓ ℓ'} {A : Type ℓ} ⦃ ua : Underlying A ⦄
     → Underlying (Lift ℓ' A)
   Underlying-Lift ⦃ ua ⦄ .ℓ-underlying = ua .ℓ-underlying
-  Underlying-Lift .⌞_⌟ x = ⌞ x .Lift.lower ⌟
+  Underlying-Lift .⌞_⌟ x = ⌞ x .lower ⌟
 
   Underlying-Bool : Underlying Bool
   Underlying-Bool = record { ⌞_⌟ = So }

diff --git a/src/1Lab/Univalence.lagda.md b/src/1Lab/Univalence.lagda.md
@@ -466,10 +466,10 @@ ident=lift} is still an equivalence:
 univalence-lift : {A B : Type ℓ} → is-equiv (λ e → lift (path→equiv {A = A} {B} e))
 univalence-lift {ℓ = ℓ} = is-iso→is-equiv morp where
   morp : is-iso (λ e → lift {ℓ = lsuc ℓ} (path→equiv e))
-  morp .is-iso.inv x = ua (x .Lift.lower)
+  morp .is-iso.inv x = ua (x .lower)
   morp .is-iso.rinv x =
-    lift (path→equiv (ua (x .Lift.lower))) ≡⟨ ap lift (Path≃Equiv .snd .is-iso.rinv _) ⟩
-    x                                      ∎
+    lift (path→equiv (ua (x .lower))) ≡⟨ ap lift (Path≃Equiv .snd .is-iso.rinv _) ⟩
+    x                                 ∎
   morp .is-iso.linv x = Path≃Equiv .snd .is-iso.linv _
 ```
 

diff --git a/src/Algebra/Group.lagda.md b/src/Algebra/Group.lagda.md
@@ -5,12 +5,12 @@ open import 1Lab.Prelude
 
 open import Algebra.Magma.Unital hiding (idl ; idr)
 open import Algebra.Semigroup
-open import Algebra.Monoid hiding (idl ; idr)
+open import Algebra.Monoid
 open import Algebra.Magma
 
-open import Cat.Instances.Delooping
+import Algebra.Monoid.Reasoning as Mon
 
-import Cat.Reasoning
+open is-monoid hiding (idl ; idr)
 ```
 -->
 
@@ -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
@@ -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
@@ -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
@@ -1,14 +1,15 @@
 <!--
 ```agda
 open import Algebra.Semigroup using (is-semigroup)
-open import Algebra.Prelude
 open import Algebra.Monoid using (is-monoid)
 open import Algebra.Group
 open import Algebra.Magma using (is-magma)
 
 open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Properties
 open import Cat.Prelude
+
+import Cat.Reasoning as Cat
 ```
 -->
 

diff --git a/src/Algebra/Group/Cat/Monadic.lagda.md b/src/Algebra/Group/Cat/Monadic.lagda.md
@@ -2,15 +2,16 @@
 ```agda
 open import Algebra.Group.Cat.Base
 open import Algebra.Group.Free
-open import Algebra.Prelude
 open import Algebra.Monoid
 open import Algebra.Group
 
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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