simplicial type theory

src/order-theory/bounded-total-orders.lagda.md

@@ -0,0 +1,124 @@
+# Bounded total orders
+
+```agda
+module order-theory.bounded-total-orders where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.propositions
+open import foundation.universe-levels
+
+open import order-theory.bottom-elements-posets
+open import order-theory.posets
+open import order-theory.top-elements-posets
+open import order-theory.total-orders
+```
+
+</details>
+
+## Idea
+
+A bounded total order is a [total order](order-theory.total-orders.md) equipped with a top and bottom element.
+
+## Definitions
+
+### The predicate of being a bounded total order
+
+```agda
+module _
+  {l1 l2 : Level} (L : Total-Order l1 l2)
+  where
+
+  is-bounded-Total-Order : UU (l1 ⊔ l2)
+  is-bounded-Total-Order =
+    has-top-element-Poset (poset-Total-Order L) ×
+    has-bottom-element-Poset (poset-Total-Order L)
+```
+
+### Bounded total orders
+
+```agda
+Bounded-Total-Order : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
+Bounded-Total-Order l1 l2 =
+  Σ (Total-Order l1 l2) is-bounded-Total-Order
+
+module _
+  {l1 l2 : Level} (L : Bounded-Total-Order l1 l2)
+  where
+
+  total-order-Bounded-Total-Order : Total-Order l1 l2
+  total-order-Bounded-Total-Order = pr1 L
+
+  poset-Bounded-Total-Order : Poset l1 l2
+  poset-Bounded-Total-Order =
+    poset-Total-Order total-order-Bounded-Total-Order
+
+  type-Bounded-Total-Order : UU l1
+  type-Bounded-Total-Order =
+    type-Total-Order total-order-Bounded-Total-Order
+
+  leq-prop-Bounded-Total-Order :
+    (x y : type-Bounded-Total-Order) → Prop l2
+  leq-prop-Bounded-Total-Order =
+    leq-prop-Poset poset-Bounded-Total-Order
+
+  leq-Bounded-Total-Order :
+    (x y : type-Bounded-Total-Order) → UU l2
+  leq-Bounded-Total-Order =
+    leq-Poset poset-Bounded-Total-Order
+
+  is-prop-leq-Bounded-Total-Order :
+    (x y : type-Bounded-Total-Order) → is-prop (leq-Bounded-Total-Order x y)
+  is-prop-leq-Bounded-Total-Order =
+    is-prop-leq-Poset poset-Bounded-Total-Order
+
+  refl-leq-Bounded-Total-Order :
+    is-reflexive leq-Bounded-Total-Order
+  refl-leq-Bounded-Total-Order =
+    refl-leq-Poset poset-Bounded-Total-Order
+
+  transitive-leq-Bounded-Total-Order :
+    is-transitive leq-Bounded-Total-Order
+  transitive-leq-Bounded-Total-Order =
+    transitive-leq-Poset poset-Bounded-Total-Order
+
+  antisymmetric-leq-Bounded-Total-Order :
+    is-antisymmetric leq-Bounded-Total-Order
+  antisymmetric-leq-Bounded-Total-Order =
+    antisymmetric-leq-Poset poset-Bounded-Total-Order
+
+  has-top-element-Bounded-Total-Order :
+    has-top-element-Poset poset-Bounded-Total-Order
+  has-top-element-Bounded-Total-Order =
+    pr1 (pr2 L)
+
+  top-Bounded-Total-Order :
+    type-Bounded-Total-Order
+  top-Bounded-Total-Order =
+    pr1 has-top-element-Bounded-Total-Order
+
+  is-top-element-top-Bounded-Total-Order :
+    is-top-element-Poset poset-Bounded-Total-Order top-Bounded-Total-Order
+  is-top-element-top-Bounded-Total-Order =
+    pr2 has-top-element-Bounded-Total-Order
+
+  has-bottom-element-Bounded-Total-Order :
+    has-bottom-element-Poset poset-Bounded-Total-Order
+  has-bottom-element-Bounded-Total-Order =
+    pr2 (pr2 L)
+
+  bottom-Bounded-Total-Order :
+    type-Bounded-Total-Order
+  bottom-Bounded-Total-Order =
+    pr1 has-bottom-element-Bounded-Total-Order
+
+  is-bottom-element-bottom-Bounded-Total-Order :
+    is-bottom-element-Poset poset-Bounded-Total-Order bottom-Bounded-Total-Order
+  is-bottom-element-bottom-Bounded-Total-Order =
+    pr2 has-bottom-element-Bounded-Total-Order
+```

src/order-theory/order-preserving-maps-posets.lagda.md

@@ -7,6 +7,8 @@ module order-theory.order-preserving-maps-posets where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.binary-relations
+open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.function-types
 open import foundation.identity-types
