------------------------------------------------------------------------
-- 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} 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)