{-# OPTIONS --cubical-compatible #-}
module Class.Setoid.Core where

open import Class.Core
open import Class.Prelude

record ISetoid (A : Type ℓ) : Typeω where
  infix  _≈_ _≉_
  field
    {relℓ} : Level
    _≈_ : Rel A relℓ

  _≉_ : Rel A relℓ
  x ≉ y = ¬ (x ≈ y)

  module Alg≈ = Alg _≈_
open ISetoid ⦃...⦄ public

record SetoidLaws (A : Type ℓ) ⦃ _ : ISetoid A ⦄ : Typeω where
  field isEquivalence : IsEquivalence _≈_

  open IsEquivalence isEquivalence public
    renaming (refl to ≈-refl; sym to ≈-sym; trans to ≈-trans; reflexive to ≈-reflexive)

  mkSetoid : Setoid ℓ relℓ
  mkSetoid = record {Carrier = A; _≈_ = _≈_; isEquivalence = isEquivalence}

  import Relation.Binary.Reasoning.Setoid as BinSetoid
  module ≈-Reasoning = BinSetoid mkSetoid
open SetoidLaws ⦃...⦄ public

_⟶_ : (A : Type ℓ) (B : Type ℓ′)
    → ⦃ _ : ISetoid A ⦄ → ⦃ SetoidLaws A ⦄
    → ⦃ _ : ISetoid B ⦄ → ⦃ SetoidLaws B ⦄
    → Type _
A ⟶ B = Func (mkSetoid {A = A}) (mkSetoid {A = B})
  where open import Function.Bundles

mkISetoid≡ : ISetoid A
mkISetoid≡ = λ where
  .relℓ → _
  ._≈_ → _≡_

mkSetoidLaws≡ : SetoidLaws A ⦃ mkISetoid≡ ⦄
mkSetoidLaws≡ .isEquivalence = PropEq.isEquivalence
  where import Relation.Binary.PropositionalEquality as PropEq