@@ -19,6 +21,7 @@ open import foundation.universe-levels
 
 open import order-theory.order-preserving-maps-preorders
 open import order-theory.posets
+open import order-theory.preorders
 ```
 
 </details>
@@ -209,3 +212,47 @@ module _
       ( preorder-Poset R)
       ( preorder-Poset S)
 ```
+
+### Pointwise inequality of order preserving maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (P : Poset l1 l2) (Q : Poset l3 l4)
+  where
+
+  leq-hom-Poset : (f g : hom-Poset P Q) → UU (l1 ⊔ l4)
+  leq-hom-Poset =
+    leq-hom-Preorder (preorder-Poset P) (preorder-Poset Q)
+
+  is-prop-leq-hom-Poset :
+    (f g : hom-Poset P Q) → is-prop (leq-hom-Poset f g)
+  is-prop-leq-hom-Poset =
+    is-prop-leq-hom-Preorder (preorder-Poset P) (preorder-Poset Q)
+
+  leq-prop-hom-Poset :
+    (f g : hom-Poset P Q) → Prop (l1 ⊔ l4)
+  leq-prop-hom-Poset =
+    leq-prop-hom-Preorder (preorder-Poset P) (preorder-Poset Q)
+
+  refl-leq-hom-Poset : is-reflexive leq-hom-Poset
+  refl-leq-hom-Poset =
+    refl-leq-hom-Preorder (preorder-Poset P) (preorder-Poset Q)
+
+  transitive-leq-hom-Poset :
+    is-transitive leq-hom-Poset
+  transitive-leq-hom-Poset =
+    transitive-leq-hom-Preorder (preorder-Poset P) (preorder-Poset Q)
+
+  antisymmetric-leq-hom-Poset :
+    is-antisymmetric leq-hom-Poset
+  antisymmetric-leq-hom-Poset f g H K =
+    eq-htpy-hom-Poset P Q f g (λ x → antisymmetric-leq-Poset Q _ _ (H x) (K x))
+
+  hom-preorder-Poset : Preorder (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l4)
+  hom-preorder-Poset =
+    hom-preorder-Preorder (preorder-Poset P) (preorder-Poset Q)
+
+  hom-poset-Poset : Poset (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l4)
+  pr1 hom-poset-Poset = hom-preorder-Poset
+  pr2 hom-poset-Poset = antisymmetric-leq-hom-Poset
+```

src/order-theory/order-preserving-maps-preorders.lagda.md

@@ -231,3 +231,41 @@ module _
   involutive-eq-associative-comp-hom-Preorder =
     involutive-eq-eq associative-comp-hom-Preorder
 ```
+
+### Pointwise inequality of order preserving maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (P : Preorder l1 l2) (Q : Preorder l3 l4)
+  where
+
+  leq-hom-Preorder : (f g : hom-Preorder P Q) → UU (l1 ⊔ l4)
+  leq-hom-Preorder f g =
+    (x : type-Preorder P) →
+    leq-Preorder Q (map-hom-Preorder P Q f x) (map-hom-Preorder P Q g x)
+
+  is-prop-leq-hom-Preorder :
+    (f g : hom-Preorder P Q) → is-prop (leq-hom-Preorder f g)
+  is-prop-leq-hom-Preorder f g =
+    is-prop-Π (λ x → is-prop-leq-Preorder Q _ _)
+
+  leq-prop-hom-Preorder :
+    (f g : hom-Preorder P Q) → Prop (l1 ⊔ l4)
+  pr1 (leq-prop-hom-Preorder f g) = leq-hom-Preorder f g
+  pr2 (leq-prop-hom-Preorder f g) = is-prop-leq-hom-Preorder f g
+
+  refl-leq-hom-Preorder : (f : hom-Preorder P Q) → leq-hom-Preorder f f
+  refl-leq-hom-Preorder f x = refl-leq-Preorder Q (map-hom-Preorder P Q f x)
+
+  transitive-leq-hom-Preorder :
+    (f g h : hom-Preorder P Q) →
+    leq-hom-Preorder g h → leq-hom-Preorder f g → leq-hom-Preorder f h
+  transitive-leq-hom-Preorder f g h H K x =
+    transitive-leq-Preorder Q _ _ _ (H x) (K x)
+
+  hom-preorder-Preorder : Preorder (l1 ⊔ l2 ⊔ l3 ⊔ l4) (l1 ⊔ l4)
+  pr1 hom-preorder-Preorder = hom-Preorder P Q
+  pr1 (pr2 hom-preorder-Preorder) = leq-prop-hom-Preorder
+  pr1 (pr2 (pr2 hom-preorder-Preorder)) = refl-leq-hom-Preorder
+  pr2 (pr2 (pr2 hom-preorder-Preorder)) = transitive-leq-hom-Preorder
+```