wip: prime numbers

src/1Lab/Classical.lagda.md

@@ -153,7 +153,7 @@ gives us a section $\Sigma P \to 2$.
 ```agda
 module _ (split : Surjections-split) (P : Ω) where
   section : ∥ ((x : Susp ∣ P ∣) → fibre 2→Σ x) ∥
-  section = split Bool-is-set (Susp-prop-is-set (hlevel 1)) 2→Σ 2→Σ-surjective
+  section = split (hlevel 2) (Susp-prop-is-set (hlevel 1)) 2→Σ 2→Σ-surjective
 ```
 
 But a section is always injective, and the booleans are [[discrete]], so we can

src/1Lab/Equiv.lagda.md

@@ -202,7 +202,7 @@ point with, rather than being a property of points.
 
 ```agda
 fibre : (A → B) → B → Type _
-fibre {A = A} f y = Σ[ x ∈ A ] (f x ≡ y)
+fibre {A = A} f y = Σ[ x ∈ A ] f x ≡ y
 ```
 :::
 
@@ -1094,13 +1094,13 @@ lift-inj p = ap Lift.lower p
 fibre-∘-≃
   : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
   → {f : B → C} {g : A → B}
-  → ∀ c → fibre (f ∘ g) c ≃ (Σ[ (b , _) ∈ fibre f c ] (fibre g b))
+  → ∀ c → fibre (f ∘ g) c ≃ (Σ[ (b , _) ∈ fibre f c ] fibre g b)
 fibre-∘-≃ {f = f} {g = g} c = Iso→Equiv (fwd , iso bwd invl invr)
     where
-      fwd : fibre (f ∘ g) c → Σ[ (b , _) ∈ fibre f c ] (fibre g b)
+      fwd : fibre (f ∘ g) c → Σ[ (b , _) ∈ fibre f c ] fibre g b
       fwd (a , p) = ((g a) , p) , (a , refl)
 
-      bwd : Σ[ (b , _) ∈ fibre f c ] (fibre g b) → fibre (f ∘ g) c
+      bwd : Σ[ (b , _) ∈ fibre f c ] fibre g b → fibre (f ∘ g) c
       bwd ((b , p) , (a , q)) = a , ap f q ∙ p
 
       invl : ∀ x → fwd (bwd x) ≡ x

src/1Lab/HLevel.lagda.md

@@ -204,7 +204,7 @@ proof (used in the *definition* of path induction), we can demonstrate
 the application of path induction:
 
 ```agda
-_ : (a : A) → is-contr (Σ[ b ∈ A ] (b ≡ a))
+_ : (a : A) → is-contr (Σ[ b ∈ A ] b ≡ a)
 _ = λ t → record
   { centre = (t , refl)
   ; paths  = λ (s , p) → J' (λ s t p → (t , refl) ≡ (s , p)) (λ t → refl) p

src/1Lab/Membership.agda

@@ -45,7 +45,7 @@ infix 30 _∉_
 ∫ₚ
   : ∀ {ℓ ℓ' ℓ''} {X : Type ℓ} {ℙX : Type ℓ'} ⦃ m : Membership X ℙX ℓ'' ⦄
   → ℙX → Type _
-∫ₚ {X = X} P = Σ[ x ∈ X ] (x ∈ P)
+∫ₚ {X = X} P = Σ[ x ∈ X ] x ∈ P
 
 -- Notation typeclass for _⊆_. We could always define
 --

src/1Lab/Path.lagda.md

@@ -1044,7 +1044,7 @@ inhabitant!
 
 ```agda
 Singleton : ∀ {ℓ} {A : Type ℓ} → A → Type _
-Singleton x = Σ[ y ∈ _ ] (x ≡ y)
+Singleton x = Σ[ y ∈ _ ] x ≡ y
 ```
 
 We're given an inhabitant $y : A$ and a path $p : x \is y$. To identify
@@ -2378,5 +2378,8 @@ _$ₚ_ : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {B : A → Type ℓ₂} {f g : 
      → f ≡ g → ∀ x → f x ≡ g x
 (f $ₚ x) i = f i x
 {-# INLINE _$ₚ_ #-}
+
+_≠_ : ∀ {ℓ} {A : Type ℓ} → A → A → Type ℓ
+x ≠ y = ¬ x ≡ y
 ```
 -->

src/1Lab/Path/IdentitySystem.lagda.md

@@ -332,12 +332,7 @@ This is known as **Hedberg's theorem**.
 
 opaque
   Discrete→is-set : ∀ {ℓ} {A : Type ℓ} → Discrete A → is-set A
