Poset Refactor

src/1Lab/HLevel.lagda.md

@@ -298,6 +298,14 @@ is-prop→is-hlevel-suc {n = suc n} aprop =
   is-hlevel-suc (suc n) (is-prop→is-hlevel-suc aprop)
 ```
 
+<!--
+```agda
+is-set→is-hlevel+2
+  : ∀ {ℓ} {A : Type ℓ} {n : Nat} → is-set A → is-hlevel A (2 + n)
+is-set→is-hlevel+2 aset x y = is-prop→is-hlevel-suc (aset x y)
+```
+-->
+
 Furthermore, by the upwards closure of h-levels, we have that if $A$ is
 an n-type, then paths in $A$ are also $n$-types. This is because, by
 definition, the paths in a $n$-type are "$(n-1)$-types", which

src/1Lab/Reflection/HLevel.agda

@@ -1,5 +1,6 @@
 {-# OPTIONS -vtactic.hlevel:20 -vtc.def:10 #-}
 open import 1Lab.Reflection.Record
+open import 1Lab.Equiv.Embedding
 open import 1Lab.HLevel.Retracts
 open import 1Lab.HLevel.Universe
 open import 1Lab.Reflection
@@ -651,6 +652,14 @@ prop!
 prop! {A = A} {aip = aip} {x} {y} =
   is-prop→pathp (λ i → coe0→i (λ j → is-prop (A j)) i aip) x y
 
+injective→is-embedding!
+  : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
+      {@(tactic hlevel-tactic-worker) bset : is-set B}
+  → ∀ {f : A → B}
+  → injective f
+  → is-embedding f
+injective→is-embedding! {bset = bset} {f} inj = injective→is-embedding bset f inj
+
 open hlevel-projection
 
 -- Hint database bootstrap

src/1Lab/Underlying.agda

@@ -98,13 +98,21 @@ apply
   → ∀ {a b} → F a b → ⌞ a ⌟ → ⌞ b ⌟
 apply = _#_
 
+-- Shortcut for ap (apply ...)
+ap#
+  : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {F : A → B → Type ℓ''}
+  → ⦃ _ : Funlike F ⦄
+  → ∀ {a : A} {b : B} (f : F a b) → ∀ {x y : ⌞ a ⌟} → x ≡ y → f # x ≡ f # y
+ap# f = ap (apply f)
+
 -- Generalised happly.
 _#ₚ_
   : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {F : A → B → Type ℓ''}
   → ⦃ _ : Funlike F ⦄
   → {a : A} {b : B} {f g : F a b} → f ≡ g → ∀ (x : ⌞ a ⌟) → f # x ≡ g # x
 f #ₚ x = ap₂ _#_ f refl
 
+
 instance
   -- Agda really dislikes inferring the level parameters here.
   Funlike-Fun

src/Cat/Displayed/Doctrine.lagda.md

@@ -242,21 +242,16 @@ the Beck-Chevalley condition.
 <!--
 ```agda
   ≤-Poset : ∀ {x : Ob} → Poset o' ℓ'
-  ∣ ≤-Poset {x = x} .fst ∣    = ℙ.Ob[ x ]
-  ≤-Poset {x = x} .fst .is-tr = has-is-set _
-
-  ≤-Poset {x = x} .snd .Poset-on._≤_ = ℙ.Hom[ id ]
-  ≤-Poset {x = x} .snd .Poset-on.has-is-poset = po where
-    open is-partial-order
-    po : is-partial-order ℙ.Hom[ id ]
-    po .≤-thin    = has-is-thin _ _
-    po .≤-refl    = ℙ.id'
-    po .≤-trans α β = Precategory._∘_ (Fibre ℙ _) β α
-    po .≤-antisym α β = has-univalence _ .to-path $
+  ≤-Poset {x = x} .Poset.Ob = ℙ.Ob[ x ]
+  ≤-Poset {x = x} .Poset._≤_ = ℙ.Hom[ id ]
+  ≤-Poset {x = x} .Poset.≤-thin = has-is-thin _ _
+  ≤-Poset {x = x} .Poset.≤-refl = ℙ.id'
+  ≤-Poset {x = x} .Poset.≤-trans α β = Precategory._∘_ (Fibre ℙ _) β α
+  ≤-Poset {x = x} .Poset.≤-antisym α β = has-univalence _ .to-path $
       Cat.make-iso (Fibre ℙ _) α β (has-is-thin _ _ _ _) (has-is-thin _ _ _ _)
 
   module _ {x} where
