module Quotient where

open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

subst-dummy : ∀ {c ℓ}{A : Set c}{B : Set ℓ}
              {a b : A}(p : a ≡ b)(x : B) → P.subst {A = A} (λ _ → B) p x ≡ x
subst-dummy P.refl x = P.refl

private
  module Dummy where

    data Quotient {c ℓ} (A : Setoid c ℓ) : Set (c ⊔ ℓ) where
      box : (x : Setoid.Carrier A) → Quotient A

  open Dummy public using (Quotient)

  module Dummy₂ {c ℓ} {A : Setoid c ℓ} where

    open Setoid A

    [_] : Carrier → Quotient A
    [_] = Dummy.box

    postulate
      [_]-cong : ∀ {a b} → a ≈ b → _≡_ {A = Quotient A} [ a ] [ b ]

    elim : ∀ {p} (P : Quotient A → Set p) 
           (f : (x : Carrier) → P [ x ]) →
           (∀ {x y} (x≈y : x ≈ y) → P.subst P ([ x≈y ]-cong) (f x) ≡ f y) →
           ∀ c → P c
    elim P f _ (Dummy.box x) = f x


    rec : ∀ {p} (P : Set p) 
             (f : (x : Carrier) → P) →
             (∀ {x y} (x≈y : x ≈ y) → f x ≡ f y) →
             Quotient A → P
    rec P f cong c = elim (λ _ → P) f (λ x≈y → P.trans (subst-dummy [ x≈y ]-cong  (f _)) (cong x≈y)) c

open Dummy₂ public