more naming

UniMath · Oct 19, 2024 · 4b8cc04 · 4b8cc04
1 parent 3658f69
commit 4b8cc04
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 15 deletions.
diff --git a/src/order-theory/chains-preorders.lagda.md b/src/order-theory/chains-preorders.lagda.md
@@ -73,7 +73,7 @@ module _
 
   inclusion-prop-chain-Preorder : Prop (l1 ⊔ l3 ⊔ l4)
   inclusion-prop-chain-Preorder =
-    inclusion-Subpreorder-Prop X
+    inclusion-prop-Subpreorder X
       ( subpreorder-chain-Preorder X C)
       ( subpreorder-chain-Preorder X D)
 

diff --git a/src/order-theory/subposets.lagda.md b/src/order-theory/subposets.lagda.md
@@ -76,7 +76,7 @@ module _
   pr2 poset-Subposet = antisymmetric-leq-Subposet
 ```
 
-### Inclusion of sub-posets
+### Inclusion of subposets
 
 ```agda
 module _
@@ -87,9 +87,9 @@ module _
     {l3 l4 : Level} (S : Subposet l3 X) (T : Subposet l4 X)
     where
 
-    inclusion-Subposet-Prop : Prop (l1 ⊔ l3 ⊔ l4)
-    inclusion-Subposet-Prop =
-      inclusion-Subpreorder-Prop (preorder-Poset X) S T
+    inclusion-prop-Subposet : Prop (l1 ⊔ l3 ⊔ l4)
+    inclusion-prop-Subposet =
+      inclusion-prop-Subpreorder (preorder-Poset X) S T
 
     inclusion-Subposet : UU (l1 ⊔ l3 ⊔ l4)
     inclusion-Subposet = inclusion-Subpreorder (preorder-Poset X) S T
@@ -111,9 +111,9 @@ module _
   transitive-inclusion-Subposet =
     transitive-inclusion-Subpreorder (preorder-Poset X)
 
-  sub-poset-Preorder : (l : Level) → Preorder (l1 ⊔ lsuc l) (l1 ⊔ l)
-  pr1 (sub-poset-Preorder l) = type-Poset X → Prop l
-  pr1 (pr2 (sub-poset-Preorder l)) = inclusion-Subposet-Prop
-  pr1 (pr2 (pr2 (sub-poset-Preorder l))) = refl-inclusion-Subposet
-  pr2 (pr2 (pr2 (sub-poset-Preorder l))) = transitive-inclusion-Subposet
+  subposet-Preorder : (l : Level) → Preorder (l1 ⊔ lsuc l) (l1 ⊔ l)
+  pr1 (subposet-Preorder l) = Subposet l X
+  pr1 (pr2 (subposet-Preorder l)) = inclusion-prop-Subposet
+  pr1 (pr2 (pr2 (subposet-Preorder l))) = refl-inclusion-Subposet
+  pr2 (pr2 (pr2 (subposet-Preorder l))) = transitive-inclusion-Subposet
 ```
diff --git a/src/order-theory/subpreorders.lagda.md b/src/order-theory/subpreorders.lagda.md
@@ -82,16 +82,16 @@ module _
     (T : type-Preorder P → Prop l4)
     where
 
-    inclusion-Subpreorder-Prop : Prop (l1 ⊔ l3 ⊔ l4)
-    inclusion-Subpreorder-Prop =
+    inclusion-prop-Subpreorder : Prop (l1 ⊔ l3 ⊔ l4)
+    inclusion-prop-Subpreorder =
       Π-Prop (type-Preorder P) (λ x → hom-Prop (S x) (T x))
 
     inclusion-Subpreorder : UU (l1 ⊔ l3 ⊔ l4)
-    inclusion-Subpreorder = type-Prop inclusion-Subpreorder-Prop
+    inclusion-Subpreorder = type-Prop inclusion-prop-Subpreorder
 
     is-prop-inclusion-Subpreorder : is-prop inclusion-Subpreorder
     is-prop-inclusion-Subpreorder =
-      is-prop-type-Prop inclusion-Subpreorder-Prop
+      is-prop-type-Prop inclusion-prop-Subpreorder
 
   refl-inclusion-Subpreorder :
     {l3 : Level} → is-reflexive (inclusion-Subpreorder {l3})
@@ -108,7 +108,7 @@ module _
 
   Sub-Preorder : (l : Level) → Preorder (l1 ⊔ lsuc l) (l1 ⊔ l)
   pr1 (Sub-Preorder l) = type-Preorder P → Prop l
-  pr1 (pr2 (Sub-Preorder l)) = inclusion-Subpreorder-Prop
+  pr1 (pr2 (Sub-Preorder l)) = inclusion-prop-Subpreorder
   pr1 (pr2 (pr2 (Sub-Preorder l))) = refl-inclusion-Subpreorder
   pr2 (pr2 (pr2 (Sub-Preorder l))) = transitive-inclusion-Subpreorder
 ```