-    open Order.Reasoning (≤-Poset {x}) hiding (has-is-set ; Ob) public
+    open Order.Reasoning (≤-Poset {x}) hiding (Ob-is-set ; Ob) public
   open Disp ℙ public
   subst-∘ : ∀ {x y z} (f : Hom y z) (g : Hom x y) {α} → (α [ f ]) [ g ] ≡ α [ f ∘ g ]
   subst-∘ f g = ≤-antisym

src/Cat/Instances/Sets.lagda.md

@@ -40,7 +40,8 @@ only difference between these types can be patched by
 
 ```agda
   iso→equiv : {A B : Set ℓ} → A Sets.≅ B → ∣ A ∣ ≃ ∣ B ∣
-  iso→equiv x = Iso→Equiv (x.to , iso x.from (happly x.invl) (happly x.invr))
+  iso→equiv x .fst = x .Sets.to
+  iso→equiv x .snd = is-iso→is-equiv $ iso x.from (happly x.invl) (happly x.invr)
     where module x = Sets._≅_ x
 ```
 

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

@@ -43,7 +43,7 @@ ordering on them, with $\bot \le \top$.
 open Precategory
 
 Bool-poset : Poset lzero lzero
-Bool-poset = to-poset Bool make-bool where
+Bool-poset = po where
   R : Bool → Bool → Type
   R false false = ⊤
   R false true  = ⊤
@@ -86,12 +86,13 @@ the poset of booleans:
   Rprop {true}  {false} () ()
   Rprop {true}  {true}  tt tt = refl
 
-  make-bool : make-poset lzero Bool
-  make-bool .make-poset.rel = R
-  make-bool .make-poset.id = Rrefl
-  make-bool .make-poset.thin = Rprop
-  make-bool .make-poset.trans = Rtrans
-  make-bool .make-poset.antisym = Rantisym
+  po : Poset _ _
+  po .Poset.Ob = Bool
+  po .Poset._≤_ = R
+  po .Poset.≤-thin = Rprop
+  po .Poset.≤-refl = Rrefl
+  po .Poset.≤-trans = Rtrans
+  po .Poset.≤-antisym = Rantisym
 ```
 -->
 

src/Data/Nat/Divisible.lagda.md

@@ -12,7 +12,7 @@ open import Data.Nat.Base
 module Data.Nat.Divisible where
 ```
 
-# Divisibility
+# Divisibility {defines="divisibility"}
 
 In the natural numbers, **divisibility**[^divide] is the property
 expressing that a given number can be expressed as a multiple of

src/Data/Nat/Divisible/GCD.lagda.md

@@ -17,7 +17,7 @@ open import Data.Sum.Base
 module Data.Nat.Divisible.GCD where
 ```
 
-# Greatest common divisors
+# Greatest common divisors {defines="greatest-common-divisor gcd"}
 
 The **greatest common divisor** $\gcd(a,b)$ of a pair of natural numbers
 is the largest number which [divides] them both. The definition we use

src/Data/Set/Coequaliser.lagda.md

@@ -270,7 +270,7 @@ instance
 ```
 -->
 
-# Quotients
+# Quotients {defines=quotient}
 
 With dependent sums, we can recover quotients as a special case of
 coequalisers. Observe that, by taking the total space of a relation $R :