{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Binary.Construct.Closure.SymmetricTransitive where
open import Level
open import Function.Base
open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_)
open import Relation.Binary.Bundles using (PartialSetoid; Setoid)
open import Relation.Binary.Structures
using (IsPartialEquivalence; IsEquivalence)
open import Relation.Binary.Definitions
using (Transitive; Symmetric; Reflexive)
private
variable
a c ℓ ℓ′ : Level
A B : Set a
module _ {A : Set a} (_≤_ : Rel A ℓ) where
data Plus⇔ : Rel A (a ⊔ ℓ) where
forth : ∀ {x y} → x ≤ y → Plus⇔ x y
back : ∀ {x y} → y ≤ x → Plus⇔ x y
forth⁺ : ∀ {x y z} → x ≤ y → Plus⇔ y z → Plus⇔ x z
back⁺ : ∀ {x y z} → y ≤ x → Plus⇔ y z → Plus⇔ x z
trans : Transitive Plus⇔
trans (forth r) rel′ = forth⁺ r rel′
trans (back r) rel′ = back⁺ r rel′
trans (forth⁺ r rel) rel′ = forth⁺ r (trans rel rel′)
trans (back⁺ r rel) rel′ = back⁺ r (trans rel rel′)
sym : Symmetric Plus⇔
sym (forth r) = back r
sym (back r) = forth r
sym (forth⁺ r rel) = trans (sym rel) (back r)
sym (back⁺ r rel) = trans (sym rel) (forth r)
isPartialEquivalence : IsPartialEquivalence Plus⇔
isPartialEquivalence = record
{ sym = sym
; trans = trans
}
partialSetoid : PartialSetoid _ _
partialSetoid = record
{ Carrier = A
; _≈_ = Plus⇔
; isPartialEquivalence = isPartialEquivalence
}
module _ (refl : Reflexive _≤_) where
isEquivalence : IsEquivalence Plus⇔
isEquivalence = record
{ refl = forth refl
; sym = sym
; trans = trans
}
setoid : Setoid _ _
setoid = record
{ Carrier = A
; _≈_ = Plus⇔
; isEquivalence = isEquivalence
}
module _ (S : Setoid c ℓ) where
private
module S = Setoid S
minimal : (f : A → S.Carrier) →
_≤_ =[ f ]⇒ S._≈_ →
Plus⇔ =[ f ]⇒ S._≈_
minimal f inj (forth r) = inj r
minimal f inj (back r) = S.sym (inj r)
minimal f inj (forth⁺ r rel) = S.trans (inj r) (minimal f inj rel)
minimal f inj (back⁺ r rel) = S.trans (S.sym (inj r)) (minimal f inj rel)
module Plus⇔Reasoning (_≤_ : Rel A ℓ) where
infix 3 forth-syntax back-syntax
infixr 2 forth⁺-syntax back⁺-syntax
forth-syntax : ∀ x y → x ≤ y → Plus⇔ _≤_ x y
forth-syntax _ _ = forth
syntax forth-syntax x y x≤y = x ⇒⟨ x≤y ⟩∎ y ∎
back-syntax : ∀ x y → y ≤ x → Plus⇔ _≤_ x y
back-syntax _ _ = back
syntax back-syntax x y y≤x = x ⇐⟨ y≤x ⟩∎ y ∎
forth⁺-syntax : ∀ x {y z} → x ≤ y → Plus⇔ _≤_ y z → Plus⇔ _≤_ x z
forth⁺-syntax _ = forth⁺
syntax forth⁺-syntax x x≤y y⇔z = x ⇒⟨ x≤y ⟩ y⇔z
back⁺-syntax : ∀ x {y z} → y ≤ x → Plus⇔ _≤_ y z → Plus⇔ _≤_ x z
back⁺-syntax _ = back⁺
syntax back⁺-syntax x y≤x y⇔z = x ⇐⟨ y≤x ⟩ y⇔z
module _ {_≤_ : Rel A ℓ} {_≼_ : Rel B ℓ′} where
gmap : (f : A → B) (inj : _≤_ =[ f ]⇒ _≼_) → Plus⇔ _≤_ =[ f ]⇒ Plus⇔ _≼_
gmap f inj (forth r) = forth (inj r)
gmap f inj (back r) = back (inj r)
gmap f inj (forth⁺ r rel) = forth⁺ (inj r) (gmap f inj rel)
gmap f inj (back⁺ r rel) = back⁺ (inj r) (gmap f inj rel)
map : {_≤_ : Rel A ℓ} {_≼_ : Rel A ℓ′} (inj : _≤_ ⇒ _≼_) → Plus⇔ _≤_ ⇒ Plus⇔ _≼_
map = gmap id