{-# OPTIONS --safe #-}
module Cubical.Relation.Binary.Base where
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Fiberwise
open import Cubical.Functions.Embedding
open import Cubical.Functions.Logic using (_⊔′_)
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma
open import Cubical.Data.Sum.Base as ⊎
open import Cubical.HITs.SetQuotients.Base
open import Cubical.HITs.PropositionalTruncation as ∥₁
open import Cubical.Relation.Nullary.Base
open import Cubical.Induction.WellFounded
private
variable
ℓA ℓ≅A ℓA' ℓ≅A' : Level
Rel : ∀ {ℓa ℓb} (A : Type ℓa) (B : Type ℓb) (ℓ' : Level) → Type (ℓ-max (ℓ-max ℓa ℓb) (ℓ-suc ℓ'))
Rel A B ℓ' = A → B → Type ℓ'
PropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
PropRel A B ℓ' = Σ[ R ∈ Rel A B ℓ' ] ∀ a b → isProp (R a b)
idPropRel : ∀ {ℓ} (A : Type ℓ) → PropRel A A ℓ
idPropRel A .fst a a' = ∥ a ≡ a' ∥₁
idPropRel A .snd _ _ = squash₁
invPropRel : ∀ {ℓ ℓ'} {A B : Type ℓ}
→ PropRel A B ℓ' → PropRel B A ℓ'
invPropRel R .fst b a = R .fst a b
invPropRel R .snd b a = R .snd a b
compPropRel : ∀ {ℓ ℓ' ℓ''} {A B C : Type ℓ}
→ PropRel A B ℓ' → PropRel B C ℓ'' → PropRel A C (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
compPropRel R S .fst a c = ∥ Σ[ b ∈ _ ] (R .fst a b × S .fst b c) ∥₁
compPropRel R S .snd _ _ = squash₁
graphRel : ∀ {ℓ} {A B : Type ℓ} → (A → B) → Rel A B ℓ
graphRel f a b = f a ≡ b
module HeterogenousRelation {ℓ ℓ' : Level} {A B : Type ℓ} (R : Rel A B ℓ') where
isUniversalRel : Type (ℓ-max ℓ ℓ')
isUniversalRel = (a : A) (b : B) → R a b
module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
isRefl : Type (ℓ-max ℓ ℓ')
isRefl = (a : A) → R a a
isRefl' : Type (ℓ-max ℓ ℓ')
isRefl' = {a : A} → R a a
isIrrefl : Type (ℓ-max ℓ ℓ')
isIrrefl = (a : A) → ¬ R a a
isSym : Type (ℓ-max ℓ ℓ')
isSym = (a b : A) → R a b → R b a
isAsym : Type (ℓ-max ℓ ℓ')
isAsym = (a b : A) → R a b → ¬ R b a
isAntisym : Type (ℓ-max ℓ ℓ')
isAntisym = (a b : A) → R a b → R b a → a ≡ b
isTrans : Type (ℓ-max ℓ ℓ')
isTrans = (a b c : A) → R a b → R b c → R a c
isTrans' : Type (ℓ-max ℓ ℓ')
isTrans' = {a b c : A} → R a b → R b c → R a c
isCotrans : Type (ℓ-max ℓ ℓ')
isCotrans = (a b c : A) → R a b → (R a c ⊔′ R b c)
isWeaklyLinear : Type (ℓ-max ℓ ℓ')
isWeaklyLinear = (a b c : A) → R a b → R a c ⊔′ R c b
isConnected : Type (ℓ-max ℓ ℓ')
isConnected = (a b : A) → ¬ (a ≡ b) → R a b ⊔′ R b a
isStronglyConnected : Type (ℓ-max ℓ ℓ')
isStronglyConnected = (a b : A) → R a b ⊔′ R b a
isStronglyConnected→isConnected : isStronglyConnected → isConnected
isStronglyConnected→isConnected strong a b _ = strong a b
isIrrefl×isTrans→isAsym : isIrrefl × isTrans → isAsym
isIrrefl×isTrans→isAsym (irrefl , trans) a₀ a₁ Ra₀a₁ Ra₁a₀
= irrefl a₀ (trans a₀ a₁ a₀ Ra₀a₁ Ra₁a₀)
WellFounded→isIrrefl : WellFounded R → isIrrefl
WellFounded→isIrrefl well = WFI.induction well λ a f Raa → f a Raa Raa
IrreflKernel : Rel A A (ℓ-max ℓ ℓ')
IrreflKernel a b = R a b × (¬ a ≡ b)
ReflClosure : Rel A A (ℓ-max ℓ ℓ')
ReflClosure a b = R a b ⊎ (a ≡ b)
SymKernel : Rel A A ℓ'
SymKernel a b = R a b × R b a
SymClosure : Rel A A ℓ'
SymClosure a b = R a b ⊎ R b a
AsymKernel : Rel A A ℓ'
AsymKernel a b = R a b × (¬ R b a)
NegationRel : Rel A A ℓ'
NegationRel a b = ¬ (R a b)
module _
{ℓ'' : Level}
(P : Embedding A ℓ'')
where
private
subtype : Type ℓ''
subtype = (fst P)
toA : subtype → A
toA = fst (snd P)
InducedRelation : Rel subtype subtype ℓ'
InducedRelation a b = R (toA a) (toA b)
record isEquivRel : Type (ℓ-max ℓ ℓ') where
constructor equivRel
field
reflexive : isRefl
symmetric : isSym
transitive : isTrans
isUniversalRel→isEquivRel : HeterogenousRelation.isUniversalRel R → isEquivRel
isUniversalRel→isEquivRel u .isEquivRel.reflexive a = u a a
isUniversalRel→isEquivRel u .isEquivRel.symmetric a b _ = u b a
isUniversalRel→isEquivRel u .isEquivRel.transitive a _ c _ _ = u a c
isPropValued : Type (ℓ-max ℓ ℓ')
isPropValued = (a b : A) → isProp (R a b)
isSetValued : Type (ℓ-max ℓ ℓ')
isSetValued = (a b : A) → isSet (R a b)
isEffective : Type (ℓ-max ℓ ℓ')
isEffective =
(a b : A) → isEquiv (eq/ {R = R} a b)
impliesIdentity : Type _
impliesIdentity = {a a' : A} → (R a a') → (a ≡ a')
inequalityImplies : Type _
inequalityImplies = (a b : A) → ¬ a ≡ b → R a b
relSinglAt : (a : A) → Type (ℓ-max ℓ ℓ')
relSinglAt a = Σ[ a' ∈ A ] (R a a')
contrRelSingl : Type (ℓ-max ℓ ℓ')
contrRelSingl = (a : A) → isContr (relSinglAt a)
isUnivalent : Type (ℓ-max ℓ ℓ')
isUnivalent = (a a' : A) → (R a a') ≃ (a ≡ a')
contrRelSingl→isUnivalent : isRefl → contrRelSingl → isUnivalent
contrRelSingl→isUnivalent ρ c a a' = isoToEquiv i
where
h : isProp (relSinglAt a)
h = isContr→isProp (c a)
aρa : relSinglAt a
aρa = a , ρ a
Q : (y : A) → a ≡ y → _
Q y _ = R a y
i : Iso (R a a') (a ≡ a')
Iso.fun i r = cong fst (h aρa (a' , r))
Iso.inv i = J Q (ρ a)
Iso.rightInv i = J (λ y p → cong fst (h aρa (y , J Q (ρ a) p)) ≡ p)
(J (λ q _ → cong fst (h aρa (a , q)) ≡ refl)
(J (λ α _ → cong fst α ≡ refl) refl
(isProp→isSet h _ _ refl (h _ _)))
(sym (JRefl Q (ρ a))))
Iso.leftInv i r = J (λ w β → J Q (ρ a) (cong fst β) ≡ snd w)
(JRefl Q (ρ a)) (h aρa (a' , r))
isUnivalent→contrRelSingl : isUnivalent → contrRelSingl
isUnivalent→contrRelSingl u a = q
where
abstract
f : (x : A) → a ≡ x → R a x
f x p = invEq (u a x) p
t : singl a → relSinglAt a
t (x , p) = x , f x p
q : isContr (relSinglAt a)
q = isOfHLevelRespectEquiv 0 (t , totalEquiv _ _ f λ x → invEquiv (u a x) .snd)
(isContrSingl a)
EquivRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
EquivRel A ℓ' = Σ[ R ∈ Rel A A ℓ' ] BinaryRelation.isEquivRel R
EquivPropRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
EquivPropRel A ℓ' = Σ[ R ∈ PropRel A A ℓ' ] BinaryRelation.isEquivRel (R .fst)
record RelIso {A : Type ℓA} (_≅_ : Rel A A ℓ≅A)
{A' : Type ℓA'} (_≅'_ : Rel A' A' ℓ≅A') : Type (ℓ-max (ℓ-max ℓA ℓA') (ℓ-max ℓ≅A ℓ≅A')) where
constructor reliso
field
fun : A → A'
inv : A' → A
rightInv : (a' : A') → fun (inv a') ≅' a'
leftInv : (a : A) → inv (fun a) ≅ a
open BinaryRelation
RelIso→Iso : {A : Type ℓA} {A' : Type ℓA'}
(_≅_ : Rel A A ℓ≅A) (_≅'_ : Rel A' A' ℓ≅A')
(uni : impliesIdentity _≅_) (uni' : impliesIdentity _≅'_)
(f : RelIso _≅_ _≅'_)
→ Iso A A'
Iso.fun (RelIso→Iso _ _ _ _ f) = RelIso.fun f
Iso.inv (RelIso→Iso _ _ _ _ f) = RelIso.inv f
Iso.rightInv (RelIso→Iso _ _ uni uni' f) a'
= uni' (RelIso.rightInv f a')
Iso.leftInv (RelIso→Iso _ _ uni uni' f) a
= uni (RelIso.leftInv f a)
isIrreflIrreflKernel : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isIrrefl (IrreflKernel R)
isIrreflIrreflKernel _ _ (_ , ¬a≡a) = ¬a≡a refl
isReflReflClosure : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isRefl (ReflClosure R)
isReflReflClosure _ _ = inr refl
isConnectedStronglyConnectedIrreflKernel : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ')
→ isStronglyConnected R
→ isConnected (IrreflKernel R)
isConnectedStronglyConnectedIrreflKernel R strong a b ¬a≡b
= ∥₁.map (λ x → ⊎.rec (λ Rab → inl (Rab , ¬a≡b))
(λ Rba → inr (Rba , (λ b≡a → ¬a≡b (sym b≡a)))) x)
(strong a b)
isSymSymKernel : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isSym (SymKernel R)
isSymSymKernel _ _ _ (Rab , Rba) = Rba , Rab
isSymSymClosure : ∀{ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isSym (SymClosure R)
isSymSymClosure _ _ _ (inl Rab) = inr Rab
isSymSymClosure _ _ _ (inr Rba) = inl Rba
isAsymAsymKernel : ∀ {ℓ ℓ'} {A : Type ℓ} (R : Rel A A ℓ') → isAsym (AsymKernel R)
isAsymAsymKernel _ _ _ (Rab , _) (_ , ¬Rab) = ¬Rab Rab