-  Discrete→is-set {A = A} dec =
-    identity-system→hlevel 1 (¬¬-stable-identity-system stable) λ x y f g →
-      funext λ h → absurd (g h)
-    where
-      stable : {x y : A} → ¬ ¬ x ≡ y → x ≡ y
-      stable {x = x} {y = y} ¬¬p with dec {x} {y}
-      ... | yes p = p
-      ... | no ¬p = absurd (¬¬p ¬p)
+  Discrete→is-set {A = A} dec = identity-system→hlevel 1
+    (¬¬-stable-identity-system (dec→dne ⦃ dec ⦄))
+    λ x y f g → funext λ h → absurd (g h)
 ```

src/1Lab/Resizing.lagda.md

@@ -227,9 +227,9 @@ disjunctions, and implications.
 
 <!--
 ```agda
-infixr 6 _∧Ω_
-infixr 5 _∨Ω_
-infixr 4 _→Ω_
+infixr 10 _∧Ω_
+infixr 9 _∨Ω_
+infixr 8 _→Ω_
 ```
 -->
 

src/1Lab/Type.lagda.md

@@ -49,7 +49,7 @@ absurd ()
 
 ¬_ : ∀ {ℓ} → Type ℓ → Type ℓ
 ¬ A = A → ⊥
-infix 3 ¬_
+infix 6 ¬_
 ```
 
 :::{.definition #product-type}

src/1Lab/Underlying.agda

@@ -6,6 +6,8 @@ open import 1Lab.HLevel
 open import 1Lab.Path
 open import 1Lab.Type hiding (Σ-syntax)
 
+open import Data.Bool.Base
+
 module 1Lab.Underlying where
 
 -- Notation class for types which have a chosen projection into a
@@ -54,6 +56,9 @@ instance
   Underlying-Lift ⦃ ua ⦄ .ℓ-underlying = ua .ℓ-underlying
   Underlying-Lift .⌞_⌟ x = ⌞ x .Lift.lower ⌟
 
+  Underlying-Bool : Underlying Bool
+  Underlying-Bool = record { ⌞_⌟ = So }
+
 -- The converse of to-is-true, generalised slightly. If P and Q are
 -- identical inhabitants of some type of structured types, and Q's
 -- underlying type is contractible, then P is inhabited. P's underlying

src/1Lab/Univalence.lagda.md

@@ -95,7 +95,7 @@ open import 1Lab.Equiv.FromPath
 ```agda
 Glue : (A : Type ℓ)
      → {φ : I}
-     → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] (T ≃ A)))
+     → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A))
      → Type ℓ'
 ```
 

src/Algebra/Magma.lagda.md

@@ -138,7 +138,7 @@ set, this obviously defines a magma:
 ```agda
 private
   is-magma-imp : is-magma imp
-  is-magma-imp .has-is-set = Bool-is-set
+  is-magma-imp .has-is-set = hlevel 2
 ```
 
 We show it is not commutative or associative by giving counterexamples:

src/Algebra/Ring/Solver.agda

@@ -12,7 +12,6 @@ Horner normal forms are not sparse).
 open import 1Lab.Reflection.Variables
 open import 1Lab.Reflection.Solver
 open import 1Lab.Reflection
-open import 1Lab.Rewrite
 
 open import Algebra.Ring.Cat.Initial
 open import Algebra.Ring.Commutative

src/Cat/Base.lagda.md

@@ -8,7 +8,6 @@ open import 1Lab.Extensionality
 open import 1Lab.HLevel.Closure
 open import 1Lab.Reflection
 open import 1Lab.Underlying
-open import 1Lab.Rewrite
 open import 1Lab.HLevel
 open import 1Lab.Equiv
 open import 1Lab.Path
@@ -198,10 +197,7 @@ C^op^op≡C {C = C} i = precat i where
 
 <!--
 ```agda
-private
-  precategory-double-dual : ∀ {o ℓ} {C : Precategory o ℓ} → C ^op ^op ≡rw C
-  precategory-double-dual = make-rewrite C^op^op≡C
-{-# REWRITE precategory-double-dual #-}
+{-# REWRITE C^op^op≡C #-}
 ```
 -->
 
@@ -312,12 +308,7 @@ F^op^op≡F {F = F} i .Functor.F₁ = F .Functor.F₁
 F^op^op≡F {F = F} i .Functor.F-id = F .Functor.F-id
 F^op^op≡F {F = F} i .Functor.F-∘ = F .Functor.F-∘
 
