Equivalence-relation

------------------------------------------------------------------------
-- Equivalence relations
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Equality

module Equivalence-relation
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Prelude

open import Extensionality eq
open import H-level eq
open import H-level.Closure eq

private
  variable
    a r r₁ r₂         : Level
    A A₁ A₂ B B₁ B₂ C : Type a
    R R₁ R₂           : A → B → Type r

------------------------------------------------------------------------
-- The definition

-- The definition of "equivalence relation".

record Is-equivalence-relation
         {A : Type a} (R : A → A → Type r) : Type (a ⊔ r) where
  field
    reflexive  : ∀ {x} → R x x
    symmetric  : ∀ {x y} → R x y → R y x
    transitive : ∀ {x y z} → R x y → R y z → R x z

------------------------------------------------------------------------
-- Some examples of equivalence relations/equivalence relation
-- transformers

-- Equality is an equivalence relation.

≡-is-equivalence-relation :
  Is-equivalence-relation (_≡_ {A = A})
≡-is-equivalence-relation = λ where
  .Is-equivalence-relation.reflexive  → refl _
  .Is-equivalence-relation.symmetric  → sym
  .Is-equivalence-relation.transitive → trans

-- A trivial binary relation.

Trivial : A → B → Type r
Trivial _ _ = ↑ _ ⊤

-- Homogeneous instances of Trivial are equivalence relations.

Trivial-is-equivalence-relation :
  Is-equivalence-relation (Trivial {A = A} {r = r})
Trivial-is-equivalence-relation = _

-- Trivial is propositional.

Trivial-is-propositional :
  {x y : A} → Is-proposition (Trivial {r = r} x y)
Trivial-is-propositional = ↑-closure 1 (mono₁ 0 ⊤-contractible)

-- The superscript P used in the names of the definitions in this
-- section stands for "pointwise".

-- Lifts binary relations from B to A → B.

infix 0 _→ᴾ_

_→ᴾ_ :
  (A : Type a) →
  (B → C → Type r) →
  ((A → B) → (A → C) → Type (a ⊔ r))
(_ →ᴾ R) f g = ∀ x → R (f x) (g x)

-- _→ᴾ_ preserves equivalence relations.

→ᴾ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R →
  Is-equivalence-relation (A →ᴾ R)
→ᴾ-preserves-Is-equivalence-relation R-equiv = record
  { reflexive  = λ _ → reflexive
  ; symmetric  = λ f∼g x → symmetric (f∼g x)
  ; transitive = λ f∼g g∼h x → transitive (f∼g x) (g∼h x)
  }
  where
  open Is-equivalence-relation R-equiv

-- _→ᴾ_ preserves Is-proposition (assuming extensionality).

→ᴾ-preserves-Is-proposition :
  {A : Type a} (R : B → C → Type r) →
  Extensionality a r →
  (∀ {x y} → Is-proposition (R x y)) →
  ∀ {f g} → Is-proposition ((A →ᴾ R) f g)
→ᴾ-preserves-Is-proposition _ ext R-prop =
  Π-closure ext 1 λ _ →
  R-prop

-- Lifts binary relations from A and B to A ⊎ B.

infixr 1 _⊎ᴾ_

_⊎ᴾ_ :
  (A₁ → A₂ → Type r) →
  (B₁ → B₂ → Type r) →
  (A₁ ⊎ B₁ → A₂ ⊎ B₂ → Type r)
(P ⊎ᴾ Q) (inj₁ x) (inj₁ y) = P x y
(P ⊎ᴾ Q) (inj₂ x) (inj₂ y) = Q x y
(P ⊎ᴾ Q) _        _        = ⊥

-- _⊎ᴾ_ preserves Is-equivalence-relation.

⊎ᴾ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R₁ →
  Is-equivalence-relation R₂ →
  Is-equivalence-relation (R₁ ⊎ᴾ R₂)
⊎ᴾ-preserves-Is-equivalence-relation R₁-equiv R₂-equiv = record
  { reflexive  = λ { {x = inj₁ _} → reflexive R₁-equiv
                   ; {x = inj₂ _} → reflexive R₂-equiv
                   }
  ; symmetric  = λ { {x = inj₁ _} {y = inj₁ _} → symmetric R₁-equiv
                   ; {x = inj₂ _} {y = inj₂ _} → symmetric R₂-equiv
                   ; {x = inj₁ _} {y = inj₂ _} ()
                   ; {x = inj₂ _} {y = inj₁ _} ()
                   }
  ; transitive = λ
     { {x = inj₁ _} {y = inj₁ _} {z = inj₁ _} → transitive R₁-equiv
     ; {x = inj₂ _} {y = inj₂ _} {z = inj₂ _} → transitive R₂-equiv

     ; {x = inj₁ _} {y = inj₂ _} ()
     ; {x = inj₂ _} {y = inj₁ _} ()
     ; {y = inj₁ _} {z = inj₂ _} _ ()
     ; {y = inj₂ _} {z = inj₁ _} _ ()
     }
  }
  where
  open Is-equivalence-relation

-- _⊎ᴾ_ preserves Is-proposition.

⊎ᴾ-preserves-Is-proposition :
  (∀ {x y} → Is-proposition (R₁ x y)) →
  (∀ {x y} → Is-proposition (R₂ x y)) →
  ∀ {x y} → Is-proposition ((R₁ ⊎ᴾ R₂) x y)
⊎ᴾ-preserves-Is-proposition = λ where
  R₁-prop R₂-prop {inj₁ _} {inj₁ _} → R₁-prop
  R₁-prop R₂-prop {inj₁ _} {inj₂ _} → ⊥-propositional
  R₁-prop R₂-prop {inj₂ _} {inj₁ _} → ⊥-propositional
  R₁-prop R₂-prop {inj₂ _} {inj₂ _} → R₂-prop

