Tight large apartness relations

Content created by Louis Wasserman.

Created on 2026-02-21.
Last modified on 2026-02-21.

module foundation.tight-large-apartness-relations where
Imports 
open import foundation.disjunction
open import foundation.empty-types
open import foundation.identity-types
open import foundation.large-apartness-relations
open import foundation.large-binary-relations
open import foundation.large-equivalence-relations
open import foundation.large-similarity-relations
open import foundation.negation
open import foundation.tight-apartness-relations
open import foundation.universe-levels

Idea

A large apartness relation is tight if it is tight at every universe level, that is, if x and y are at the same universe level and are not apart, then they are equal.

Definition

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

  is-tight-Large-Apartness-Relation : UUω
  is-tight-Large-Apartness-Relation =
    (l : Level) →
    is-tight-Apartness-Relation
      ( apartness-relation-Large-Apartness-Relation R l)

record
  Tight-Large-Apartness-Relation
    {α : Level → Level}
    (β : Level → Level → Level)
    (A : (l : Level) → UU (α l)) : UUω
  where

  field
    large-apartness-relation-Tight-Large-Apartness-Relation :
      Large-Apartness-Relation β A
    is-tight-large-apartness-relation-Tight-Large-Apartness-Relation :
      is-tight-Large-Apartness-Relation
        ( large-apartness-relation-Tight-Large-Apartness-Relation)

  apart-prop-Tight-Large-Apartness-Relation : Large-Relation-Prop β A
  apart-prop-Tight-Large-Apartness-Relation =
    apart-prop-Large-Apartness-Relation
      ( large-apartness-relation-Tight-Large-Apartness-Relation)

  apart-Tight-Large-Apartness-Relation : Large-Relation β A
  apart-Tight-Large-Apartness-Relation =
    apart-Large-Apartness-Relation
      ( large-apartness-relation-Tight-Large-Apartness-Relation)

  antirefl-Tight-Large-Apartness-Relation :
    is-antireflexive-Large-Relation-Prop
      ( A)
      ( apart-prop-Tight-Large-Apartness-Relation)
  antirefl-Tight-Large-Apartness-Relation =
    antirefl-Large-Apartness-Relation
      ( large-apartness-relation-Tight-Large-Apartness-Relation)

  symmetric-Tight-Large-Apartness-Relation :
    is-symmetric-Large-Relation-Prop
      ( A)
      ( apart-prop-Tight-Large-Apartness-Relation)
  symmetric-Tight-Large-Apartness-Relation =
    symmetric-Large-Apartness-Relation
      ( large-apartness-relation-Tight-Large-Apartness-Relation)

  cotransitive-Tight-Large-Apartness-Relation :
    is-cotransitive-Large-Relation-Prop
      ( A)
      ( apart-prop-Tight-Large-Apartness-Relation)
  cotransitive-Tight-Large-Apartness-Relation =
    cotransitive-Large-Apartness-Relation
      ( large-apartness-relation-Tight-Large-Apartness-Relation)

open Tight-Large-Apartness-Relation public

Properties

A tight large apartness relation induces a large similarity relation

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

  sim-prop-Tight-Large-Apartness-Relation : Large-Relation-Prop β A
  sim-prop-Tight-Large-Apartness-Relation x y =
    ¬' apart-prop-Tight-Large-Apartness-Relation R x y

  sim-Tight-Large-Apartness-Relation : Large-Relation β A
  sim-Tight-Large-Apartness-Relation =
    large-relation-Large-Relation-Prop A sim-prop-Tight-Large-Apartness-Relation

  abstract
    eq-sim-Tight-Large-Apartness-Relation :
      {l : Level} (x y : A l) →
      sim-Tight-Large-Apartness-Relation x y → x ＝ y
    eq-sim-Tight-Large-Apartness-Relation {l} =
      is-tight-large-apartness-relation-Tight-Large-Apartness-Relation R l

  large-equivalence-relation-Tight-Large-Apartness-Relation :
    Large-Equivalence-Relation β A
  large-equivalence-relation-Tight-Large-Apartness-Relation =
    large-equivalence-relation-Large-Apartness-Relation
      ( large-apartness-relation-Tight-Large-Apartness-Relation R)

  large-similarity-relation-Tight-Large-Apartness-Relation :
    Large-Similarity-Relation β A
  large-similarity-relation-Tight-Large-Apartness-Relation =
    λ where
      .large-equivalence-relation-Large-Similarity-Relation →
        large-equivalence-relation-Tight-Large-Apartness-Relation
      .eq-sim-Large-Similarity-Relation →
        eq-sim-Tight-Large-Apartness-Relation

Recent changes