# Large binary relations

Content created by Fredrik Bakke, Egbert Rijke, Julian KG, fernabnor, Gregor Perčič and louismntnu.

Created on 2023-06-25.

module foundation.large-binary-relations where

Imports
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
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, 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

module _
{α : Level → Level} (β : Level → Level → Level)
(A : (l : Level) → UU (α l))
where

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

is-prop-Large-Relation :
{α : Level → Level} {β : Level → Level → Level}
(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)
(A : (l : Level) → UU (α l)) →
UUω
Large-Relation-Prop β A = {l1 l2 : Level} → A l1 → A l2 → Prop (β l1 l2)

module _
{α : Level → Level} {β : Level → Level → Level}
(A : (l : Level) → UU (α l))
(R : Large-Relation-Prop β A)
where

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

module _
{α : Level → Level} {β : Level → Level → Level}
(A : (l : Level) → UU (α l))
where

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-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

module _
{α : Level → Level} {β : Level → Level → Level}
(A : (l : Level) → UU (α l))
(R : Large-Relation β A)
where

is-reflexive-Large-Relation : UUω
is-reflexive-Large-Relation = {l : Level} (x : A l) → R x x

is-symmetric-Large-Relation : UUω
is-symmetric-Large-Relation =
{l1 l2 : Level} (x : A l1) (y : A l2) → R x y → R y x

is-transitive-Large-Relation : UUω
is-transitive-Large-Relation =
{l1 l2 l3 : Level} (x : A l1) (y : A l2) (z : A l3) → R y z → R x y → R x z

is-antisymmetric-Large-Relation : UUω
is-antisymmetric-Large-Relation =
{l : Level} → is-antisymmetric (relation-Large-Relation A R l)

module _
{α : Level → Level} {β : Level → Level → Level}
(A : (l : Level) → UU (α l))
(R : Large-Relation-Prop β A)
where

is-reflexive-Large-Relation-Prop : UUω
is-reflexive-Large-Relation-Prop =
is-reflexive-Large-Relation A (large-relation-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 (large-relation-Large-Relation-Prop A R)

is-antisymmetric-Large-Relation-Prop : UUω
is-antisymmetric-Large-Relation-Prop =
is-antisymmetric-Large-Relation A (large-relation-Large-Relation-Prop A R)