```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

```