We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent bad2ee9 commit 1841d6eCopy full SHA for 1841d6e
src/Relation/Binary/Domain.agda
@@ -1,7 +1,7 @@
1
------------------------------------------------------------------------
2
-- The Agda standard library
3
--
4
--- Order-theoretic Domains
+-- Domain theory
5
6
7
{-# OPTIONS --cubical-compatible --safe #-}
src/Relation/Binary/Domain/Structures.agda
@@ -63,4 +63,4 @@ module _ {c ℓ₁ ℓ₂ : Level} {P : Poset c ℓ₁ ℓ₂} {Q : Poset c ℓ
63
→ (lub : P.Carrier)
64
→ IsLub P s lub
65
→ IsLub Q (f ∘ s) (f lub)
66
- PreserveEquality : ∀ {x y} → x P.≈ y → f x Q.≈ f y
+ cong : ∀ {x y} → x P.≈ y → f x Q.≈ f y
0 commit comments