eq-rel.agda

open import 1Lab.Prelude
open import 1Lab.Reflection
open import Order.Base

module eq-rel where

record is-equivalence-relation
  {ℓ} {A : Type ℓ} ℓ≈ (_≈_ : A → A → Type ℓ≈)
  : Type (ℓ ⊔ ℓ≈) where
  no-eta-equality
  field
    has-is-prop : ∀ x y → is-prop (x ≈ y)

    ≈-refl : ∀ {x} → x ≈ x
    ≈-sym : ∀ {x y} → x ≈ y → y ≈ x
    ≈-trans : ∀ {x y z} → y ≈ z → x ≈ y → x ≈ z

record Equivalence-relation-on {ℓ} (A : Type ℓ) ℓ≈ : Type (lsuc ℓ ⊔ lsuc ℓ≈) where
  field
    _≈_ : A → A → Type ℓ≈
    ≈-is-equivalence-relation : is-equivalence-relation ℓ≈ _≈_

  open is-equivalence-relation ≈-is-equivalence-relation public

instance
  H-Level-is-equivalence-relation
    : ∀ {ℓ} {A : Type ℓ} {ℓ≈} {_≈_ : A → A → Type ℓ≈} {n}
    → H-Level (is-equivalence-relation ℓ≈ _≈_) (suc n)
  H-Level-is-equivalence-relation {_≈_ = _≈_} = prop-instance λ x →
    let
      open is-equivalence-relation x
      instance
        hl : ∀ {k x y} → H-Level (_≈_ x y) (suc k)
        hl = prop-instance (has-is-prop _ _)
    in Iso→is-hlevel! 1 eqv x
    where
      unquoteDecl eqv = declare-record-iso eqv (quote is-equivalence-relation)

unquoteDecl Equivalence-relation-on-path =
  declare-record-path Equivalence-relation-on-path (quote Equivalence-relation-on)

private
  hlevel-≈ : ∀ {ℓ ℓ≈} {A : Type ℓ} (A≈ : Equivalence-relation-on A ℓ≈) {x y} → is-prop (A≈ .Equivalence-relation-on._≈_ x y)
  hlevel-≈ A≈ = A≈ .Equivalence-relation-on.has-is-prop _ _

instance
  open hlevel-projection

  hlevel-proj-≈ : hlevel-projection (quote Equivalence-relation-on._≈_)
  hlevel-proj-≈ .has-level = quote hlevel-≈
  hlevel-proj-≈ .get-level _ = pure (lit (nat 1))
  hlevel-proj-≈ .get-argument (_ ∷ _ ∷ _ ∷ o v∷ _) = pure o
  hlevel-proj-≈ .get-argument _ = typeError []

module _ {ℓ} (A : Type ℓ) ℓ≈ where
  _≤≈_ : (R₁ R₂ : Equivalence-relation-on A ℓ≈) → Type (ℓ ⊔ ℓ≈)
  record{ _≈_ = _≈₁_ } ≤≈ record{ _≈_ = _≈₂_ } =
    ∀ x y → x ≈₁ y → x ≈₂ y

  Equivalence-relations-on : Poset _ _
  Equivalence-relations-on .Poset.Ob = Equivalence-relation-on A ℓ≈
  Equivalence-relations-on .Poset._≤_ = _≤≈_
  Equivalence-relations-on .Poset.≤-thin = hlevel 1
  Equivalence-relations-on .Poset.≤-refl _ _ = id
  Equivalence-relations-on .Poset.≤-trans r≤s s≤t _ _ = s≤t _ _ ∘ r≤s _ _
  Equivalence-relations-on .Poset.≤-antisym r≤s s≤r = Equivalence-relation-on-path
    (ext λ x y → ua (prop-ext! (r≤s x y) (s≤r x y)))

  Equivalence-relation-on-is-set : is-set (Equivalence-relation-on A ℓ≈)
  Equivalence-relation-on-is-set = Poset.Ob-is-set Equivalence-relations-on

instance
  H-Level-equivalence-relation-on
    : ∀ {ℓ} {A : Type ℓ} {ℓ≈} {n}
    → H-Level (Equivalence-relation-on A ℓ≈) (2 + n)
  H-Level-equivalence-relation-on {A = A} {ℓ≈} = basic-instance 2 $
    Equivalence-relation-on-is-set A ℓ≈