From f41d92199a05d726c459bd0f898cc860f4211b55 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 10 Apr 2015 20:33:33 -0400 Subject: [PATCH] feat(hit): make type quotient primitive instead of colimit --- hott/hit/coeq.hlean | 37 ++++-------- hott/hit/colimit.hlean | 113 +++++++++++++++++++++++++---------- hott/hit/cylinder.hlean | 37 +++++------- hott/hit/pushout.hlean | 67 ++++++--------------- hott/hit/quotient.hlean | 34 ++++------- hott/hit/suspension.hlean | 2 +- hott/hit/type_quotient.hlean | 32 ++++++++++ hott/init/hit.hlean | 55 +++++++---------- 8 files changed, 189 insertions(+), 188 deletions(-) create mode 100644 hott/hit/type_quotient.hlean diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index 6ebe1c410..2d8251bf6 100644 --- a/hott/hit/coeq.hlean +++ b/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 := - diagram.mk bool - bool - (λi, bool.rec_on i A B) - (λj, ff) - (λj, tt) - (λj, bool.rec_on j f g) + inductive coeq_rel : B → B → Type := + | Rmk : Π(x : A), coeq_rel (f x) (g x) + open coeq_rel + local abbreviation R := coeq_rel - local notation `D` := coeq_diag - - definition coeq := colimit coeq_diag -- TODO: define this in root namespace - local attribute coeq_diag [instance] + definition coeq : Type := type_quotient coeq_rel -- TODO: define this in root namespace 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), - { intros [i, x], cases i, - exact (@cglue _ _ x ▹ P_i (f x)), - 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} + fapply (type_quotient.rec_on y), + { intro a, apply P_i}, + { intros [a, a', H], cases H, apply Pcp} end protected definition rec_on [reducible] {P : coeq → Type} (y : coeq) diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index ac8570047..1ad909d5b 100644 --- a/hott/hit/colimit.hlean +++ b/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. -/ - -open eq colimit colimit.diagram function +/- definition of a general colimit -/ +open eq nat type_quotient sigma 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) - (Pglue : Π(j : Ihom) (x : ob (dom j)), Pincl (hom j x) = Pincl x) : colimit D → P := - rec Pincl (λj x, !tr_constant ⬝ Pglue j x) + local abbreviation B := Σ(i : I), A i + inductive colim_rel : B → B → Type := + | 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) - (Pincl : Π⦃i : Iob⦄ (x : ob i), P) - (Pglue : Π(j : Ihom) (x : ob (dom j)), Pincl (hom j x) = Pincl x) : P := + -- TODO: define this in root namespace + definition colimit : Type := + 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) - (Pglue : Π(j : Ihom) (x : ob (dom j)), Pincl (hom j x) = Pincl x) {j : Ihom} (x : ob (dom j)) : - ap (elim Pincl Pglue) (cglue j x) = sorry ⬝ Pglue j x ⬝ sorry := + definition rec_cglue [reducible] {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) + {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_colimit +namespace seq_colim context parameters {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n)) variables {n : ℕ} (a : A n) - definition seq_diagram : diagram := - diagram.mk ℕ ℕ A id succ f - local attribute seq_diagram [instance] + local abbreviation B := Σ(n : ℕ), A n + inductive seq_rel : B → B → Type := + | 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 := - colimit seq_diagram + definition seq_colim : Type := + type_quotient seq_rel - definition inclusion : seq_colim f := - @colimit.inclusion _ _ a + definition inclusion : seq_colim := + 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 := - @colimit.rec _ _ Pincl Pglue + (Pglue : Π(n : ℕ) (a : A n), glue a ▹ Pincl (f a) = Pincl a) (aa : seq_colim) : P aa := + 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 := - @colimit.elim _ _ Pincl Pglue + (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : seq_colim → P := + 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 diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean index 62c098cac..773e8c3bc 100644 --- a/hott/hit/cylinder.hlean +++ b/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 := - diagram.mk bool - unit.{0} - (λi, bool.rec_on i A B) - (λj, ff) - (λj, tt) - (λj, f) + local abbreviation C := B + A + inductive cylinder_rel : C → C → Type := + | Rmk : Π(a : A), cylinder_rel (inl (f a)) (inr a) + open cylinder_rel + local abbreviation R := cylinder_rel - local notation `D` := cylinder_diag - - definition cylinder := colimit cylinder_diag -- TODO: define this in root namespace - local attribute cylinder_diag [instance] + definition cylinder := type_quotient cylinder_rel -- TODO: define this in root namespace 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), - { intros [i, x], cases i, - apply Ptop, - apply Pbase}, - { intros [j, x], cases j, apply Pseg} + fapply (type_quotient.rec_on x), + { intro a, cases a, + apply Pbase, + apply Ptop}, + { intros [a, a', H], cases H, apply Pseg} end protected definition rec_on [reducible] {P : cylinder → Type} (x : cylinder) diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index 939343c82..271694069 100644 --- a/hott/hit/pushout.hlean +++ b/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.{u}} (f : TL → BL) (g : TL → TR) +parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) - inductive pushout_ob := - | tl : pushout_ob - | bl : pushout_ob - | tr : pushout_ob + local abbreviation A := BL + TR + inductive pushout_rel : A → A → Type := + | Rmk : Π(x : TL), pushout_rel (inl (f x)) (inr (g x)) + open pushout_rel + local abbreviation R := pushout_rel - open pushout_ob - - 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 pushout : Type := type_quotient pushout_rel -- TODO: define this in root namespace 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), - { intros [i, x], cases i, - exact (@cglue _ _ x ▹ Pinl (f x)), + fapply (type_quotient.rec_on y), + { intro a, cases a, apply Pinl, apply Pinr}, - { intros [j, x], cases j, - 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} + { intros [a, a', H], cases H, apply 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 diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index a0536e672..5c074c617 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -8,36 +8,23 @@ Authors: Floris van Doorn Declaration of set-quotients -/ -/- -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 .type_quotient .trunc -import .coeq .trunc - -open coeq eq is_trunc trunc +open eq is_trunc trunc type_quotient namespace quotient context -universe u -parameters {A : Type.{u}} (R : A → A → hprop.{u}) - - 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)) +parameters {A : Type} (R : A → A → hprop) + -- set-quotients are just truncations of type-quotients + definition quotient : Type := trunc 0 (type_quotient (λa a', trunctype.carrier (R a 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], - --rewrite (transport_compose P tr (cp pt1 pt2 (total.mk H)) (Pc a)) + { intros [a, a', H], apply concat, apply transport_compose;apply Pp}} end diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean index d7ddc440e..b3d6e274e 100644 --- a/hott/hit/suspension.hlean +++ b/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 diff --git a/hott/hit/type_quotient.hlean b/hott/hit/type_quotient.hlean new file mode 100644 index 000000000..26f5030df --- /dev/null +++ b/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 diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean index 7698f033c..8c770aab3 100644 --- a/hott/init/hit.hlean +++ b/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 -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 type_quotient.{u v} {A : Type.{u}} (R : A → A → Type.{v}) : Type.{max u v} -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 - abbreviation ι := @inclusion + constant eq_of_rel {A : Type} {R : A → A → Type} {a a' : A} (H : R a a') + : 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} - (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) - (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) - (y : colimit D), P y + protected definition rec_on [reducible] {A : Type} {R : A → A → Type} {P : type_quotient R → Type} + (x : type_quotient R) (Pc : Π(a : A), P (class_of R a)) + (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a') : P x := + rec Pc Pp x - definition rec_incl [reducible] [D : diagram] {P : colimit D → Type} - (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) - (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) - {i : Iob} (x : ob i) : rec Pincl Pglue (ι x) = Pincl x := + definition rec_class_of {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') + (a : A) : rec Pc Pp (class_of R a) = Pc a := sorry --idp - definition rec_cglue [reducible] [D : diagram] {P : colimit D → Type} - (Pincl : Π⦃i : Iob⦄ (x : ob i), P (ι x)) - (Pglue : Π(j : Ihom) (x : ob (dom j)), cglue j x ▹ Pincl (hom j x) = Pincl x) - {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 + constant rec_eq_of_rel {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') + {a a' : A} (H : R a a') : apD (rec Pc Pp) (eq_of_rel H) = sorry ⬝ Pp H ⬝ sorry - protected definition rec_on [reducible] [D : diagram] {P : colimit D → Type} (y : colimit D) - (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 +end type_quotient