nLab tight relation

Redirected from "weakly tight relation".

Contents

Definition

A binary relation RR on a set AA is tight if for all elements aAa \in A and bAb \in A, ¬R(a,b)\neg R(a, b) implies that a=ba = b.

Every tight relation is a connected relation. Every connected symmetric relation is a tight relation.

 Examples

Weakly tight relations

Sometimes in constructive mathematics, what matters for a relation is not that the negation implies equality, but the negation implies the double negation of equality. Such a relation is called weakly tight.

A binary relation RR on a set AA is weakly tight if for all elements aAa \in A and bAb \in A, ¬R(a,b)\neg R(a, b) implies that ¬¬(a=b)\neg \neg (a = b). By intuitionistic contraposition, this implies that for all elements aAa \in A and bAb \in A, ¬(a=b)\neg (a = b) implies that ¬¬R(a,b)\neg \neg R(a, b).

Important examples of weakly tight relations include denial inequality.

In dependent type theory

An irreflexive relation \sim with terms a:Airr(a):(aa)a:A \vdash \mathrm{irr}(a):(a \sim a) \to \emptyset is tight if the canonical function

idtonotrel(a,b):(a= Ab)((ab))\mathrm{idtonotrel}(a, b):(a =_A b) \to ((a \sim b) \to \emptyset)

inductively defined by

idtonotrel(a,a)(refl A(a))irr(a):(aa)\mathrm{idtonotrel}(a, a)(\mathrm{refl}_A(a)) \equiv \mathrm{irr}(a):(a \sim a) \to \emptyset

is an equivalence of types

conn(a,b):isEquiv(idtonotrel(a,b))\mathrm{conn}(a, b):\mathrm{isEquiv}(\mathrm{idtonotrel}(a, b))

 See also

Created on December 8, 2022 at 17:08:57. See the history of this page for a list of all contributions to it.