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