import logic.relator

variables {α : Sort*} {β : Sort*}

open function

namespace setoid

lemma ext {α : Sort*} :

∀{s t : setoid α}, (∀a b, @setoid.r α s a b ↔ @setoid.r α t a b) → s = t

| ⟨r, _⟩ ⟨p, _⟩ eq :=

have r = p, from funext $ assume a, funext $ assume b, propext $ eq a b,

by subst this

end setoid

namespace quot

variables {ra : α → α → Prop} {rb : β → β → Prop} {φ : quot ra → quot rb → Sort*}

local notation (name := mk) `⟦`:max a `⟧` := quot.mk _ a

instance (r : α → α → Prop) [inhabited α] : inhabited (quot r) := ⟨⟦default⟧⟩

instance [subsingleton α] : subsingleton (quot ra) :=

⟨λ x, quot.induction_on x (λ y, quot.ind (λ b, congr_arg _ (subsingleton.elim _ _)))⟩

protected def hrec_on₂ (qa : quot ra) (qb : quot rb) (f : Π a b, φ ⟦a⟧ ⟦b⟧)

(ca : ∀ {b a₁ a₂}, ra a₁ a₂ → f a₁ b == f a₂ b)

(cb : ∀ {a b₁ b₂}, rb b₁ b₂ → f a b₁ == f a b₂) : φ qa qb :=

quot.hrec_on qa (λ a, quot.hrec_on qb (f a) (λ b₁ b₂ pb, cb pb)) $ λ a₁ a₂ pa,

quot.induction_on qb $ λ b,

calc @quot.hrec_on _ _ (φ _) ⟦b⟧ (f a₁) (@cb _)

== f a₁ b : by simp [heq_self_iff_true]

... == f a₂ b : ca pa

... == @quot.hrec_on _ _ (φ _) ⟦b⟧ (f a₂) (@cb _) : by simp [heq_self_iff_true]

protected def map (f : α → β) (h : (ra ⇒ rb) f f) : quot ra → quot rb :=

quot.lift (λ x, ⟦f x⟧) $ assume x y (h₁ : ra x y), quot.sound $ h h₁

protected def map_right {ra' : α → α → Prop} (h : ∀a₁ a₂, ra a₁ a₂ → ra' a₁ a₂) :

quot ra → quot ra' :=

quot.map id h

def factor {α : Type*} (r s : α → α → Prop) (h : ∀ x y, r x y → s x y) :

quot r → quot s :=

quot.lift (quot.mk s) (λ x y rxy, quot.sound (h x y rxy))

lemma factor_mk_eq {α : Type*} (r s : α → α → Prop) (h : ∀ x y, r x y → s x y) :

factor r s h ∘ quot.mk _ = quot.mk _ := rfl

variables {γ : Sort*} {r : α → α → Prop} {s : β → β → Prop}

lemma lift_mk (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) (a : α) :

quot.lift f h (quot.mk r a) = f a := rfl

lemma lift_on_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :

quot.lift_on (quot.mk r a) f h = f a := rfl

