Tight apartness relations

module foundation.tight-apartness-relations where

open import foundation.apartness-relations
open import foundation.binary-relations
open import foundation.function-extensionality
open import foundation.propositional-truncations

open import foundation-core.cartesian-product-types
open import foundation-core.dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.negation
open import foundation-core.propositions
open import foundation-core.universe-levels

Idea

A relation R is said to be tight if for every x y : A we have ¬ (R x y) → (x ＝ y).

Definition

module _
  {l1 l2 : Level} {A : UU l1} (R : A → A → Prop l2)
  where

  is-tight : UU (l1 ⊔ l2)
  is-tight = (x y : A) → ¬ (type-Prop (R x y)) → x ＝ y

  is-tight-apartness-relation : UU (l1 ⊔ l2)
  is-tight-apartness-relation =
    is-apartness-relation R × is-tight

is-tight-Apartness-Relation :
  {l1 l2 : Level} {A : UU l1} (R : Apartness-Relation l2 A) → UU (l1 ⊔ l2)
is-tight-Apartness-Relation R = is-tight (rel-Apartness-Relation R)

Tight-Apartness-Relation :
  {l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2)
Tight-Apartness-Relation l2 A =
  Σ (Apartness-Relation l2 A) (λ R → is-tight-Apartness-Relation R)

module _
  {l1 l2 : Level} {A : UU l1} (R : Tight-Apartness-Relation l2 A)
  where

  apartness-relation-Tight-Apartness-Relation :
    Apartness-Relation l2 A
  apartness-relation-Tight-Apartness-Relation = pr1 R

  is-tight-apartness-relation-Tight-Apartness-Relation :
    is-tight-Apartness-Relation apartness-relation-Tight-Apartness-Relation
  is-tight-apartness-relation-Tight-Apartness-Relation = pr2 R

Types with tight apartness

Type-With-Tight-Apartness : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Type-With-Tight-Apartness l1 l2 =
  Σ ( Type-With-Apartness l1 l2)
    ( λ X → is-tight (rel-apart-Type-With-Apartness X))

module _
  {l1 l2 : Level} (X : Type-With-Tight-Apartness l1 l2)
  where

  type-with-apartness-Type-With-Tight-Apartness : Type-With-Apartness l1 l2
  type-with-apartness-Type-With-Tight-Apartness = pr1 X

  type-Type-With-Tight-Apartness : UU l1
  type-Type-With-Tight-Apartness =
    type-Type-With-Apartness type-with-apartness-Type-With-Tight-Apartness

  rel-apart-Type-With-Tight-Apartness :
    Rel-Prop l2 type-Type-With-Tight-Apartness
  rel-apart-Type-With-Tight-Apartness =
    rel-apart-Type-With-Apartness type-with-apartness-Type-With-Tight-Apartness

  apart-Type-With-Tight-Apartness :
    Rel l2 type-Type-With-Tight-Apartness
  apart-Type-With-Tight-Apartness =
    apart-Type-With-Apartness type-with-apartness-Type-With-Tight-Apartness

  is-tight-apart-Type-With-Tight-Apartness :
    is-tight rel-apart-Type-With-Tight-Apartness
  is-tight-apart-Type-With-Tight-Apartness = pr2 X

Properties

The apartness relation of functions into a type with tight apartness is tight

is-tight-apartness-function-into-Type-With-Tight-Apartness :
  {l1 l2 l3 : Level} {X : UU l1} (Y : Type-With-Tight-Apartness l2 l3) →
  is-tight
    ( rel-apart-function-into-Type-With-Apartness X
      ( type-with-apartness-Type-With-Tight-Apartness Y))
is-tight-apartness-function-into-Type-With-Tight-Apartness Y f g H =
  eq-htpy
    ( λ x →
      is-tight-apart-Type-With-Tight-Apartness Y
        ( f x)
        ( g x)
        ( λ u → H ( unit-trunc-Prop (x , u))))

exp-Type-With-Tight-Apartness :
  {l1 l2 l3 : Level} (X : UU l1) → Type-With-Tight-Apartness l2 l3 →
  Type-With-Tight-Apartness (l1 ⊔ l2) (l1 ⊔ l3)
pr1 (exp-Type-With-Tight-Apartness X Y) =
  exp-Type-With-Apartness X (type-with-apartness-Type-With-Tight-Apartness Y)
pr2 (exp-Type-With-Tight-Apartness X Y) =
  is-tight-apartness-function-into-Type-With-Tight-Apartness Y