feat(hit): make type quotient primitive instead of colimit

hott/hit/coeq.hlean

@@ -8,9 +8,9 @@ Authors: Floris van Doorn
 Declaration of the coequalizer
 -/
 
-import .colimit
+import .type_quotient
 
-open colimit bool eq
+open type_quotient eq
 
 namespace coeq
 context
@@ -18,39 +18,26 @@ context
 universe u
 parameters {A B : Type.{u}} (f g : A → B)
 
-  definition coeq_diag [reducible] : diagram :=
+  inductive coeq_rel : B → B → Type :=
-  diagram.mk bool
+  | Rmk : Π(x : A), coeq_rel (f x) (g x)
-             bool
+  open coeq_rel
-             (λi, bool.rec_on i A B)
+  local abbreviation R := coeq_rel
-             (λj, ff)
-             (λj, tt)
-             (λj, bool.rec_on j f g)
 
-  local notation `D` := coeq_diag
+  definition coeq : Type := type_quotient coeq_rel -- TODO: define this in root namespace
-
-  definition coeq := colimit coeq_diag -- TODO: define this in root namespace
-  local attribute coeq_diag [instance]
 
   definition coeq_i (x : B) : coeq :=
-  @ι _ _ x
+  class_of R x
 
   /- cp is the name Coq uses. I don't know what it abbreviates, but at least it's short :-) -/
   definition cp (x : A) : coeq_i (f x) = coeq_i (g x) :=
-  @cglue _ _ x ⬝ (@cglue _ _ x)⁻¹
+  eq_of_rel (Rmk f g x)
 
   protected definition rec {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
     (Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x)) (y : coeq) : P y :=
   begin
-    fapply (@colimit.rec_on _ _ y),
+    fapply (type_quotient.rec_on y),
-    { intros [i, x], cases i,
+    { intro a, apply P_i},
-        exact (@cglue _ _ x ▹ P_i (f x)),
+    { intros [a, a', H], cases H, apply Pcp}
-        apply P_i},
-    { intros [j, x], cases j,
-        exact idp,
-      esimp [coeq_diag],
-      apply tr_eq_of_eq_inv_tr,
-      apply concat, rotate 1, apply tr_con,
-      rewrite -Pcp}
   end
 
   protected definition rec_on [reducible] {P : coeq → Type} (y : coeq)

hott/hit/colimit.hlean

@@ -5,76 +5,123 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: hit.colimit
 Authors: Floris van Doorn
 
-Colimits.
+Definition of general colimits and sequential colimits.
 -/
 
-/- The hit colimit is primitive, declared in init.hit. -/
+/- definition of a general colimit -/
-
+open eq nat type_quotient sigma
-open eq colimit colimit.diagram function
 
 namespace colimit
+context
+  parameters {I J : Type} (A : I → Type) (dom cod : J → I)
+             (f : Π(j : J), A (dom j) → A (cod j))
+  variables {i : I} (a : A i) (j : J) (b : A (dom j))
 
-  protected definition elim [D : diagram] {P : Type} (Pincl : Π⦃i : Iob⦄ (x : ob i), P)
+  local abbreviation B := Σ(i : I), A i
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), Pincl (hom j x) = Pincl x) : colimit D → P :=
+  inductive colim_rel : B → B → Type :=
-  rec Pincl (λj x, !tr_constant ⬝ Pglue j x)
+  | Rmk : Π{j : J} (a : A (dom j)), colim_rel ⟨cod j, f j a⟩ ⟨dom j, a⟩
+  open colim_rel
+  local abbreviation R := colim_rel
 