-private
-  functor-double-dual
-    : ∀ {o ℓ o' ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} {F : Functor C D}
-    → Functor.op (Functor.op F) ≡rw F
-  functor-double-dual = make-rewrite F^op^op≡F
-{-# REWRITE functor-double-dual #-}
+{-# REWRITE F^op^op≡F #-}
 ```
 -->
 

src/Cat/CartesianClosed/Instances/PSh.agda

@@ -53,7 +53,7 @@ module _ {o ℓ κ} {C : Precategory o ℓ} where
     open is-pullback
 
     pb-path
-      : ∀ {i} {x y : Σ[ x ∈ X.₀ i ] Σ[ y ∈ Y.₀ i ] (f.η i x ≡ g.η i y)}
+      : ∀ {i} {x y : Σ[ x ∈ X.₀ i ] Σ[ y ∈ Y.₀ i ] f.η i x ≡ g.η i y}
       → x .fst ≡ y .fst
       → x .snd .fst ≡ y .snd .fst
       → x ≡ y
@@ -65,7 +65,7 @@ module _ {o ℓ κ} {C : Precategory o ℓ} where
         i j
 
     pb : Pullback (PSh κ C) f g
-    pb .apex .F₀ i = el! (Σ[ x ∈ X.₀ i ] Σ[ y ∈ Y.₀ i ] (f.η i x ≡ g.η i y))
+    pb .apex .F₀ i = el! (Σ[ x ∈ X.₀ i ] Σ[ y ∈ Y.₀ i ] f.η i x ≡ g.η i y)
     pb .apex .F₁ {x} {y} h (a , b , p) = X.₁ h a , Y.₁ h b , path where abstract
       path : f.η y (X.₁ h a) ≡ g.η y (Y.₁ h b)
       path = happly (f.is-natural _ _ _) _

src/Cat/Displayed/Comprehension.lagda.md

@@ -164,7 +164,7 @@ with projections.
   _⨾ˢ_ : ∀ {Γ Δ x y} (σ : Hom Γ Δ) → Hom[ σ ] x y → Hom (Γ ⨾ x) (Δ ⨾ y)
   σ ⨾ˢ f = F₁' f .to
 
-  infixl 5 _⨾ˢ_
+  infixl 8 _⨾ˢ_
 
   sub-proj : ∀ {Γ Δ x y} {σ : Hom Γ Δ} → (f : Hom[ σ ] x y) → πᶜ ∘ (σ ⨾ˢ f) ≡ σ ∘ πᶜ
   sub-proj f = sym $ F₁' f .commute

src/Cat/Displayed/Total/Op.lagda.md

@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Rewrite
-
 open import Cat.Functor.Equivalence.Path
 open import Cat.Functor.Equivalence
 open import Cat.Displayed.Fibre
@@ -68,12 +66,7 @@ total-op-involution {ℰ = ℰ} = path where
 
 <!--
 ```agda
-private
-  displayed-double-dual
-    : ∀ {o ℓ o' ℓ'} {ℬ : Precategory o ℓ} {ℰ : Displayed ℬ o' ℓ'}
-    → ((ℰ ^total-op) ^total-op) ≡rw ℰ
-  displayed-double-dual {ℰ = ℰ} = make-rewrite (total-op-involution {ℰ = ℰ})
-  {-# REWRITE displayed-double-dual #-}
+{-# REWRITE total-op-involution #-}
 ```
 -->
 
@@ -180,12 +173,6 @@ fibre-functor-total-op-total-op {ℰ = ℰ} {y = y} {F = F} i .F-∘ f g =
     i
     where open Precategory (Fibre ℰ y)
 
-private
-  fibre-functor-double-dual
-    : ∀ {o ℓ o' ℓ'} {ℬ : Precategory o ℓ} {ℰ : Displayed ℬ o' ℓ'} {x y}
-    → {F : Functor (Fibre ℰ x) (Fibre ℰ y)}
-    → fibre-functor-total-op (fibre-functor-total-op F) ≡rw F
-  fibre-functor-double-dual = make-rewrite fibre-functor-total-op-total-op
-{-# REWRITE fibre-functor-double-dual #-}
+{-# REWRITE fibre-functor-total-op-total-op #-}
 ```
 -->

src/Cat/Instances/Comma.lagda.md

@@ -239,7 +239,7 @@ square.
 module _ {A : Precategory ao ah} {B : Precategory bo bh} where
   private module A = Precategory A
 
-  infix 5 _↙_ _↘_
+  infix 8 _↙_ _↘_
   _↙_ : A.Ob → Functor B A → Precategory _ _
   X ↙ T = !Const X ↓ T
 

src/Cat/Instances/Shape/Involution.lagda.md

@@ -24,7 +24,7 @@ composition operation.
 ∙⤮∙ : Precategory lzero lzero
 ∙⤮∙ .Precategory.Ob = ⊤
 ∙⤮∙ .Precategory.Hom _ _ = Bool
-∙⤮∙ .Precategory.Hom-set _ _ = Bool-is-set
+∙⤮∙ .Precategory.Hom-set _ _ = hlevel 2
 ∙⤮∙ .Precategory.id = false
 ∙⤮∙ .Precategory._∘_ = xor
 ∙⤮∙ .Precategory.idr f = xor-falser f

src/Cat/Instances/Shape/Parallel.lagda.md

@@ -39,9 +39,9 @@ parallel arrows between them. It is the shape of [[equaliser]] and
 
 <!--
 ```agda
-  precat .Hom-set false false a b p q i j = tt
-  precat .Hom-set false true  a b p q i j = Bool-is-set a b p q i j
-  precat .Hom-set true  true  a b p q i j = tt
+  precat .Hom-set false false = hlevel 2
+  precat .Hom-set false true  = hlevel 2
+  precat .Hom-set true  true  = hlevel 2
 
   precat .id {false} = tt
   precat .id {true} = tt

src/Cat/Instances/Shape/Two.lagda.md

@@ -66,11 +66,11 @@ defined above.
 
     q : ∀ {x y} (f : x ≡ y) → _
     q {false} {false} p =
-      F .F₁ p           ≡⟨ ap (F .F₁) (Bool-is-set _ _ _ _) ⟩
+      F .F₁ p           ≡⟨ ap (F .F₁) prop! ⟩
       F .F₁ refl        ≡⟨ F .F-id ⟩
       id                ∎
     q {true} {true} p =
-      F .F₁ p           ≡⟨ ap (F .F₁) (Bool-is-set _ _ _ _) ⟩
+      F .F₁ p           ≡⟨ ap (F .F₁) prop! ⟩
       F .F₁ refl        ≡⟨ F .F-id ⟩
       id                ∎
     q {false} {true} p = absurd (true≠false (sym p))

src/Cat/Instances/StrictCat/Cohesive.lagda.md

@@ -337,7 +337,7 @@ category are product sets of connected components.
 
 ```agda
 Π₀-preserve-prods
-  : ∀ {C D : Precategory o h} → π₀ ʻ (C ×ᶜ D) ≡ π₀ ʻ C × π₀ ʻ D
+  : ∀ {C D : Precategory o h} → π₀ ʻ (C ×ᶜ D) ≡ (π₀ ʻ C × π₀ ʻ D)
 Π₀-preserve-prods {C = C} {D = D} = Iso→Path (f , isom) where
   open is-iso
 ```

src/Cat/Internal/Opposite.lagda.md

@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Rewrite
-
 open import Cat.Prelude
 
 import Cat.Internal.Base
@@ -51,8 +49,8 @@ private
   op-ihom-involutive
     : ∀ {C₀ C₁ Γ} {src tgt : Hom C₁ C₀} {x y : Hom Γ C₀}
     → {f : Internal-hom src tgt x y}
-    → op-ihom (op-ihom f) ≡rw f
-  op-ihom-involutive = make-rewrite (Internal-hom-path refl)
+    → op-ihom (op-ihom f) ≡ f
+  op-ihom-involutive = Internal-hom-path refl
 {-# REWRITE op-ihom-involutive #-}
 ```
 -->

src/Cat/Monoidal/Instances/Day.lagda.md

@@ -1,7 +1,5 @@
 <!--
 ```agda
-open import 1Lab.Rewrite
-
 open import Cat.Diagram.Coend.Sets
 open import Cat.Functor.Naturality
 open import Cat.Instances.Product
@@ -283,8 +281,8 @@ $f(\day{h,x,y})$, in a way compatible with the relation above.
 ```agda
     factor-day
       : ∀ {i a b} {W : Cowedge (Day-diagram i)} {h : Hom i (a ⊗ b)} {x : X ʻ a} {y : Y ʻ b}
-      → factor W (day h x y) ≡rw W .ψ (a , b) (h , x , y)
-    factor-day = idrw
+      → factor W (day h x y) ≡ W .ψ (a , b) (h , x , y)
+    factor-day = refl
 
   {-# REWRITE factor-day #-}