Skip to content

Commit

Permalink
capitalization
Browse files Browse the repository at this point in the history
  • Loading branch information
@EgbertRijke
EgbertRijke committed Sep 12, 2023
1 parent 63c807b commit 4bf206b
Showing 1 changed file with 64 additions and 64 deletions.
128 changes: 64 additions & 64 deletions src/foundation/symmetric-binary-relations.lagda.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,105 +49,105 @@ universe `𝒰`.
### Symmetric binary relations

```agda
symmetric-binary-relation :
Symmetric-Relation :
{l1 : Level} (l2 : Level) → UU l1 → UU (l1 ⊔ lsuc l2)
symmetric-binary-relation l2 A = symmetric-operation A (UU l2)
Symmetric-Relation l2 A = symmetric-operation A (UU l2)
```

### Action on symmetries of symmetric binary relations

```agda
module _
{l1 l2 : Level} {A : UU l1} (R : symmetric-binary-relation l2 A)
{l1 l2 : Level} {A : UU l1} (R : Symmetric-Relation l2 A)
where

abstract
equiv-tr-symmetric-binary-relation :
equiv-tr-Symmetric-Relation :
(p q : unordered-pair A) → Eq-unordered-pair p q → R p ≃ R q
equiv-tr-symmetric-binary-relation p =
equiv-tr-Symmetric-Relation p =
ind-Eq-unordered-pair p (λ q e → R p ≃ R q) id-equiv

compute-refl-equiv-tr-symmetric-binary-relation :
compute-refl-equiv-tr-Symmetric-Relation :
(p : unordered-pair A) →
equiv-tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ＝
equiv-tr-Symmetric-Relation p p (refl-Eq-unordered-pair p) ＝
id-equiv
compute-refl-equiv-tr-symmetric-binary-relation p =
compute-refl-equiv-tr-Symmetric-Relation p =
compute-refl-ind-Eq-unordered-pair p (λ q e → R p ≃ R q) id-equiv

htpy-compute-refl-equiv-tr-symmetric-binary-relation :
htpy-compute-refl-equiv-tr-Symmetric-Relation :
(p : unordered-pair A) →
htpy-equiv
( equiv-tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p))
( equiv-tr-Symmetric-Relation p p (refl-Eq-unordered-pair p))
( id-equiv)
htpy-compute-refl-equiv-tr-symmetric-binary-relation p =
htpy-eq-equiv (compute-refl-equiv-tr-symmetric-binary-relation p)
htpy-compute-refl-equiv-tr-Symmetric-Relation p =
htpy-eq-equiv (compute-refl-equiv-tr-Symmetric-Relation p)

abstract
tr-symmetric-binary-relation :
tr-Symmetric-Relation :
(p q : unordered-pair A) → Eq-unordered-pair p q → R p → R q
tr-symmetric-binary-relation p q e =
map-equiv (equiv-tr-symmetric-binary-relation p q e)
tr-Symmetric-Relation p q e =
map-equiv (equiv-tr-Symmetric-Relation p q e)

tr-inv-symmetric-binary-relation :
tr-inv-Symmetric-Relation :
(p q : unordered-pair A) → Eq-unordered-pair p q → R q → R p
tr-inv-symmetric-binary-relation p q e =
map-inv-equiv (equiv-tr-symmetric-binary-relation p q e)
tr-inv-Symmetric-Relation p q e =
map-inv-equiv (equiv-tr-Symmetric-Relation p q e)

is-section-tr-inv-symmetric-binary-relation :
is-section-tr-inv-Symmetric-Relation :
(p q : unordered-pair A) (e : Eq-unordered-pair p q) →
tr-symmetric-binary-relation p q e ∘
tr-inv-symmetric-binary-relation p q e ~
tr-Symmetric-Relation p q e ∘
tr-inv-Symmetric-Relation p q e ~
id
is-section-tr-inv-symmetric-binary-relation p q e =
is-section-map-inv-equiv (equiv-tr-symmetric-binary-relation p q e)
is-section-tr-inv-Symmetric-Relation p q e =
is-section-map-inv-equiv (equiv-tr-Symmetric-Relation p q e)

is-retraction-tr-inv-symmetric-binary-relation :
is-retraction-tr-inv-Symmetric-Relation :
(p q : unordered-pair A) (e : Eq-unordered-pair p q) →
tr-inv-symmetric-binary-relation p q e ∘
tr-symmetric-binary-relation p q e ~
tr-inv-Symmetric-Relation p q e ∘
tr-Symmetric-Relation p q e ~
id
is-retraction-tr-inv-symmetric-binary-relation p q e =
is-retraction-map-inv-equiv (equiv-tr-symmetric-binary-relation p q e)
is-retraction-tr-inv-Symmetric-Relation p q e =
is-retraction-map-inv-equiv (equiv-tr-Symmetric-Relation p q e)

compute-refl-tr-symmetric-binary-relation :
compute-refl-tr-Symmetric-Relation :
(p : unordered-pair A) →
tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ＝ id
compute-refl-tr-symmetric-binary-relation p =
ap map-equiv (compute-refl-equiv-tr-symmetric-binary-relation p)
tr-Symmetric-Relation p p (refl-Eq-unordered-pair p) ＝ id
compute-refl-tr-Symmetric-Relation p =
ap map-equiv (compute-refl-equiv-tr-Symmetric-Relation p)

htpy-compute-refl-tr-symmetric-binary-relation :
htpy-compute-refl-tr-Symmetric-Relation :
(p : unordered-pair A) →
tr-symmetric-binary-relation p p (refl-Eq-unordered-pair p) ~ id
htpy-compute-refl-tr-symmetric-binary-relation p =
htpy-eq (compute-refl-tr-symmetric-binary-relation p)
tr-Symmetric-Relation p p (refl-Eq-unordered-pair p) ~ id
htpy-compute-refl-tr-Symmetric-Relation p =
htpy-eq (compute-refl-tr-Symmetric-Relation p)
```

