Strict symmetrizations of binary relations

src/category-theory/large-precategories.lagda.md

@@ -34,6 +34,7 @@ be done with Σ-types, we must use a record type.)
 ```agda
 record
   Large-Precategory (α : Level → Level) (β : Level → Level → Level) : UUω where
+
   field
     obj-Large-Precategory :
       (l : Level) → UU (α l)
@@ -45,10 +46,10 @@ record
       Set (β l1 l2)
 
   hom-Large-Precategory :
-    {l1 l2 : Level}
-    (X : obj-Large-Precategory l1)
-    (Y : obj-Large-Precategory l2) →
-    UU (β l1 l2)
+      {l1 l2 : Level} →
+      obj-Large-Precategory l1 →
+      obj-Large-Precategory l2 →
+      UU (β l1 l2)
   hom-Large-Precategory X Y = type-Set (hom-set-Large-Precategory X Y)
 
   is-set-hom-Large-Precategory :

src/foundation-core/equivalence-relations.lagda.md

@@ -34,7 +34,8 @@ is-equivalence-relation :
   {l1 l2 : Level} {A : UU l1} (R : Relation-Prop l2 A) → UU (l1 ⊔ l2)
 is-equivalence-relation R =
   is-reflexive-Relation-Prop R ×
-    ( is-symmetric-Relation-Prop R × is-transitive-Relation-Prop R)
+  is-symmetric-Relation-Prop R ×
+  is-transitive-Relation-Prop R
 
 equivalence-relation :
   (l : Level) {l1 : Level} (A : UU l1) → UU ((lsuc l) ⊔ l1)

src/foundation.lagda.md

@@ -266,6 +266,7 @@ open import foundation.operations-span-diagrams public
 open import foundation.operations-spans public
 open import foundation.operations-spans-families-of-types public
 open import foundation.opposite-spans public
+open import foundation.outer-2-horn-filler-conditions-binary-relations public
 open import foundation.pairs-of-distinct-elements public
 open import foundation.partial-elements public
 open import foundation.partial-functions public
@@ -310,7 +311,6 @@ open import foundation.pullbacks public
 open import foundation.pullbacks-subtypes public
 open import foundation.raising-universe-levels public
 open import foundation.reflecting-maps-equivalence-relations public
-open import foundation.reflexive-relations public
 open import foundation.regensburg-extension-fundamental-theorem-of-identity-types public
 open import foundation.relaxed-sigma-decompositions public
 open import foundation.repetitions-of-values public
@@ -346,6 +346,7 @@ open import foundation.spans-families-of-types public
 open import foundation.split-surjective-maps public
 open import foundation.standard-apartness-relations public
 open import foundation.standard-pullbacks public
+open import foundation.strict-symmetrization-binary-relations public
 open import foundation.strictly-involutive-identity-types public
 open import foundation.strictly-right-unital-concatenation-identifications public
 open import foundation.strongly-extensional-maps public

src/foundation/binary-relations.lagda.md

@@ -150,7 +150,7 @@ module _
 
 ### The predicate of being a transitive relation valued in propositions
 
-A relation `R` on a type `A` valued in propositions is said to be \*\*transitive
+A relation `R` on a type `A` valued in propositions is said to be **transitive**
 if its underlying relation is transitive.
 
 ```agda

src/foundation/discrete-reflexive-relations.lagda.md

@@ -9,7 +9,6 @@ module foundation.discrete-reflexive-relations where
 ```agda
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
-open import foundation.reflexive-relations
 open import foundation.universe-levels
 
 open import foundation-core.identity-types

src/foundation/exclusive-disjunction.lagda.md

@@ -146,7 +146,7 @@ pr1 (symmetric-xor-Prop E) = type-symmetric-xor-Prop E
 pr2 (symmetric-xor-Prop E) = is-prop-type-symmetric-xor-Prop E
 ```
 
-### Second definition of exclusiove disjunction
+### Second definition of exclusive disjunction
 
 ```agda
 module _

src/foundation/large-binary-relations.lagda.md

@@ -19,89 +19,86 @@ open import foundation-core.propositions
 
 ## Idea
 
-A **large binary relation** on a family of types indexed by universe levels `A`
-is a family of types `R x y` depending on two variables `x : A l1` and
-`y : A l2`. In the special case where each `R x y` is a
-[proposition](foundation-core.propositions.md), we say that the relation is
-valued in propositions. Thus, we take a general relation to mean a
-_proof-relevant_ relation.
+A
+{{#concept "large binary relation" Disambiguation="valued in types" Agda=Large-Relation}}
+on a family of types indexed by universe levels `A` is a family of types `R x y`
+depending on two variables `x : A l1` and `y : A l2`. In the special case where
+each `R x y` is a [proposition](foundation-core.propositions.md), we say that
+the relation is valued in propositions. Thus, we take a general relation to mean
+a _proof-relevant_ relation.
 
 ## Definition
 
 ### Large relations valued in types
 
 ```agda
