Large binary relations

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

Created on 2023-06-25.
Last modified on 2024-04-11.

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)

See also

Recent changes