-- Lifts a binary relation from A to Maybe A.

Maybeᴾ :
  (A → B → Type r) →
  (Maybe A → Maybe B → Type r)
Maybeᴾ R = Trivial ⊎ᴾ R

-- Maybeᴾ preserves Is-equivalence-relation.

Maybeᴾ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R →
  Is-equivalence-relation (Maybeᴾ R)
Maybeᴾ-preserves-Is-equivalence-relation =
  ⊎ᴾ-preserves-Is-equivalence-relation Trivial-is-equivalence-relation

-- Maybeᴾ preserves Is-proposition.

Maybeᴾ-preserves-Is-proposition :
  (∀ {x y} → Is-proposition (R x y)) →
  ∀ {x y} → Is-proposition (Maybeᴾ R x y)
Maybeᴾ-preserves-Is-proposition =
  ⊎ᴾ-preserves-Is-proposition λ {x} →
  Trivial-is-propositional {x = x}

-- Lifts binary relations from A and B to A × B.

infixr 2 _×ᴾ_

_×ᴾ_ :
  (A₁ → B₁ → Type r₁) →
  (A₂ → B₂ → Type r₂) →
  (A₁ × A₂ → B₁ × B₂ → Type (r₁ ⊔ r₂))
(P ×ᴾ Q) (x₁ , x₂) (y₁ , y₂) = P x₁ y₁ × Q x₂ y₂

-- _×ᴾ_ preserves Is-equivalence-relation.

×ᴾ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R₁ →
  Is-equivalence-relation R₂ →
  Is-equivalence-relation (R₁ ×ᴾ R₂)
×ᴾ-preserves-Is-equivalence-relation R₁-equiv R₂-equiv = λ where
    .Is-equivalence-relation.reflexive →
      E₁.reflexive , E₂.reflexive
    .Is-equivalence-relation.symmetric →
      Σ-map E₁.symmetric E₂.symmetric
    .Is-equivalence-relation.transitive →
      Σ-zip E₁.transitive E₂.transitive
  where
  module E₁ = Is-equivalence-relation R₁-equiv
  module E₂ = Is-equivalence-relation R₂-equiv

-- _×ᴾ_ preserves Is-proposition.

×ᴾ-preserves-Is-proposition :
  (∀ {x y} → Is-proposition (R₁ x y)) →
  (∀ {x y} → Is-proposition (R₂ x y)) →
  ∀ {x y} → Is-proposition ((R₁ ×ᴾ R₂) x y)
×ᴾ-preserves-Is-proposition R₁-prop R₂-prop =
  ×-closure 1 R₁-prop R₂-prop

-- Lifts a binary relation from A to List A.

Listᴾ :
  (A → B → Type r) →
  (List A → List B → Type r)
Listᴾ R []       []       = ↑ _ ⊤
Listᴾ R (x ∷ xs) (y ∷ ys) = R x y × Listᴾ R xs ys
Listᴾ R _        _        = ⊥

-- Listᴾ preserves reflexivity.

Listᴾ-preserves-reflexivity :
  (∀ {x} → R x x) →
  ∀ {xs} → Listᴾ R xs xs
Listᴾ-preserves-reflexivity = λ where
  r {xs = []}    → _
  r {xs = _ ∷ _} → r , Listᴾ-preserves-reflexivity r

-- Listᴾ preserves symmetry.

Listᴾ-preserves-symmetry :
  (∀ {x y} → R x y → R y x) →
  ∀ {xs ys} → Listᴾ R xs ys → Listᴾ R ys xs
Listᴾ-preserves-symmetry = λ where
  s {xs = []}    {ys = []}    _        → _
  s {xs = _ ∷ _} {ys = _ ∷ _} (p , ps) →
    s p , Listᴾ-preserves-symmetry s ps

-- Listᴾ preserves transitivity.

Listᴾ-preserves-transitivity :
  (∀ {x y z} → R x y → R y z → R x z) →
  ∀ {xs ys zs} → Listᴾ R xs ys → Listᴾ R ys zs → Listᴾ R xs zs
Listᴾ-preserves-transitivity = λ where
  t {xs = []}    {ys = []}    {zs = []}    _        _        → _
  t {xs = _ ∷ _} {ys = _ ∷ _} {zs = _ ∷ _} (p , ps) (q , qs) →
    t p q , Listᴾ-preserves-transitivity t ps qs

-- Listᴾ preserves Is-equivalence-relation.

Listᴾ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R →
  Is-equivalence-relation (Listᴾ R)
Listᴾ-preserves-Is-equivalence-relation R-equiv = λ where
    .reflexive  → Listᴾ-preserves-reflexivity  reflexive
    .symmetric  → Listᴾ-preserves-symmetry     symmetric
    .transitive → Listᴾ-preserves-transitivity transitive
  where
  open Is-equivalence-relation R-equiv

-- Listᴾ preserves Is-proposition.

Listᴾ-preserves-Is-proposition :
  (∀ {x y} → Is-proposition (R x y)) →
  ∀ {xs ys} → Is-proposition (Listᴾ R xs ys)
Listᴾ-preserves-Is-proposition {R} R-prop = prop _ _
  where
  prop : ∀ xs ys → Is-proposition (Listᴾ R xs ys)
  prop []       []       _        _        = refl _
  prop (_ ∷ xs) (_ ∷ ys) (p , ps) (q , qs) =
    cong₂ _,_ (R-prop p q) (prop xs ys ps qs)