From 8026cd60594f4d41241bd1708b7feaea2267d708 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Wed, 29 Nov 2023 09:41:11 -0300
Subject: [PATCH] chore: automation-related cleanup

---
 src/Order/Base.lagda.md      |  73 +++++++++++-------------
 src/Order/Univalent.lagda.md | 106 ++++++++++++++++-------------------
 2 files changed, 81 insertions(+), 98 deletions(-)

diff --git a/src/Order/Base.lagda.md b/src/Order/Base.lagda.md
index 7907c6e14..05851f4b6 100644
--- a/src/Order/Base.lagda.md
+++ b/src/Order/Base.lagda.md
@@ -79,31 +79,32 @@ instance
   Underlying-Poset .Underlying.ℓ-underlying = _
   Underlying-Poset .Underlying.⌞_⌟ = Poset.Ob
 
-instance
+  open hlevel-projection
+
   Poset-ob-hlevel-proj : hlevel-projection (quote Poset.Ob)
-  Poset-ob-hlevel-proj .hlevel-projection.has-level = quote Poset.Ob-is-set
-  Poset-ob-hlevel-proj .hlevel-projection.get-level _ = pure (lit (nat 2))
-  Poset-ob-hlevel-proj .hlevel-projection.get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
-  Poset-ob-hlevel-proj .hlevel-projection.get-argument _ = typeError []
+  Poset-ob-hlevel-proj .has-level   = quote Poset.Ob-is-set
+  Poset-ob-hlevel-proj .get-level _ = pure (lit (nat 2))
+  Poset-ob-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
+  Poset-ob-hlevel-proj .get-argument _                     = typeError []
 
   Poset-≤-hlevel-proj : hlevel-projection (quote Poset._≤_)
-  Poset-≤-hlevel-proj .hlevel-projection.has-level = quote Poset.≤-thin
-  Poset-≤-hlevel-proj .hlevel-projection.get-level _ = pure (lit (nat 1))
-  Poset-≤-hlevel-proj .hlevel-projection.get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
-  Poset-≤-hlevel-proj .hlevel-projection.get-argument _ = typeError []
+  Poset-≤-hlevel-proj .has-level   = quote Poset.≤-thin
+  Poset-≤-hlevel-proj .get-level _ = pure (lit (nat 1))
+  Poset-≤-hlevel-proj .get-argument (_ ∷ _ ∷ arg _ t ∷ _) = pure t
+  Poset-≤-hlevel-proj .get-argument _                     = typeError []
 ```
 -->
 
 ```agda
-record Monotone
-  {o o' ℓ ℓ'}
-  (P : Poset o ℓ) (Q : Poset o' ℓ')
-  : Type (o ⊔ o' ⊔ ℓ ⊔ ℓ')
-  where
+record
+  Monotone {o o' ℓ ℓ'} (P : Poset o ℓ) (Q : Poset o' ℓ')
+    : Type (o ⊔ o' ⊔ ℓ ⊔ ℓ') where
   no-eta-equality
+
   private
     module P = Poset P
     module Q = Poset Q
+
   field
     hom : P.Ob → Q.Ob
     pres-≤ : ∀ {x y} → x P.≤ y → hom x Q.≤ hom y
@@ -120,25 +121,15 @@ private
 
 Monotone-is-hlevel : ∀ n → is-hlevel (Monotone P Q) (2 + n)
 Monotone-is-hlevel {Q = Q} n =
-  Iso→is-hlevel (2 + n) eqv $
-  Σ-is-hlevel (2 + n) (Π-is-hlevel (2 + n) λ _ → is-set→is-hlevel+2 Q.Ob-is-set) λ _ →
-  Π-is-hlevel' (2 + n) λ _ → Π-is-hlevel' (2 + n) λ _ → Π-is-hlevel (2 + n) λ _ →
-  is-prop→is-hlevel-suc {n = suc n} Q.≤-thin
-  where
-    unquoteDecl eqv = declare-record-iso eqv (quote Monotone)
-    module Q = Poset Q
+  Iso→is-hlevel (2 + n) eqv $ is-set→is-hlevel+2 $ hlevel!
+  where unquoteDecl eqv = declare-record-iso eqv (quote Monotone)
 
 instance
-  H-Level-Monotone
-    : ∀ {n}
-    → H-Level (Monotone P Q) (2 + n)
+  H-Level-Monotone : ∀ {n} → H-Level (Monotone P Q) (2 + n)
   H-Level-Monotone = basic-instance 2 (Monotone-is-hlevel 0)
 
-instance
   Funlike-Monotone : ∀ {o o' ℓ ℓ'} → Funlike (Monotone {o} {o'} {ℓ} {ℓ'})
