import logic.cast data.list data.sigma

-- The (pre-)quotient type kernel extension would add the following constants
--    quot, pquot.mk, pquot.eqv and pquot.rec
-- and a computational rule, which we call pquot.comp here.
-- Note that, these constants do not assume the environment contains =
constant pquot.{l} {A : Type.{l}} (R : A → A → Prop) : Type.{l}

constant pquot.abs  {A : Type} (R : A → A → Prop) : A → pquot R
-- pquot.eqv is a way to say R a b → (pquot.abs R a) = (pquot.abs R b) without mentioning equality
constant pquot.eqv {A : Type} (R : A → A → Prop) {a b : A} : R a b → ∀ (P : pquot R → Prop), P (pquot.abs R a) → P (pquot.abs R b)
constant pquot.rec {A : Type} {R : A → A → Prop} {C : pquot R → Type}
                  (f : Π a, C (pquot.abs R a))
                  -- sound is essentially saying: ∀ (a b : A) (H : R a b), f a == f b
                  -- H makes sure we can only define a function on (quot R) if for all a b : A
                  --  R a b → f a == f b
                  (sound : ∀ a b, R a b → ∀ P : (Π (q : pquot R), C q → Prop), P (pquot.abs R a) (f a) → P (pquot.abs R b) (f b))
                  (q : pquot R)
                  : C q
-- We would also get the following computational rule:
--    pquot.rec R H₁ H₂ (pquot.abs R a) ==> H₁ a
constant pquot.comp {A : Type} {R : A → A → Prop} {C : pquot R → Type}
                   (f : Π a, C (pquot.abs R a))
                   (sound : ∀ a b, R a b → ∀ P : (Π (q : pquot R), C q → Prop), P (pquot.abs R a) (f a) → P (pquot.abs R b) (f b))
                   (a : A)
                   -- In the implementation this would be a computational rule
                   : pquot.rec f sound (pquot.abs R a) = f a

-- If the environment contains = and ==, then we can define

definition pquot.eq {A : Type} (R : A → A → Prop) {a b : A} (H : R a b) : pquot.abs R a = pquot.abs R b :=
have aux : ∀ (P : pquot R → Prop), P (pquot.abs R a) → P (pquot.abs R b), from
  pquot.eqv R H,
aux (λ x : pquot R, pquot.abs R a = x) rfl

definition pquot.rec_on {A : Type} {R : A → A → Prop} {C : pquot R → Type}
                        (q : pquot R)
                        (f : Π a, C (pquot.abs R a))
                        (sound : ∀ (a b : A), R a b → f a == f b)
                        : C q :=
pquot.rec f
  (λ (a b : A) (H : R a b) (P : Π (q : pquot R), C q → Prop) (Ha : P (pquot.abs R a) (f a)),
    have aux₁ : f a == f b, from sound a b H,
    have aux₂ : pquot.abs R a = pquot.abs R b, from pquot.eq R H,
    have aux₃ : ∀ (c₁ c₂ : C (pquot.abs R a)) (e : c₁ == c₂), P (pquot.abs R a) c₁ → P (pquot.abs R a) c₂, from
      λ c₁ c₂ e H, eq.rec_on (heq.to_eq e) H,
    have aux₄ : ∀ (c₁ : C (pquot.abs R a)) (c₂ : C (pquot.abs R b)) (e : c₁ == c₂), P (pquot.abs R a) c₁ → P (pquot.abs R b) c₂, from
      eq.rec_on aux₂ aux₃,
    show P (pquot.abs R b) (f b), from
      aux₄ (f a) (f b) aux₁ Ha)
  q

definition pquot.lift {A : Type} {R : A → A → Prop} {B : Type}
                      (f : A → B)
                      (sound : ∀ (a b : A), R a b → f a = f b)
                      (q : pquot R)
                      : B :=
pquot.rec_on q f (λ (a b : A) (H : R a b), heq.of_eq (sound a b H))

theorem pquot.induction_on {A : Type} {R : A → A → Prop} {P : pquot R → Prop}
                           (q : pquot R)
                           (f : ∀ a, P (pquot.abs R a))
                           : P q :=
pquot.rec_on q f (λ (a b : A) (H : R a b),
  have aux₁ : pquot.abs R a = pquot.abs R b,         from pquot.eq R H,
  have aux₂ : P (pquot.abs R a) = P (pquot.abs R b), from congr_arg P aux₁,
  have aux₃ : cast aux₂ (f a) = f b,             from proof_irrel (cast aux₂ (f a)) (f b),
  show f a == f b, from
    @cast_to_heq _ _ _ _ aux₂ aux₃)

theorem pquot.abs.surjective {A : Type} {R : A → A → Prop} : ∀ q : pquot R, ∃ x : A, pquot.abs R x = q :=
take q, pquot.induction_on q (take a, exists_intro a rfl)

definition pquot.exact {A : Type} (R : A → A → Prop) :=
∀ a b : A, pquot.abs R a = pquot.abs R b → R a b

-- Definable quotient
structure dquot {A : Type} (R : A → A → Prop) :=
mk :: (rep : pquot R → A)
      (complete : ∀a, R (rep (pquot.abs R a)) a)
      -- (stable : ∀q, pquot.abs R (rep q) = q)

structure is_equiv {A : Type} (R : A → A → Prop) :=
mk :: (refl  : ∀x, R x x)
      (symm  : ∀{x y}, R x y → R y x)
      (trans : ∀{x y z}, R x y → R y z → R x z)

-- Definiable quotients are exact if R is an equivalence relation
theorem quot.exact {A : Type} {R : A → A → Prop} (eqv : is_equiv R) (q : dquot R) : pquot.exact R :=
λ (a b : A) (H : pquot.abs R a = pquot.abs R b),
  have H₁ : pquot.abs R a = pquot.abs R a → R (dquot.rep q (pquot.abs R a)) (dquot.rep q (pquot.abs R a)),
    from λH, is_equiv.refl eqv _,
  have H₂ : pquot.abs R a = pquot.abs R b → R (dquot.rep q (pquot.abs R a)) (dquot.rep q (pquot.abs R b)),
    from eq.subst H H₁,
  have H₃ : R (dquot.rep q (pquot.abs R a)) (dquot.rep q (pquot.abs R b)),
    from H₂ H,
  have H₄ : R a (dquot.rep q (pquot.abs R a)), from is_equiv.symm eqv (dquot.complete q a),
  have H₅ : R (dquot.rep q (pquot.abs R b)) b, from dquot.complete q b,
  is_equiv.trans eqv H₄ (is_equiv.trans eqv H₃ H₅)