@[simp] lemma surjective_lift {f : α → γ} (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :

surjective (lift f h) ↔ surjective f :=

⟨λ hf, hf.comp quot.exists_rep, λ hf y, let ⟨x, hx⟩ := hf y in ⟨quot.mk _ x, hx⟩⟩

protected def lift₂

(f : α → β → γ)

(hr : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂)

(hs : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b)

(q₁ : quot r) (q₂ : quot s) : γ :=

quot.lift (λ a, quot.lift (f a) (hr a))

(λ a₁ a₂ ha, funext (λ q, quot.induction_on q (λ b, hs a₁ a₂ b ha)))

q₁ q₂

lemma lift₂_mk (f : α → β → γ)

(hr : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂)

(hs : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b) (a : α) (b : β) :

quot.lift₂ f hr hs (quot.mk r a) (quot.mk s b) = f a b := rfl

protected def lift_on₂ (p : quot r) (q : quot s) (f : α → β → γ)

(hr : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂)

(hs : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b) : γ := quot.lift₂ f hr hs p q

lemma lift_on₂_mk (a : α) (b : β) (f : α → β → γ)

(hr : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂)

(hs : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b) :

quot.lift_on₂ (quot.mk r a) (quot.mk s b) f hr hs = f a b := rfl

variables {t : γ → γ → Prop}

protected def map₂ (f : α → β → γ)

(hr : ∀ a b₁ b₂, s b₁ b₂ → t (f a b₁) (f a b₂))

(hs : ∀ a₁ a₂ b, r a₁ a₂ → t (f a₁ b) (f a₂ b))

(q₁ : quot r) (q₂ : quot s) : quot t :=

quot.lift₂ (λ a b, quot.mk t $ f a b) (λ a b₁ b₂ hb, quot.sound (hr a b₁ b₂ hb))

(λ a₁ a₂ b ha, quot.sound (hs a₁ a₂ b ha)) q₁ q₂

lemma map₂_mk (f : α → β → γ)

(hr : ∀ a b₁ b₂, s b₁ b₂ → t (f a b₁) (f a b₂))

(hs : ∀ a₁ a₂ b, r a₁ a₂ → t (f a₁ b) (f a₂ b))

(a : α) (b : β) : quot.map₂ f hr hs (quot.mk r a) (quot.mk s b) = quot.mk t (f a b) := rfl

protected def rec_on_subsingleton₂ {φ : quot r → quot s → Sort*}

[h : ∀ a b, subsingleton (φ ⟦a⟧ ⟦b⟧)] (q₁ : quot r) (q₂ : quot s) (f : Π a b, φ ⟦a⟧ ⟦b⟧) :

φ q₁ q₂ :=

@quot.rec_on_subsingleton _ r (λ q, φ q q₂) (λ a, quot.ind (h a) q₂) q₁ $

λ a, quot.rec_on_subsingleton q₂ $ λ b, f a b

protected lemma induction_on₂

{δ : quot r → quot s → Prop} (q₁ : quot r) (q₂ : quot s)

(h : ∀ a b, δ (quot.mk r a) (quot.mk s b)) : δ q₁ q₂ :=

quot.ind (λ a₁, quot.ind (λ a₂, h a₁ a₂) q₂) q₁

protected lemma induction_on₃

{δ : quot r → quot s → quot t → Prop} (q₁ : quot r) (q₂ : quot s) (q₃ : quot t)

(h : ∀ a b c, δ (quot.mk r a) (quot.mk s b) (quot.mk t c)) : δ q₁ q₂ q₃ :=

quot.ind (λ a₁, quot.ind (λ a₂, quot.ind (λ a₃, h a₁ a₂ a₃) q₃) q₂) q₁

instance (r : α → α → Prop) (f : α → Prop) (h : ∀ a b, r a b → f a = f b) [hf : decidable_pred f] :

decidable_pred (quot.lift f h) :=

λ q, quot.rec_on_subsingleton q hf

instance (r : α → α → Prop) (s : β → β → Prop) (f : α → β → Prop)

(ha : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂) (hb : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b)

[hf : Π a, decidable_pred (f a)] (q₁ : quot r) :

decidable_pred (quot.lift₂ f ha hb q₁) :=

λ q₂, quot.rec_on_subsingleton₂ q₁ q₂ hf

instance (r : α → α → Prop) (q : quot r) (f : α → Prop) (h : ∀ a b, r a b → f a = f b)

[decidable_pred f] :

decidable (quot.lift_on q f h) :=

quot.lift.decidable_pred _ _ _ _

instance (r : α → α → Prop) (s : β → β → Prop) (q₁ : quot r) (q₂ : quot s) (f : α → β → Prop)

(ha : ∀ a b₁ b₂, s b₁ b₂ → f a b₁ = f a b₂) (hb : ∀ a₁ a₂ b, r a₁ a₂ → f a₁ b = f a₂ b)

[Π a, decidable_pred (f a)] :

decidable (quot.lift_on₂ q₁ q₂ f ha hb) :=

quot.lift₂.decidable_pred _ _ _ _ _ _ _

end quot

namespace quotient

variables [sa : setoid α] [sb : setoid β]

variables {φ : quotient sa → quotient sb → Sort*}

instance (s : setoid α) [inhabited α] : inhabited (quotient s) := ⟨⟦default⟧⟩

instance (s : setoid α) [subsingleton α] : subsingleton (quotient s) :=

quot.subsingleton

instance {α : Type*} [setoid α] : is_equiv α (≈) :=

{ refl := setoid.refl,

symm := λ a b, setoid.symm,

trans := λ a b c, setoid.trans }

protected def hrec_on₂ (qa : quotient sa) (qb : quotient sb) (f : Π a b, φ ⟦a⟧ ⟦b⟧)

(c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ == f a₂ b₂) : φ qa qb :=

quot.hrec_on₂ qa qb f

(λ _ _ _ p, c _ _ _ _ p (setoid.refl _))

(λ _ _ _ p, c _ _ _ _ (setoid.refl _) p)

protected def map (f : α → β) (h : ((≈) ⇒ (≈)) f f) : quotient sa → quotient sb :=

quot.map f h

@[simp] lemma map_mk (f : α → β) (h : ((≈) ⇒ (≈)) f f) (x : α) :

quotient.map f h (⟦x⟧ : quotient sa) = (⟦f x⟧ : quotient sb) :=

rfl

variables {γ : Sort*} [sc : setoid γ]

protected def map₂ (f : α → β → γ) (h : ((≈) ⇒ (≈) ⇒ (≈)) f f) :

quotient sa → quotient sb → quotient sc :=

quotient.lift₂ (λ x y, ⟦f x y⟧) (λ x₁ y₁ x₂ y₂ h₁ h₂, quot.sound $ h h₁ h₂)

@[simp] lemma map₂_mk (f : α → β → γ) (h : ((≈) ⇒ (≈) ⇒ (≈)) f f) (x : α) (y : β) :

quotient.map₂ f h (⟦x⟧ : quotient sa) (⟦y⟧ : quotient sb) = (⟦f x y⟧ : quotient sc) := rfl

include sa

instance (f : α → Prop) (h : ∀ a b, a ≈ b → f a = f b) [decidable_pred f] :

decidable_pred (quotient.lift f h) :=

quot.lift.decidable_pred _ _ _

include sb

instance (f : α → β → Prop) (h : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂)

[hf : Π a, decidable_pred (f a)] (q₁ : quotient sa) :

decidable_pred (quotient.lift₂ f h q₁) :=

λ q₂, quotient.rec_on_subsingleton₂ q₁ q₂ hf

omit sb

instance (q : quotient sa) (f : α → Prop) (h : ∀ a b, a ≈ b → f a = f b) [decidable_pred f] :

decidable (quotient.lift_on q f h) :=

quotient.lift.decidable_pred _ _ _

instance (q₁ : quotient sa) (q₂ : quotient sb) (f : α → β → Prop)

(h : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) [Π a, decidable_pred (f a)] :

decidable (quotient.lift_on₂ q₁ q₂ f h) :=

quotient.lift₂.decidable_pred _ _ _ _

end quotient

lemma quot.eq {α : Type*} {r : α → α → Prop} {x y : α} :

quot.mk r x = quot.mk r y ↔ eqv_gen r x y :=

⟨quot.exact r, quot.eqv_gen_sound⟩

@[simp] theorem quotient.eq [r : setoid α] {x y : α} : ⟦x⟧ = ⟦y⟧ ↔ x ≈ y :=

⟨quotient.exact, quotient.sound⟩

theorem forall_quotient_iff {α : Type*} [r : setoid α] {p : quotient r → Prop} :

(∀a:quotient r, p a) ↔ (∀a:α, p ⟦a⟧) :=

⟨assume h x, h _, assume h a, a.induction_on h⟩

@[simp] lemma quotient.lift_mk [s : setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b)

(x : α) :

quotient.lift f h (quotient.mk x) = f x := rfl

@[simp] lemma quotient.lift_comp_mk [setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) :

quotient.lift f h ∘ quotient.mk = f :=

rfl

@[simp] lemma quotient.lift₂_mk {α : Sort*} {β : Sort*} {γ : Sort*} [setoid α] [setoid β]

(f : α → β → γ)

(h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂)

(a : α) (b : β) :

quotient.lift₂ f h (quotient.mk a) (quotient.mk b) = f a b := rfl

@[simp] lemma quotient.lift_on_mk [s : setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b)

(x : α) :

quotient.lift_on (quotient.mk x) f h = f x := rfl

@[simp] theorem quotient.lift_on₂_mk {α : Sort*} {β : Sort*} [setoid α] (f : α → α → β)

(h : ∀ (a₁ a₂ b₁ b₂ : α), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (x y : α) :

quotient.lift_on₂ (quotient.mk x) (quotient.mk y) f h = f x y := rfl

lemma surjective_quot_mk (r : α → α → Prop) : surjective (quot.mk r) := quot.exists_rep

lemma surjective_quotient_mk (α : Sort*) [s : setoid α] :

surjective (quotient.mk : α → quotient s) :=

quot.exists_rep

noncomputable def quot.out {r : α → α → Prop} (q : quot r) : α :=

classical.some (quot.exists_rep q)

meta def quot.unquot {r : α → α → Prop} : quot r → α := unchecked_cast

@[simp] theorem quot.out_eq {r : α → α → Prop} (q : quot r) : quot.mk r q.out = q :=

classical.some_spec (quot.exists_rep q)

noncomputable def quotient.out [s : setoid α] : quotient s → α := quot.out

@[simp] theorem quotient.out_eq [s : setoid α] (q : quotient s) : ⟦q.out⟧ = q := q.out_eq

theorem quotient.mk_out [s : setoid α] (a : α) : ⟦a⟧.out ≈ a :=

quotient.exact (quotient.out_eq _)

lemma quotient.mk_eq_iff_out [s : setoid α] {x : α} {y : quotient s} :

⟦x⟧ = y ↔ x ≈ quotient.out y :=

refine iff.trans _ quotient.eq,

rw quotient.out_eq y,

lemma quotient.eq_mk_iff_out [s : setoid α] {x : quotient s} {y : α} :

x = ⟦y⟧ ↔ quotient.out x ≈ y :=

refine iff.trans _ quotient.eq,

rw quotient.out_eq x,

@[simp] lemma quotient.out_equiv_out {s : setoid α} {x y : quotient s} :

x.out ≈ y.out ↔ x = y :=

by rw [← quotient.eq_mk_iff_out, quotient.out_eq]

lemma quotient.out_injective {s : setoid α} : injective (@quotient.out α s) :=

λ a b h, quotient.out_equiv_out.1 $ h ▸ setoid.refl _

@[simp] lemma quotient.out_inj {s : setoid α} {x y : quotient s} :

x.out = y.out ↔ x = y :=

⟨λ h, quotient.out_injective h, λ h, h ▸ rfl⟩

section pi

instance pi_setoid {ι : Sort*} {α : ι → Sort*} [∀ i, setoid (α i)] : setoid (Π i, α i) :=

{ r := λ a b, ∀ i, a i ≈ b i,

iseqv := ⟨

λ a i, setoid.refl _,

λ a b h i, setoid.symm (h _),

λ a b c h₁ h₂ i, setoid.trans (h₁ _) (h₂ _)⟩ }

noncomputable def quotient.choice {ι : Type*} {α : ι → Type*} [S : Π i, setoid (α i)]

(f : Π i, quotient (S i)) : @quotient (Π i, α i) (by apply_instance) :=

⟦λ i, (f i).out⟧

@[simp] theorem quotient.choice_eq {ι : Type*} {α : ι → Type*} [Π i, setoid (α i)]

(f : Π i, α i) : quotient.choice (λ i, ⟦f i⟧) = ⟦f⟧ :=

quotient.sound $ λ i, quotient.mk_out _

@[elab_as_eliminator] lemma quotient.induction_on_pi

{ι : Type*} {α : ι → Sort*} [s : ∀ i, setoid (α i)]

{p : (Π i, quotient (s i)) → Prop} (f : Π i, quotient (s i))

(h : ∀ a : Π i, α i, p (λ i, ⟦a i⟧)) : p f :=

rw ← (funext (λ i, quotient.out_eq (f i)) : (λ i, ⟦(f i).out⟧) = f),

apply h,

end pi

lemma nonempty_quotient_iff (s : setoid α) : nonempty (quotient s) ↔ nonempty α :=

⟨assume ⟨a⟩, quotient.induction_on a nonempty.intro, assume ⟨a⟩, ⟨⟦a⟧⟩⟩

theorem true_equivalence : @equivalence α (λ _ _, true) :=

⟨λ _, trivial, λ _ _ _, trivial, λ _ _ _ _ _, trivial⟩

def true_setoid : setoid α :=

⟨_, true_equivalence⟩

def {u} trunc (α : Sort u) : Sort u := @quotient α true_setoid

namespace trunc

def mk (a : α) : trunc α := quot.mk _ a

instance [inhabited α] : inhabited (trunc α) := ⟨mk default⟩

def lift (f : α → β) (c : ∀ a b : α, f a = f b) : trunc α → β :=

quot.lift f (λ a b _, c a b)

theorem ind {β : trunc α → Prop} : (∀ a : α, β (mk a)) → ∀ q : trunc α, β q := quot.ind

protected theorem lift_mk (f : α → β) (c) (a : α) : lift f c (mk a) = f a := rfl

protected def lift_on (q : trunc α) (f : α → β)

(c : ∀ a b : α, f a = f b) : β := lift f c q

protected theorem induction_on {β : trunc α → Prop} (q : trunc α)

(h : ∀ a, β (mk a)) : β q := ind h q

theorem exists_rep (q : trunc α) : ∃ a : α, mk a = q := quot.exists_rep q

protected theorem induction_on₂ {C : trunc α → trunc β → Prop} (q₁ : trunc α) (q₂ : trunc β)

(h : ∀ a b, C (mk a) (mk b)) : C q₁ q₂ :=

trunc.induction_on q₁ $ λ a₁, trunc.induction_on q₂ (h a₁)

protected theorem eq (a b : trunc α) : a = b :=

trunc.induction_on₂ a b (λ x y, quot.sound trivial)

instance : subsingleton (trunc α) := ⟨trunc.eq⟩

def bind (q : trunc α) (f : α → trunc β) : trunc β :=

trunc.lift_on q f (λ a b, trunc.eq _ _)

def map (f : α → β) (q : trunc α) : trunc β := bind q (trunc.mk ∘ f)

instance : monad trunc :=

{ pure := @trunc.mk,

bind := @trunc.bind }

instance : is_lawful_monad trunc :=

{ id_map := λ α q, trunc.eq _ _,

pure_bind := λ α β q f, rfl,

bind_assoc := λ α β γ x f g, trunc.eq _ _ }

variable {C : trunc α → Sort*}

protected def rec

(f : Π a, C (mk a)) (h : ∀ (a b : α), (eq.rec (f a) (trunc.eq (mk a) (mk b)) : C (mk b)) = f b)

(q : trunc α) : C q :=

quot.rec f (λ a b _, h a b) q

protected def rec_on (q : trunc α) (f : Π a, C (mk a))

(h : ∀ (a b : α), (eq.rec (f a) (trunc.eq (mk a) (mk b)) : C (mk b)) = f b) : C q :=

trunc.rec f h q

protected def rec_on_subsingleton

[∀ a, subsingleton (C (mk a))] (q : trunc α) (f : Π a, C (mk a)) : C q :=

trunc.rec f (λ a b, subsingleton.elim _ (f b)) q

noncomputable def out : trunc α → α := quot.out

@[simp] theorem out_eq (q : trunc α) : mk q.out = q := trunc.eq _ _

protected theorem nonempty (q : trunc α) : nonempty α :=

nonempty_of_exists q.exists_rep

end trunc

namespace quotient

variables {γ : Sort*} {φ : Sort*}

{s₁ : setoid α} {s₂ : setoid β} {s₃ : setoid γ}

protected def mk' (a : α) : quotient s₁ := quot.mk s₁.1 a

lemma surjective_quotient_mk' : surjective (quotient.mk' : α → quotient s₁) :=

quot.exists_rep

protected def lift_on' (q : quotient s₁) (f : α → φ)

(h : ∀ a b, @setoid.r α s₁ a b → f a = f b) : φ := quotient.lift_on q f h

protected lemma lift_on'_mk' (f : α → φ) (h) (x : α) :

quotient.lift_on' (@quotient.mk' _ s₁ x) f h = f x := rfl

