wip: start lattice refactor

the1lab · Nov 29, 2023 · fdcb5cc · fdcb5cc
1 parent 3575285
commit fdcb5cc
Show file tree

Hide file tree

Showing 5 changed files with 629 additions and 467 deletions.
diff --git a/src/Order/Diagram/Glb.lagda.md b/src/Order/Diagram/Glb.lagda.md
@@ -234,6 +234,9 @@ record Top : Type (o ⊔ ℓ) where
     top : Ob
     has-top : is-top top
 
+  ! : ∀ {x} → x ≤ top
+  ! = has-top _
+
 is-top→is-glb : ∀ {glb} {f : ⊥ → _} → is-top glb → is-glb f glb
 is-top→is-glb is-top .greatest x _ = is-top x