-Large-Relation :
-  (α : Level → Level) (β : Level → Level → Level)
-  (A : (l : Level) → UU (α l)) → UUω
-Large-Relation α β A = {l1 l2 : Level} → A l1 → A l2 → UU (β l1 l2)
+module _
+  {α : Level → Level} (β : Level → Level → Level)
+  (A : (l : Level) → UU (α l))
+  where
 
-total-space-Large-Relation :
-  {α : Level → Level} {β : Level → Level → Level}
-  (A : (l : Level) → UU (α l)) → Large-Relation α β A → UUω
-total-space-Large-Relation A R =
-  (l1 l2 : Level) → Σ (A l1 × A l2) (λ (a , a') → R a a')
+  Large-Relation : UUω
+  Large-Relation = {l1 l2 : Level} → A l1 → A l2 → UU (β l1 l2)
+
+  total-space-Large-Relation : Large-Relation → UUω
+  total-space-Large-Relation R =
+    (l1 l2 : Level) → Σ (A l1 × A l2) (λ (a , a') → R a a')
 ```
 
 ### Large relations valued in propositions
 
 ```agda
 is-prop-Large-Relation :
   {α : Level → Level} {β : Level → Level → Level}
-  (A : (l : Level) → UU (α l)) → Large-Relation α β A → UUω
+  (A : (l : Level) → UU (α l)) → Large-Relation β A → UUω
 is-prop-Large-Relation A R =
   {l1 l2 : Level} (x : A l1) (y : A l2) → is-prop (R x y)
 
 Large-Relation-Prop :
-  (α : Level → Level) (β : Level → Level → Level)
+  {α : Level → Level} (β : Level → Level → Level)
   (A : (l : Level) → UU (α l)) →
   UUω
-Large-Relation-Prop α β A = {l1 l2 : Level} → A l1 → A l2 → Prop (β l1 l2)
+Large-Relation-Prop β A = {l1 l2 : Level} → A l1 → A l2 → Prop (β l1 l2)
 
-type-Large-Relation-Prop :
-  {α : Level → Level} {β : Level → Level → Level}
-  (A : (l : Level) → UU (α l)) →
-  Large-Relation-Prop α β A → Large-Relation α β A
-type-Large-Relation-Prop A R x y = pr1 (R x y)
-
-is-prop-type-Large-Relation-Prop :
+module _
   {α : Level → Level} {β : Level → Level → Level}
   (A : (l : Level) → UU (α l))
-  (R : Large-Relation-Prop α β A) →
-  is-prop-Large-Relation A (type-Large-Relation-Prop A R)
-is-prop-type-Large-Relation-Prop A R x y = pr2 (R x y)
+  (R : Large-Relation-Prop β A)
+  where
 
-total-space-Large-Relation-Prop :
-  {α : Level → Level} {β : Level → Level → Level}
-  (A : (l : Level) → UU (α l))
-  (R : Large-Relation-Prop α β A) →
-  UUω
-total-space-Large-Relation-Prop A R =
-  (l1 l2 : Level) →
-  Σ (A l1 × A l2) (λ (a , a') → type-Large-Relation-Prop A R a a')
+  large-relation-Large-Relation-Prop : Large-Relation β A
+  large-relation-Large-Relation-Prop x y = type-Prop (R x y)
+
+  is-prop-large-relation-Large-Relation-Prop :
+    is-prop-Large-Relation A large-relation-Large-Relation-Prop
+  is-prop-large-relation-Large-Relation-Prop x y = is-prop-type-Prop (R x y)
+
+  total-space-Large-Relation-Prop : UUω
+  total-space-Large-Relation-Prop =
+    (l1 l2 : Level) →
+    Σ (A l1 × A l2) (λ (a , a') → large-relation-Large-Relation-Prop a a')
 ```
 
 ## Small relations from large relations
 
 ```agda
-relation-Large-Relation :
+module _
   {α : Level → Level} {β : Level → Level → Level}
-  (A : (l : Level) → UU (α l)) (R : Large-Relation α β A)
-  (l : Level) → Relation (β l l) (A l)
-relation-Large-Relation A R l x y = R x y
+  (A : (l : Level) → UU (α l))
+  where
 
-relation-prop-Large-Relation-Prop :
-  {α : Level → Level} {β : Level → Level → Level}
-  (A : (l : Level) → UU (α l)) (R : Large-Relation-Prop α β A)
-  (l : Level) → Relation-Prop (β l l) (A l)
-relation-prop-Large-Relation-Prop A R l x y = R x y
+  relation-Large-Relation :
+    (R : Large-Relation β A) (l : Level) → Relation (β l l) (A l)
+  relation-Large-Relation R l x y = R x y
 
-relation-Large-Relation-Prop :
-  {α : Level → Level} {β : Level → Level → Level}
-  (A : (l : Level) → UU (α l)) (R : Large-Relation-Prop α β A)
-  (l : Level) → Relation (β l l) (A l)
-relation-Large-Relation-Prop A R =
-  relation-Large-Relation A (type-Large-Relation-Prop A R)
+  relation-prop-Large-Relation-Prop :
+    (R : Large-Relation-Prop β A) (l : Level) → Relation-Prop (β l l) (A l)
+  relation-prop-Large-Relation-Prop R l x y = R x y
+
+  relation-Large-Relation-Prop :
+    (R : Large-Relation-Prop β A) (l : Level) → Relation (β l l) (A l)
+  relation-Large-Relation-Prop R =
+    relation-Large-Relation (large-relation-Large-Relation-Prop A R)
 ```
 
 ## Specifications of properties of binary relations
@@ -110,12 +107,11 @@ relation-Large-Relation-Prop A R =
 module _
   {α : Level → Level} {β : Level → Level → Level}
   (A : (l : Level) → UU (α l))
-  (R : Large-Relation α β A)
+  (R : Large-Relation β A)
   where
 
   is-reflexive-Large-Relation : UUω
-  is-reflexive-Large-Relation =
-    {l : Level} → is-reflexive (relation-Large-Relation A R l)
+  is-reflexive-Large-Relation = {l : Level} (x : A l) → R x x
 
   is-symmetric-Large-Relation : UUω
   is-symmetric-Large-Relation =
@@ -132,24 +128,24 @@ module _
 module _
   {α : Level → Level} {β : Level → Level → Level}
   (A : (l : Level) → UU (α l))
-  (R : Large-Relation-Prop α β A)
+  (R : Large-Relation-Prop β A)
   where
 
   is-reflexive-Large-Relation-Prop : UUω
   is-reflexive-Large-Relation-Prop =
-    is-reflexive-Large-Relation A (type-Large-Relation-Prop A R)
+    is-reflexive-Large-Relation A (large-relation-Large-Relation-Prop A R)
 
-  is-large-symmetric-Large-Relation-Prop : UUω
-  is-large-symmetric-Large-Relation-Prop =
-    is-symmetric-Large-Relation A (type-Large-Relation-Prop A R)
+  is-symmetric-Large-Relation-Prop : UUω
+  is-symmetric-Large-Relation-Prop =
+    is-symmetric-Large-Relation A (large-relation-Large-Relation-Prop A R)
 
   is-transitive-Large-Relation-Prop : UUω
   is-transitive-Large-Relation-Prop =
-    is-transitive-Large-Relation A (type-Large-Relation-Prop A R)
+    is-transitive-Large-Relation A (large-relation-Large-Relation-Prop A R)
 
   is-antisymmetric-Large-Relation-Prop : UUω
   is-antisymmetric-Large-Relation-Prop =
-    is-antisymmetric-Large-Relation A (type-Large-Relation-Prop A R)
+    is-antisymmetric-Large-Relation A (large-relation-Large-Relation-Prop A R)
 ```
 
 ## See also

src/foundation/large-locale-of-subtypes.lagda.md

@@ -75,15 +75,13 @@ module _
 
   leq-prop-powerset-Large-Locale :
     Large-Relation-Prop
-      ( λ l2 → l1 ⊔ lsuc l2)
       ( λ l2 l3 → l1 ⊔ l2 ⊔ l3)
       ( type-powerset-Large-Locale A)
   leq-prop-powerset-Large-Locale =
     leq-prop-Large-Locale (powerset-Large-Locale A)
 
   leq-powerset-Large-Locale :
     Large-Relation
-      ( λ l2 → l1 ⊔ lsuc l2)
       ( λ l2 l3 → l1 ⊔ l2 ⊔ l3)
       ( type-powerset-Large-Locale A)
   leq-powerset-Large-Locale =