@[simp] lemma surjective_lift_on' {f : α → φ} (h : ∀ a b, @setoid.r α s₁ a b → f a = f b) :

surjective (λ x, quotient.lift_on' x f h) ↔ surjective f :=

quot.surjective_lift _

protected def lift_on₂' (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α → β → γ)

(h : ∀ a₁ a₂ b₁ b₂, @setoid.r α s₁ a₁ b₁ → @setoid.r β s₂ a₂ b₂ → f a₁ a₂ = f b₁ b₂) : γ :=

quotient.lift_on₂ q₁ q₂ f h

protected lemma lift_on₂'_mk' (f : α → β → γ) (h) (a : α) (b : β) :

quotient.lift_on₂' (@quotient.mk' _ s₁ a) (@quotient.mk' _ s₂ b) f h = f a b := rfl

protected lemma ind' {p : quotient s₁ → Prop}

(h : ∀ a, p (quotient.mk' a)) (q : quotient s₁) : p q :=

quotient.ind h q

protected lemma ind₂' {p : quotient s₁ → quotient s₂ → Prop}

(h : ∀ a₁ a₂, p (quotient.mk' a₁) (quotient.mk' a₂))

(q₁ : quotient s₁) (q₂ : quotient s₂) : p q₁ q₂ :=

quotient.ind₂ h q₁ q₂

protected lemma induction_on' {p : quotient s₁ → Prop} (q : quotient s₁)

(h : ∀ a, p (quotient.mk' a)) : p q := quotient.induction_on q h

protected lemma induction_on₂' {p : quotient s₁ → quotient s₂ → Prop} (q₁ : quotient s₁)

(q₂ : quotient s₂) (h : ∀ a₁ a₂, p (quotient.mk' a₁) (quotient.mk' a₂)) : p q₁ q₂ :=

quotient.induction_on₂ q₁ q₂ h

protected lemma induction_on₃' {p : quotient s₁ → quotient s₂ → quotient s₃ → Prop}

(q₁ : quotient s₁) (q₂ : quotient s₂) (q₃ : quotient s₃)

(h : ∀ a₁ a₂ a₃, p (quotient.mk' a₁) (quotient.mk' a₂) (quotient.mk' a₃)) : p q₁ q₂ q₃ :=

quotient.induction_on₃ q₁ q₂ q₃ h

protected def rec_on_subsingleton' {φ : quotient s₁ → Sort*}

[h : ∀ a, subsingleton (φ ⟦a⟧)] (q : quotient s₁) (f : Π a, φ (quotient.mk' a)) : φ q :=

quotient.rec_on_subsingleton q f

protected def rec_on_subsingleton₂'

{φ : quotient s₁ → quotient s₂ → Sort*} [h : ∀ a b, subsingleton (φ ⟦a⟧ ⟦b⟧)]

(q₁ : quotient s₁) (q₂ : quotient s₂) (f : Π a₁ a₂, φ (quotient.mk' a₁) (quotient.mk' a₂)) :

φ q₁ q₂ :=

quotient.rec_on_subsingleton₂ q₁ q₂ f

protected def hrec_on' {φ : quotient s₁ → Sort*} (qa : quotient s₁) (f : Π a, φ (quotient.mk' a))

(c : ∀ a₁ a₂, a₁ ≈ a₂ → f a₁ == f a₂) : φ qa :=

quot.hrec_on qa f c

@[simp] lemma hrec_on'_mk' {φ : quotient s₁ → Sort*} (f : Π a, φ (quotient.mk' a))

(c : ∀ a₁ a₂, a₁ ≈ a₂ → f a₁ == f a₂) (x : α) :

(quotient.mk' x).hrec_on' f c = f x :=

rfl

protected def hrec_on₂' {φ : quotient s₁ → quotient s₂ → Sort*} (qa : quotient s₁)

(qb : quotient s₂) (f : ∀ a b, φ (quotient.mk' a) (quotient.mk' b))

(c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ == f a₂ b₂) : φ qa qb :=

quotient.hrec_on₂ qa qb f c

@[simp] lemma hrec_on₂'_mk' {φ : quotient s₁ → quotient s₂ → Sort*}

(f : ∀ a b, φ (quotient.mk' a) (quotient.mk' b))

(c : ∀ a₁ b₁ a₂ b₂, a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ == f a₂ b₂) (x : α) (qb : quotient s₂) :

(quotient.mk' x).hrec_on₂' qb f c = qb.hrec_on' (f x) (λ b₁ b₂, c _ _ _ _ (setoid.refl _)) :=

rfl

protected def map' (f : α → β) (h : (s₁.r ⇒ s₂.r) f f) :

quotient s₁ → quotient s₂ :=

quot.map f h

@[simp] lemma map'_mk' (f : α → β) (h) (x : α) :

(quotient.mk' x : quotient s₁).map' f h = (quotient.mk' (f x) : quotient s₂) :=

rfl

protected def map₂' (f : α → β → γ) (h : (s₁.r ⇒ s₂.r ⇒ s₃.r) f f) :

quotient s₁ → quotient s₂ → quotient s₃ :=

quotient.map₂ f h

@[simp] lemma map₂'_mk' (f : α → β → γ) (h) (x : α) :

(quotient.mk' x : quotient s₁).map₂' f h =

(quotient.map' (f x) (h (setoid.refl x)) : quotient s₂ → quotient s₃) :=

rfl

lemma exact' {a b : α} :

(quotient.mk' a : quotient s₁) = quotient.mk' b → @setoid.r _ s₁ a b :=

quotient.exact

lemma sound' {a b : α} : @setoid.r _ s₁ a b → @quotient.mk' α s₁ a = quotient.mk' b :=

quotient.sound

protected lemma eq' {a b : α} : @quotient.mk' α s₁ a = quotient.mk' b ↔ @setoid.r _ s₁ a b :=

quotient.eq

noncomputable def out' (a : quotient s₁) : α := quotient.out a

@[simp] theorem out_eq' (q : quotient s₁) : quotient.mk' q.out' = q := q.out_eq

theorem mk_out' (a : α) : @setoid.r α s₁ (quotient.mk' a : quotient s₁).out' a :=

quotient.exact (quotient.out_eq _)

variables [setoid α]

protected lemma mk'_eq_mk (x : α) : quotient.mk' x = ⟦x⟧ := rfl

@[simp] protected lemma lift_on'_mk (x : α) (f : α → β) (h) : ⟦x⟧.lift_on' f h = f x := rfl

@[simp] protected lemma lift_on₂'_mk [setoid β] (f : α → β → γ) (h) (a : α) (b : β) :

quotient.lift_on₂' ⟦a⟧ ⟦b⟧ f h = f a b := quotient.lift_on₂'_mk' _ _ _ _

@[simp] lemma map'_mk [setoid β] (f : α → β) (h) (x : α) : ⟦x⟧.map' f h = ⟦f x⟧ := rfl

instance (q : quotient s₁) (f : α → Prop) (h : ∀ a b, @setoid.r α s₁ a b → f a = f b)

[decidable_pred f] :

decidable (quotient.lift_on' q f h) :=

quotient.lift.decidable_pred _ _ q

instance (q₁ : quotient s₁) (q₂ : quotient s₂) (f : α → β → Prop)

(h : ∀ a₁ b₁ a₂ b₂, @setoid.r α s₁ a₁ a₂ → @setoid.r β s₂ b₁ b₂ → f a₁ b₁ = f a₂ b₂)

[Π a, decidable_pred (f a)] :

decidable (quotient.lift_on₂' q₁ q₂ f h) :=

quotient.lift₂.decidable_pred _ _ _ _

end quotient