{-# OPTIONS --without-K --safe #-}

-- was not ported from old function hierarchy

module Function.Construct.Setoid where

  open import Function.Bundles using (Func; _⟨$⟩_)
  import Function.Construct.Composition as Comp
  open import Level using (Level)
  open import Relation.Binary.Bundles using (Setoid)


  private
    variable
      a₁ a₂ b₁ b₂ c₁ c₂ : Level

  setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
  setoid From To = record
    { Carrier = Func From To
    ; _≈_ = λ f g → ∀ {x} → f ⟨$⟩ x To.≈ g ⟨$⟩ x
    ; isEquivalence = record
      { refl = To.refl
      ; sym = λ f≈g → To.sym f≈g
      ; trans = λ f≈g g≈h → To.trans f≈g g≈h
      }
    }
    where
      module To = Setoid To

  -- This doesn't really belong here, it should be in Function.Construct.Composition but that's in stdlib
  -- so will need to be contributed to there first.
  infixr  _∙_
  _∙_ : {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} {C : Setoid c₁ c₂} → Func B C → Func A B → Func A C
  f ∙ g = Comp.function g f