-  protected definition elim_on [reducible] [D : diagram] {P : Type} (y : colimit D)
+  -- TODO: define this in root namespace
-    (Pincl : Π⦃i : Iob⦄ (x : ob i), P)
+  definition colimit : Type :=
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), Pincl (hom j x) = Pincl x) : P :=
+  type_quotient colim_rel
+
+  definition incl : colimit :=
+  class_of R ⟨i, a⟩
+  abbreviation ι := @incl
+
+  definition cglue : ι (f j b) = ι b :=
+  eq_of_rel (Rmk f b)
+
+   protected definition rec {P : colimit → Type}
+    (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
+    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x)
+      (y : colimit) : P y :=
+  begin
+    fapply (type_quotient.rec_on y),
+    { intro a, cases a, apply Pincl},
+    { intros [a, a', H], cases H, apply Pglue}
+  end
+
+  protected definition rec_on [reducible] {P : colimit → Type} (y : colimit)
+    (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
+    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x) : P y :=
+  rec Pincl Pglue y
+
+   protected definition elim {P : Type} (Pincl : Π⦃i : I⦄ (x : A i), P)
+    (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) (y : colimit) : P :=
+  rec Pincl (λj a, !tr_constant ⬝ Pglue j a) y
+
+  protected definition elim_on [reducible] {P : Type} (y : colimit)
+    (Pincl : Π⦃i : I⦄ (x : A i), P)
+    (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) : P :=
   elim Pincl Pglue y
 
-  definition elim_cglue [D : diagram] {P : Type} (Pincl : Π⦃i : Iob⦄ (x : ob i), P)
+  definition rec_cglue [reducible] {P : colimit → Type}
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), Pincl (hom j x) = Pincl x) {j : Ihom} (x : ob (dom j)) :
+    (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
-      ap (elim Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
+    (Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x)
+      {j : J} (x : A (dom j)) : apD (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
   sorry
 
+  definition elim_cglue [reducible] {P : Type}
+    (Pincl : Π⦃i : I⦄ (x : A i), P)
+    (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x)
+      {j : J} (x : A (dom j)) : ap (elim Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
+  sorry
+
+end
 end colimit
 
 /- definition of a sequential colimit -/
-open nat
+namespace seq_colim
-
-namespace seq_colimit
 context
   parameters {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n))
   variables {n : ℕ} (a : A n)
 
-  definition seq_diagram : diagram :=
+  local abbreviation B := Σ(n : ℕ), A n
-  diagram.mk ℕ ℕ A id succ f
+  inductive seq_rel : B → B → Type :=
-  local attribute seq_diagram [instance]
+  | Rmk : Π{n : ℕ} (a : A n), seq_rel ⟨succ n, f a⟩ ⟨n, a⟩
+  open seq_rel
+  local abbreviation R := seq_rel
 
   -- TODO: define this in root namespace
-  definition seq_colim {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n)) : Type :=
+  definition seq_colim : Type :=
-  colimit seq_diagram
+  type_quotient seq_rel
 
-  definition inclusion : seq_colim f :=
+  definition inclusion : seq_colim :=
-  @colimit.inclusion _ _ a
+  class_of R ⟨n, a⟩
 
   abbreviation sι := @inclusion
 
   definition glue : sι (f a) = sι a :=
-  @cglue _ _ a
+  eq_of_rel (Rmk f a)
 
-  protected definition rec [reducible] {P : seq_colim f → Type}
+  protected definition rec [reducible] {P : seq_colim → Type}
     (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
-    (Pglue : Π(n : ℕ) (a : A n), glue a ▹ Pincl (f a) = Pincl a) : Πaa, P aa :=
+    (Pglue : Π(n : ℕ) (a : A n), glue a ▹ Pincl (f a) = Pincl a) (aa : seq_colim) : P aa :=
-  @colimit.rec _ _ Pincl Pglue
+  begin
+    fapply (type_quotient.rec_on aa),
+    { intro a, cases a, apply Pincl},
+    { intros [a, a', H], cases H, apply Pglue}
+  end
 
-  protected definition rec_on [reducible] {P : seq_colim f → Type} (aa : seq_colim f)
+  protected definition rec_on [reducible] {P : seq_colim → Type} (aa : seq_colim)
     (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
     (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▹ Pincl (f a) = Pincl a)
       : P aa :=
   rec Pincl Pglue aa
 
   protected definition elim {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
-    (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : seq_colim f → P :=
+    (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : seq_colim → P :=
-  @colimit.elim _ _ Pincl Pglue
+  rec Pincl (λn a, !tr_constant ⬝ Pglue a)
 
-  protected definition elim_on [reducible] {P : Type} (aa : seq_colim f)
+  protected definition elim_on [reducible] {P : Type} (aa : seq_colim)
     (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
     (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : P :=
   elim Pincl Pglue aa
 
-  definition rec_glue {P : seq_colim f → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
+  definition rec_glue {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
     (Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▹ Pincl (f a) = Pincl a) {n : ℕ} (a : A n)
       : apD (rec Pincl Pglue) (glue a) = sorry ⬝ Pglue a ⬝ sorry :=
   sorry
@@ -85,4 +132,4 @@ context
   sorry
 
 end
-end seq_colimit
+end seq_colim

hott/hit/cylinder.hlean

@@ -8,9 +8,9 @@ Authors: Floris van Doorn
 Declaration of mapping cylinders
 -/
 
-import .colimit
+import .type_quotient
 
-open colimit bool unit eq
+open type_quotient eq sum
 
 namespace cylinder
 context
@@ -18,37 +18,32 @@ context
 universe u
 parameters {A B : Type.{u}} (f : A → B)
 
-  definition cylinder_diag [reducible] : diagram :=
+  local abbreviation C := B + A
-  diagram.mk bool
+  inductive cylinder_rel : C → C → Type :=
-             unit.{0}
+  | Rmk : Π(a : A), cylinder_rel (inl (f a)) (inr a)
-             (λi, bool.rec_on i A B)
+  open cylinder_rel
-             (λj, ff)
+  local abbreviation R := cylinder_rel
-             (λj, tt)
-             (λj, f)
 
-  local notation `D` := cylinder_diag
+  definition cylinder := type_quotient cylinder_rel -- TODO: define this in root namespace
-
-  definition cylinder := colimit cylinder_diag -- TODO: define this in root namespace
-  local attribute cylinder_diag [instance]
 
   definition base (b : B) : cylinder :=
-  @ι _ _ b
+  class_of R (inl b)
 
   definition top (a : A) : cylinder :=
-  @ι _ _ a
+  class_of R (inr a)
 
   definition seg (a : A) : base (f a) = top a :=
-  @cglue _ star a
+  eq_of_rel (Rmk f a)
 
   protected definition rec {P : cylinder → Type}
     (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
     (Pseg : Π(a : A), seg a ▹ Pbase (f a) = Ptop a) (x : cylinder) : P x :=
   begin
-    fapply (@colimit.rec_on _ _ x),
+    fapply (type_quotient.rec_on x),
-    { intros [i, x], cases i,
+    { intro a, cases a,
-        apply Ptop,
+       apply Pbase,
-        apply Pbase},
+       apply Ptop},
-    { intros [j, x], cases j, apply Pseg}
+    { intros [a, a', H], cases H, apply Pseg}
   end
 
   protected definition rec_on [reducible] {P : cylinder → Type} (x : cylinder)

hott/hit/pushout.hlean

@@ -8,72 +8,41 @@ Authors: Floris van Doorn
 Declaration of the pushout
 -/
 
-import .colimit
+import .type_quotient
 
-open colimit bool eq
+open type_quotient eq sum
 
 namespace pushout
 context
 
-universe u
+parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
-parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
 
-  inductive pushout_ob :=
+  local abbreviation A := BL + TR
-  | tl : pushout_ob
+  inductive pushout_rel : A → A → Type :=
-  | bl : pushout_ob
+  | Rmk : Π(x : TL), pushout_rel (inl (f x)) (inr (g x))
-  | tr : pushout_ob
+  open pushout_rel
+  local abbreviation R := pushout_rel
 
-  open pushout_ob
+  definition pushout : Type := type_quotient pushout_rel -- TODO: define this in root namespace
-
-  definition pushout_diag [reducible] : diagram :=
-  diagram.mk pushout_ob
-             bool
-             (λi, pushout_ob.rec_on i TL BL TR)
-             (λj, bool.rec_on j tl tl)
-             (λj, bool.rec_on j bl tr)
-             (λj, bool.rec_on j f  g)
-
-  local notation `D` := pushout_diag
-  -- open bool
-  -- definition pushout_diag : diagram :=
-  -- diagram.mk pushout_ob
-  --            bool
-  --            (λi, match i with | tl := TL | tr := TR | bl := BL end)
-  --            (λj, match j with | tt := tl | ff := tl end)
-  --            (λj, match j with | tt := bl | ff := tr end)
-  --            (λj, match j with | tt := f  | ff := g  end)
-
-  definition pushout := colimit pushout_diag -- TODO: define this in root namespace
-  local attribute pushout_diag [instance]
 
   definition inl (x : BL) : pushout :=
-  @ι _ _ x
+  class_of R (inl x)
 
   definition inr (x : TR) : pushout :=
-  @ι _ _ x
+  class_of R (inr x)
 
   definition glue (x : TL) : inl (f x) = inr (g x) :=
-  @cglue _ _ x ⬝ (@cglue _ _ x)⁻¹
+  eq_of_rel (Rmk f g x)
 
   protected definition rec {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
     (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
       (y : pushout) : P y :=
   begin
-    fapply (@colimit.rec_on _ _ y),
+    fapply (type_quotient.rec_on y),
-    { intros [i, x], cases i,
+    { intro a, cases a,
-       exact (@cglue _ _ x ▹ Pinl (f x)),
        apply Pinl,
        apply Pinr},
-    { intros [j, x], cases j,
+    { intros [a, a', H], cases H, apply Pglue}
-        exact idp,
-      esimp [pushout_ob.cases_on, pushout_diag],
--- change (transport P (@cglue _ tt x) (Pinr (g x)) = transport P (coherence x) (Pinl (f x))),
-      -- apply concat;rotate 1;apply (idpath (coherence x ▹ Pinl (f x))),
-      -- apply concat;apply (ap (transport _ _));apply (idpath (Pinr (g x))),
-      apply tr_eq_of_eq_inv_tr,
---      rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}tr_con,
-      apply concat, rotate 1, apply tr_con,
-      rewrite -Pglue}
   end
 
   protected definition rec_on [reducible] {P : pushout → Type} (y : pushout)
@@ -85,12 +54,12 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
   definition rec_inl {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
     (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
       (x : BL) : rec Pinl Pinr Pglue (inl x) = Pinl x :=
-  @colimit.rec_incl _ _ _ _ _ _ --idp
+  rec_class_of _ _ _ --idp
 
   definition rec_inr {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
     (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
       (x : TR) : rec Pinl Pinr Pglue (inr x) = Pinr x :=
-  @colimit.rec_incl _ _ _ _ _ _ --idp
+  rec_class_of _ _ _ --idp
 
   protected definition elim {P : Type} (Pinl : BL → P) (Pinr : TR → P)
     (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (y : pushout) : P :=
@@ -113,7 +82,7 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
 
 end
 
-  open pushout equiv is_equiv unit
+  open pushout equiv is_equiv unit bool
 
   namespace test
     definition unit_of_empty (u : empty) : unit := star

hott/hit/quotient.hlean

@@ -8,36 +8,23 @@ Authors: Floris van Doorn
 Declaration of set-quotients
 -/
 
-/-
+import .type_quotient .trunc
-We aim to model
-HIT quotient : Type :=
-   | class_of : A -> quotient
-   | eq_of_rel : Πa a', R a a' → class_of a = class_of a'
-   | is_hset_quotient : is_hset quotient
--/
 
-import .coeq .trunc
+open eq is_trunc trunc type_quotient
-
-open coeq eq is_trunc trunc
 
 namespace quotient
 context
-universe u
+parameters {A : Type} (R : A → A → hprop)
-parameters {A : Type.{u}} (R : A → A → hprop.{u})
+  -- set-quotients are just truncations of type-quotients
-
+  definition quotient : Type := trunc 0 (type_quotient (λa a', trunctype.carrier (R a a')))
-  structure total : Type := {pt1 : A} {pt2 : A} (rel : R pt1 pt2)
-  open total
-
-  definition quotient : Type :=
-  trunc 0 (coeq (pt1 : total → A) (pt2 : total → A))
 
   definition class_of (a : A) : quotient :=
-  tr (coeq_i _ _ a)
+  tr (class_of _ a)
 
   definition eq_of_rel {a a' : A} (H : R a a') : class_of a = class_of a' :=
-  ap tr (cp _ _ (total.mk H))
+  ap tr (eq_of_rel H)
 
-  definition is_hset_quotient : is_hset quotient :=
+  theorem is_hset_quotient : is_hset quotient :=
   by unfold quotient; exact _
 
   protected definition rec {P : quotient → Type} [Pt : Πaa, is_trunc 0 (P aa)]
@@ -46,10 +33,9 @@ parameters {A : Type.{u}} (R : A → A → hprop.{u})
   begin
     apply (@trunc.rec_on _ _ P x),
     { intro x', apply Pt},
-    { intro y, fapply (coeq.rec_on _ _ y),
+    { intro y, fapply (type_quotient.rec_on y),
       { exact Pc},
-      { intro H, cases H with [a, a', H], esimp [is_typeof],
+      { intros [a, a', H],
-        --rewrite (transport_compose P tr (cp pt1 pt2 (total.mk H)) (Pc a))
         apply concat, apply transport_compose;apply Pp}}
   end
 

hott/hit/suspension.hlean

@@ -12,7 +12,7 @@ import .pushout
 
 open pushout unit eq
 
-definition suspension (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star)
+definition suspension (A : Type) : Type := pushout (λ(a : A), star.{0}) (λ(a : A), star.{0})
 
 namespace suspension
 

hott/hit/type_quotient.hlean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: hit.type_quotient
+Authors: Floris van Doorn
+
+Type quotients (quotient without truncation)
+-/
+
+/- The hit type_quotient is primitive, declared in init.hit. -/
+
+open eq
+
+namespace type_quotient
+
+  variables {A : Type} {R : A → A → Type}
+
+  protected definition elim {P : Type} (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a')
+    (x : type_quotient R) : P :=
+  rec Pc (λa a' H, !tr_constant ⬝ Pp H) x
+
+  protected definition elim_on [reducible] {P : Type} (x : type_quotient R)
+    (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P :=
+  elim Pc Pp x
+
+  protected definition elim_eq_of_rel {P : Type} (Pc : A → P)
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a')
+    : ap (elim Pc Pp) (eq_of_rel H) = sorry ⬝ Pp H ⬝ sorry :=
+  sorry
+
+end type_quotient

hott/init/hit.hlean

@@ -18,7 +18,7 @@ open is_trunc eq
   We take two higher inductive types (hits) as primitive notions in Lean. We define all other hits
   in terms of these two hits. The hits which are primitive are
     - n-truncation
-    - general colimits
+    - type quotients (non-truncated quotients)
   For each of the hits we add the following constants:
     - the type formation
     - the term and path constructors
@@ -52,46 +52,31 @@ namespace trunc
 
 end trunc
 
-namespace colimit
+constant type_quotient.{u v} {A : Type.{u}} (R : A → A → Type.{v}) : Type.{max u v}
-structure diagram [class] :=
-  (Iob : Type)
-  (Ihom : Type)
-  (ob : Iob → Type)
-  (dom cod : Ihom → Iob)
-  (hom : Π(j : Ihom), ob (dom j) → ob (cod j))
-end colimit
-open colimit colimit.diagram
 
-constant colimit.{u v w} : diagram.{u v w} → Type.{max u v w}
+namespace type_quotient
 
-namespace colimit
+  constant class_of {A : Type} (R : A → A → Type) (a : A) : type_quotient R
 
-  constant inclusion : Π [D : diagram] {i : Iob}, ob i → colimit D
+  constant eq_of_rel {A : Type} {R : A → A → Type} {a a' : A} (H : R a a')
-  abbreviation ι := @inclusion
+    : class_of R a = class_of R a'
 
-  constant cglue : Π [D : diagram] (j : Ihom) (x : ob (dom j)), ι (hom j x) = ι x
+  /-protected-/ constant rec {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
+    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
+    (x : type_quotient R) : P x
 
-  /-protected-/ constant rec : Π [D : diagram] {P : colimit D → Type}
+  protected definition rec_on [reducible] {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
-    (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
+    (x : type_quotient R) (Pc : Π(a : A), P (class_of R a))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a') : P x :=
-      (y : colimit D), P y
+  rec Pc Pp x
 
-  definition rec_incl [reducible] [D : diagram] {P : colimit D → Type}
+  definition rec_class_of {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
-    (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
+    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
+    (a : A) : rec Pc Pp (class_of R a) = Pc a :=
-      {i : Iob} (x : ob i) : rec Pincl Pglue (ι x) = Pincl x :=
   sorry --idp
 
-  definition rec_cglue [reducible] [D : diagram] {P : colimit D → Type}
+  constant rec_eq_of_rel {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
-    (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
+    (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x)
+    {a a' : A} (H : R a a') : apD (rec Pc Pp) (eq_of_rel H) = sorry ⬝ Pp H ⬝ sorry
-      {j : Ihom} (x : ob (dom j)) : apD (rec Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry :=
-  --the sorry's in the statement can be removed when rec_incl is definitional
-  sorry
 
-  protected definition rec_on [reducible] [D : diagram] {P : colimit D → Type} (y : colimit D)
+end type_quotient
-    (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x))
-    (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) : P y :=
-  colimit.rec Pincl Pglue y
-
-end colimit