### The underlying binary relation of a symmetric binary relation

```agda
module _
{l1 l2 : Level} {A : UU l1} (R : symmetric-binary-relation l2 A)
{l1 l2 : Level} {A : UU l1} (R : Symmetric-Relation l2 A)
where

relation-symmetric-binary-relation : Relation l2 A
relation-symmetric-binary-relation x y = R (standard-unordered-pair x y)
relation-Symmetric-Relation : Relation l2 A
relation-Symmetric-Relation x y = R (standard-unordered-pair x y)

equiv-symmetric-relation-symmetric-binary-relation :
equiv-symmetric-relation-Symmetric-Relation :
{x y : A} →
relation-symmetric-binary-relation x y ≃
relation-symmetric-binary-relation y x
equiv-symmetric-relation-symmetric-binary-relation {x} {y} =
equiv-tr-symmetric-binary-relation R
relation-Symmetric-Relation x y ≃
relation-Symmetric-Relation y x
equiv-symmetric-relation-Symmetric-Relation {x} {y} =
equiv-tr-Symmetric-Relation R
( standard-unordered-pair x y)
( standard-unordered-pair y x)
( swap-standard-unordered-pair x y)

symmetric-relation-symmetric-binary-relation :
symmetric-relation-Symmetric-Relation :
{x y : A} →
relation-symmetric-binary-relation x y →
relation-symmetric-binary-relation y x
symmetric-relation-symmetric-binary-relation =
map-equiv equiv-symmetric-relation-symmetric-binary-relation
relation-Symmetric-Relation x y →
relation-Symmetric-Relation y x
symmetric-relation-Symmetric-Relation =
map-equiv equiv-symmetric-relation-Symmetric-Relation
```

### The forgetful functor from binary relations to symmetric binary relations
Expand All @@ -157,17 +157,17 @@ module _
{l1 l2 : Level} {A : UU l1} (R : Relation l2 A)
where

symmetric-binary-relation-Relation : symmetric-binary-relation l2 A
symmetric-binary-relation-Relation p =
symmetric-relation-Relation : Symmetric-Relation l2 A
symmetric-relation-Relation p =
Σ ( type-unordered-pair p)
( λ i →
R (element-unordered-pair p i) (other-element-unordered-pair p i))

unit-symmetric-binary-relation-Relation :
unit-symmetric-relation-Relation :
(x y : A) → R x y →
relation-symmetric-binary-relation symmetric-binary-relation-Relation x y
pr1 (unit-symmetric-binary-relation-Relation x y r) = zero-Fin 1
pr2 (unit-symmetric-binary-relation-Relation x y r) =
relation-Symmetric-Relation symmetric-relation-Relation x y
pr1 (unit-symmetric-relation-Relation x y r) = zero-Fin 1
pr2 (unit-symmetric-relation-Relation x y r) =
tr
( R x)
( inv (compute-other-element-standard-unordered-pair x y (zero-Fin 1)))
Expand All @@ -181,18 +181,18 @@ module _
{l1 l2 l3 : Level} {A : UU l1}
where

hom-symmetric-binary-relation :
symmetric-binary-relation l2 A → symmetric-binary-relation l3 A →
hom-Symmetric-Relation :
Symmetric-Relation l2 A → Symmetric-Relation l3 A →
UU (lsuc lzero ⊔ l1 ⊔ l2 ⊔ l3)
hom-symmetric-binary-relation R S =
hom-Symmetric-Relation R S =
(p : unordered-pair A) → R p → S p

hom-relation-hom-symmetric-binary-relation :
(R : symmetric-binary-relation l2 A) (S : symmetric-binary-relation l3 A) →
hom-symmetric-binary-relation R S →
hom-relation-hom-Symmetric-Relation :
(R : Symmetric-Relation l2 A) (S : Symmetric-Relation l3 A) →
hom-Symmetric-Relation R S →
hom-Relation
( relation-symmetric-binary-relation R)
( relation-symmetric-binary-relation S)
hom-relation-hom-symmetric-binary-relation R S f x y =
( relation-Symmetric-Relation R)
( relation-Symmetric-Relation S)
hom-relation-hom-Symmetric-Relation R S f x y =
f (standard-unordered-pair x y)
```

0 comments on commit 4bf206b

Please sign in to comment.