-  Funlike-Monotone .Funlike.au = Underlying-Poset
-  Funlike-Monotone .Funlike.bu = Underlying-Poset
-  Funlike-Monotone .Funlike._#_ = hom
+  Funlike-Monotone = record { _#_ = hom }
 
 Monotone-pathp
   : ∀ {o ℓ o' ℓ'} {P : I → Poset o ℓ} {Q : I → Poset o' ℓ'}
@@ -151,17 +142,17 @@ Monotone-pathp {P = P} {Q} {f} {g} q i .Monotone.pres-≤ {x} {y} α =
     (λ i → Π-is-hlevel³ {A = ⌞ P i ⌟} {B = λ _ → ⌞ P i ⌟} {C = λ x y → P i .Poset._≤_ x y} 1
       λ x y _ → Q i .Poset.≤-thin {q i x} {q i y})
     (λ _ _ α → f .Monotone.pres-≤ α)
-    (λ _ _ α → g .Monotone.pres-≤ α) i x y α      
+    (λ _ _ α → g .Monotone.pres-≤ α) i x y α
 
 Extensional-Monotone
   : ∀ {o ℓ o' ℓ' ℓr} {P : Poset o ℓ} {Q : Poset o' ℓ'}
-  → ⦃ sq : Extensional (⌞ Q ⌟) ℓr ⦄
-  → Extensional (Monotone P Q) (o ⊔ ℓr)
+  → ⦃ sa : Extensional (⌞ P ⌟ → ⌞ Q ⌟) ℓr ⦄
+  → Extensional (Monotone P Q) ℓr
 Extensional-Monotone {Q = Q} ⦃ sq ⦄ =
-  injection→extensional! Monotone-pathp (Extensional-→ ⦃ sq ⦄)
+  injection→extensional! Monotone-pathp sq
 
 instance
-  Extensionality-Monotone 
+  Extensionality-Monotone
     : ∀ {o ℓ o' ℓ'} {P : Poset o ℓ} {Q : Poset o' ℓ'}
     → Extensionality (Monotone P Q)
   Extensionality-Monotone = record { lemma = quote Extensional-Monotone }
@@ -170,21 +161,23 @@ instance
 
 ```agda
 idₘ : Monotone P P
-idₘ .hom x = x
+idₘ .hom    x   = x
 idₘ .pres-≤ x≤y = x≤y
 
 _∘ₘ_ : Monotone Q R → Monotone P Q → Monotone P R
-(f ∘ₘ g) .hom x = f # (g # x)
+(f ∘ₘ g) .hom    x   = f # (g # x)
 (f ∘ₘ g) .pres-≤ x≤y = f .pres-≤ (g .pres-≤ x≤y)
 
 Posets : ∀ (o ℓ : Level) → Precategory (lsuc o ⊔ lsuc ℓ) (o ⊔ ℓ)
-Posets o ℓ .Precategory.Ob = Poset o ℓ
-Posets o ℓ .Precategory.Hom = Monotone
+Posets o ℓ .Precategory.Ob      = Poset o ℓ
+Posets o ℓ .Precategory.Hom     = Monotone
 Posets o ℓ .Precategory.Hom-set = hlevel!
-Posets o ℓ .Precategory.id = idₘ
+
+Posets o ℓ .Precategory.id  = idₘ
 Posets o ℓ .Precategory._∘_ = _∘ₘ_
-Posets o ℓ .Precategory.idr f = trivial!
-Posets o ℓ .Precategory.idl f = trivial!
+
+Posets o ℓ .Precategory.idr f       = trivial!
+Posets o ℓ .Precategory.idl f       = trivial!
 Posets o ℓ .Precategory.assoc f g h = trivial!
 ```
 
diff --git a/src/Order/Univalent.lagda.md b/src/Order/Univalent.lagda.md
index 2fa18e1c0..9d1d2a54c 100644
--- a/src/Order/Univalent.lagda.md
+++ b/src/Order/Univalent.lagda.md
@@ -17,71 +17,61 @@ module Order.Univalent where
 
 # The Category of Posets is Univalent
 
-<!--
-```agda
-module _ {o ℓ} {P Q : Poset o ℓ} where
-  private
-    module P = Poset P
-    module Q = Poset Q
-```
--->
-
 ```agda
-  Poset-path : P Posets.≅ Q → P ≡ Q
-  Poset-path f = path
-    where
-      open Posets
-
-      P≃Q : ⌞ P ⌟ ≃ ⌞ Q ⌟ 
-      P≃Q = iso→equiv (F-map-iso Forget-poset f)
+Poset-path : ∀ {o ℓ} {P Q : Poset o ℓ} → P Posets.≅ Q → P ≡ Q
+Poset-path {P = P} {Q} f = path where
+  module P = Poset P
+  module Q = Poset Q
+  open Posets
 
-      ob : ∀ i → Type o
-      ob i = ua P≃Q i
+  P≃Q : ⌞ P ⌟ ≃ ⌞ Q ⌟
+  P≃Q = iso→equiv (F-map-iso Forget-poset f)
 
-      sys : ∀ i (x y : ob i) → Partial (i ∨ ~ i) _
-      sys i x y (i = i0) = (x P.≤ y) , iso→≤-equiv f
-      sys i x y (i = i1) = (x Q.≤ y) , (λ x → x) , id-equiv
+  ob : ∀ i → Type _
+  ob i = ua P≃Q i
 
-      order : PathP (λ i → ob i → ob i → Type ℓ) P._≤_ Q._≤_
-      order i x y = Glue ((unglue (i ∨ ~ i) x) Q.≤ (unglue (i ∨ ~ i) y)) (sys i x y)
+  order : PathP (λ i → ob i → ob i → Type _) P._≤_ Q._≤_
+  order i x y = Glue (unglue (∂ i) x Q.≤ unglue (∂ i) y) λ where
+    (i = i0) → x P.≤ y , iso→≤-equiv f
+    (i = i1) → x Q.≤ y , _ , id-equiv
 
-      order-thin : ∀ i x y → is-prop (order i x y)
-      order-thin i = coe0→i (λ i → (x y : ob i) → is-prop (order i x y)) i hlevel!
+  order-thin : ∀ i x y → is-prop (order i x y)
+  order-thin i = coe0→i (λ i → (x y : ob i) → is-prop (order i x y)) i hlevel!
 
-      ob-set : ∀ i → is-set (ob i)
-      ob-set i = coe0→i (λ i → is-set (ob i)) i hlevel!
+  ob-set : ∀ i → is-set (ob i)
+  ob-set i = coe0→i (λ i → is-set (ob i)) i hlevel!
 
-      path : P ≡ Q
-      path i .Poset.Ob = ob i
-      path i .Poset._≤_ x y = order i x y
-      path i .Poset.≤-thin {x} {y} =
-        is-prop→pathp
-          (λ i →
-            Π-is-hlevel² {A = ob i} {B = λ _ → ob i} 1 λ x y →
-            is-prop-is-prop {A = order i x y})
-          (λ _ _ → P.≤-thin)
-          (λ _ _ → Q.≤-thin) i x y
-      path i .Poset.≤-refl {x = x} =
-        is-prop→pathp
-          (λ i → Π-is-hlevel {A = ob i} 1 λ x → order-thin i x x)
-            (λ _ → P.≤-refl)
-            (λ _ → Q.≤-refl) i x
-      path i .Poset.≤-trans {x} {y} {z} x≤y y≤z =
-        is-prop→pathp
-          (λ i →
-            Π-is-hlevel³ {A = ob i} {B = λ _ → ob i} {C = λ _ _ → ob i} 1 λ x y z →
-            Π-is-hlevel² {A = order i x y} {B = λ _ → order i y z} 1 λ _ _ →
-            order-thin i x z)
-          (λ _ _ _ → P.≤-trans)
-          (λ _ _ _ → Q.≤-trans) i x y z x≤y y≤z
-      path i .Poset.≤-antisym {x} {y} x≤y y≤x =
-        is-prop→pathp
-          (λ i →
-            Π-is-hlevel² {A = ob i } {B = λ _ → ob i} 1 λ x y →
-            Π-is-hlevel² {A = order i x y} {B = λ _ → order i y x} 1 λ _ _ →
-            ob-set i x y)
-          (λ _ _ → P.≤-antisym)
-          (λ _ _ → Q.≤-antisym) i x y x≤y y≤x
+  path : P ≡ Q
+  path i .Poset.Ob      = ob i
+  path i .Poset._≤_ x y = order i x y
+  path i .Poset.≤-thin {x} {y} =
+    is-prop→pathp
+      (λ i →
+        Π-is-hlevel² {A = ob i} {B = λ _ → ob i} 1 λ x y →
+        is-prop-is-prop {A = order i x y})
+      (λ _ _ → P.≤-thin)
+      (λ _ _ → Q.≤-thin) i x y
+  path i .Poset.≤-refl {x = x} =
+    is-prop→pathp
+      (λ i → Π-is-hlevel {A = ob i} 1 λ x → order-thin i x x)
+        (λ _ → P.≤-refl)
+        (λ _ → Q.≤-refl) i x
+  path i .Poset.≤-trans {x} {y} {z} x≤y y≤z =
+    is-prop→pathp
+      (λ i →
+        Π-is-hlevel³ {A = ob i} {B = λ _ → ob i} {C = λ _ _ → ob i} 1 λ x y z →
+        Π-is-hlevel² {A = order i x y} {B = λ _ → order i y z} 1 λ _ _ →
+        order-thin i x z)
+      (λ _ _ _ → P.≤-trans)
+      (λ _ _ _ → Q.≤-trans) i x y z x≤y y≤z
+  path i .Poset.≤-antisym {x} {y} x≤y y≤x =
+    is-prop→pathp
+      (λ i →
+        Π-is-hlevel² {A = ob i } {B = λ _ → ob i} 1 λ x y →
+        Π-is-hlevel² {A = order i x y} {B = λ _ → order i y x} 1 λ _ _ →
+        ob-set i x y)
+      (λ _ _ → P.≤-antisym)
+      (λ _ _ → Q.≤-antisym) i x y x≤y y≤x
 ```
 
 ```agda