From ff01774fd7f90f50b345a4d487ad072fc65c1590 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 4 Jun 2015 15:57:00 -0400 Subject: [PATCH] renaming(hit): rename type_quotient to quotient, and quotient to set_quotient This renaming is because type_quotient is a nonstandard name. I've had a discussion with Egbert Rijke, Steve Awodey and Dan Licata, and the consensus for a better name was 'quotient'. I had to make changes in src/kernel/hits/hits.cpp, I renamed g_type_quotient* by g_hit_quotient* (to avoid name clash the standard library quotient, although I don't know whether that name clash would matter). --- hott/hit/coeq.hlean | 6 +- hott/hit/colimit.hlean | 12 ++-- hott/hit/cylinder.hlean | 6 +- hott/hit/hit.md | 19 ++++--- hott/hit/pushout.hlean | 6 +- hott/hit/quotient.hlean | 94 +++++++++++++------------------ hott/hit/set_quotient.hlean | 75 ++++++++++++++++++++++++ hott/hit/type_quotient.hlean | 60 -------------------- hott/init/hit.hlean | 40 ++++++------- src/kernel/hits/hits.cpp | 66 +++++++++++----------- tests/lean/640.hlean | 8 +-- tests/lean/640.hlean.expected.out | 8 +-- tests/lean/extra/616a.hlean | 2 +- tests/lean/extra/616b.hlean | 2 +- tests/lean/extra/616c.hlean | 2 +- tests/lean/hott/610.hlean | 6 +- tests/lean/hott/ind_tac2.hlean | 6 +- 17 files changed, 210 insertions(+), 208 deletions(-) create mode 100644 hott/hit/set_quotient.hlean delete mode 100644 hott/hit/type_quotient.hlean diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index ca84309c12..f485c9e8e4 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -6,9 +6,9 @@ Authors: Floris van Doorn Declaration of the coequalizer -/ -import .type_quotient +import .quotient -open type_quotient eq equiv equiv.ops +open quotient eq equiv equiv.ops namespace coeq section @@ -21,7 +21,7 @@ parameters {A B : Type.{u}} (f g : A → B) open coeq_rel local abbreviation R := coeq_rel - definition coeq : Type := type_quotient coeq_rel -- TODO: define this in root namespace + definition coeq : Type := quotient coeq_rel -- TODO: define this in root namespace definition coeq_i (x : B) : coeq := class_of R x diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index 668067fc42..6df6340421 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -7,7 +7,7 @@ Definition of general colimits and sequential colimits. -/ /- definition of a general colimit -/ -open eq nat type_quotient sigma equiv equiv.ops +open eq nat quotient sigma equiv equiv.ops namespace colimit section @@ -23,7 +23,7 @@ section -- TODO: define this in root namespace definition colimit : Type := - type_quotient colim_rel + quotient colim_rel definition incl : colimit := class_of R ⟨i, a⟩ @@ -37,7 +37,7 @@ section (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x) (y : colimit) : P y := begin - fapply (type_quotient.rec_on y), + fapply (quotient.rec_on y), { intro a, cases a, apply Pincl}, { intro a a' H, cases H, apply Pglue} end @@ -92,7 +92,7 @@ end colimit namespace seq_colim section /- - we define it directly in terms of type quotients. An alternative definition could be + we define it directly in terms of quotients. An alternative definition could be definition seq_colim := colimit.colimit A function.id succ f -/ parameters {A : ℕ → Type} (f : Π⦃n⦄, A n → A (succ n)) @@ -106,7 +106,7 @@ section -- TODO: define this in root namespace definition seq_colim : Type := - type_quotient seq_rel + quotient seq_rel definition inclusion : seq_colim := class_of R ⟨n, a⟩ @@ -120,7 +120,7 @@ section (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) (Pglue : Π(n : ℕ) (a : A n), Pincl (f a) =[glue a] Pincl a) (aa : seq_colim) : P aa := begin - fapply (type_quotient.rec_on aa), + fapply (quotient.rec_on aa), { intro a, cases a, apply Pincl}, { intro a a' H, cases H, apply Pglue} end diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean index 8c97afd3a8..1bc3e68509 100644 --- a/hott/hit/cylinder.hlean +++ b/hott/hit/cylinder.hlean @@ -6,9 +6,9 @@ Authors: Floris van Doorn Declaration of mapping cylinders -/ -import .type_quotient +import .quotient -open type_quotient eq sum equiv equiv.ops +open quotient eq sum equiv equiv.ops namespace cylinder section @@ -22,7 +22,7 @@ parameters {A B : Type.{u}} (f : A → B) open cylinder_rel local abbreviation R := cylinder_rel - definition cylinder := type_quotient cylinder_rel -- TODO: define this in root namespace + definition cylinder := quotient cylinder_rel -- TODO: define this in root namespace definition base (b : B) : cylinder := class_of R (inl b) diff --git a/hott/hit/hit.md b/hott/hit/hit.md index eea03abf6b..521c44f28b 100644 --- a/hott/hit/hit.md +++ b/hott/hit/hit.md @@ -4,19 +4,20 @@ hit Declaration and theorems of higher inductive types in Lean. 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 and type quotients. These are defined in -[init.hit](../init.hit.hlean) and they have definitional computation +primitive are n-truncation and quotients. These are defined in +[init.hit](../init/hit.hlean) and they have definitional computation rules on the point constructors. Files in this folder: -* [type_quotient](type_quotient.hlean) (Type quotients, primitive) +* [quotient](quotient.hlean) (quotients, primitive) * [trunc](trunc.hlean) (truncation, primitive) -* [colimit](colimit.hlean) (Colimits of arbitrary diagrams and sequential colimits, defined using type quotients) -* [pushout](pushout.hlean) (Pushouts, defined using type quotients) -* [coeq](coeq.hlean) (Co-equalizers, defined using type quotients) -* [cylinder](cylinder.hlean) (Mapping cylinders, defined using type quotients) -* [quotient](quotient.hlean) (Set-quotients, defined using type quotients and set-truncation) +* [colimit](colimit.hlean) (Colimits of arbitrary diagrams and sequential colimits, defined using quotients) +* [pushout](pushout.hlean) (Pushouts, defined using quotients) +* [coeq](coeq.hlean) (Co-equalizers, defined using quotients) +* [cylinder](cylinder.hlean) (Mapping cylinders, defined using quotients) +* [set_quotient](set_quotient.hlean) (Set-quotients, defined using quotients and set-truncation) * [suspension](suspension.hlean) (Suspensions, defined using pushouts) * [sphere](sphere.hlean) (Higher spheres, defined recursively using suspensions) -* [circle](circle.hlean) \ No newline at end of file +* [circle](circle.hlean) (defined as sphere 1) +* [interval](interval.hlean) (defined as the suspension of unit) \ No newline at end of file diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index 6101efdfd6..e93f4dbf1b 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -6,9 +6,9 @@ Authors: Floris van Doorn Declaration of the pushout -/ -import .type_quotient +import .quotient -open type_quotient eq sum equiv equiv.ops +open quotient eq sum equiv equiv.ops namespace pushout section @@ -21,7 +21,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) open pushout_rel local abbreviation R := pushout_rel - definition pushout : Type := type_quotient R -- TODO: define this in root namespace + definition pushout : Type := quotient R -- TODO: define this in root namespace definition inl (x : BL) : pushout := class_of R (inl x) diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index 7fd57234c8..917b11d389 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -3,73 +3,59 @@ Copyright (c) 2015 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -Declaration of set-quotients +Quotients. This is a quotient without truncation for an arbitrary type-valued binary relation. +See also .set_quotient -/ -import .type_quotient .trunc +/- + The hit quotient is primitive, declared in init.hit. + The constructors are, given {A : Type} (R : A → A → Type), + * class_of : A → quotient R (A implicit, R explicit) + * eq_of_rel : Π{a a' : A}, R a a' → class_of a = class_of a' (R explicit) +-/ -open eq is_trunc trunc type_quotient equiv +open eq equiv sigma.ops namespace quotient -section -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 (class_of _ a) + variables {A : Type} {R : A → A → Type} - definition eq_of_rel {a a' : A} (H : R a a') : class_of a = class_of a' := - ap tr (eq_of_rel _ H) + protected definition elim {P : Type} (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') + (x : quotient R) : P := + quotient.rec Pc (λa a' H, pathover_of_eq (Pp H)) x - theorem is_hset_quotient : is_hset quotient := - begin unfold quotient, exact _ end + protected definition elim_on [reducible] {P : Type} (x : quotient R) + (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P := + quotient.elim Pc Pp x - protected definition rec {P : quotient → Type} [Pt : Πaa, is_hset (P aa)] - (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') - (x : quotient) : P x := - begin - apply (@trunc.rec_on _ _ P x), - { intro x', apply Pt}, - { intro y, fapply (type_quotient.rec_on y), - { exact Pc}, - { intros, apply equiv.to_inv !(pathover_compose _ tr), apply Pp}} - end - - protected definition rec_on [reducible] {P : quotient → Type} (x : quotient) - [Pt : Πaa, is_hset (P aa)] (Pc : Π(a : A), P (class_of a)) - (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') : P x := - rec Pc Pp x - - theorem rec_eq_of_rel {P : quotient → Type} [Pt : Πaa, is_hset (P aa)] - (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') - {a a' : A} (H : R a a') : apdo (rec Pc Pp) (eq_of_rel H) = Pp H := - !is_hset.elimo - - protected definition elim {P : Type} [Pt : is_hset P] (Pc : A → P) - (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : quotient) : P := - rec Pc (λa a' H, pathover_of_eq (Pp H)) x - - protected definition elim_on [reducible] {P : Type} (x : quotient) [Pt : is_hset P] - (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P := - elim Pc Pp x - - theorem elim_eq_of_rel {P : Type} [Pt : is_hset P] (Pc : A → P) + theorem 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) = Pp H := + : ap (quotient.elim Pc Pp) (eq_of_rel R H) = Pp H := begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel H)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel], + apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel R H)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑quotient.elim,rec_eq_of_rel], end - /- - there are no theorems to eliminate to the universe here, - because the universe is generally not a set - -/ + protected definition elim_type (Pc : A → Type) + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : quotient R → Type := + quotient.elim Pc (λa a' H, ua (Pp H)) -end + protected definition elim_type_on [reducible] (x : quotient R) (Pc : A → Type) + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : Type := + quotient.elim_type Pc Pp x + + theorem elim_type_eq_of_rel (Pc : A → Type) + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a') + : transport (quotient.elim_type Pc Pp) (eq_of_rel R H) = to_fun (Pp H) := + by rewrite [tr_eq_cast_ap_fn, ↑quotient.elim_type, elim_eq_of_rel];apply cast_ua_fn + + definition elim_type_uncurried (H : Σ(Pc : A → Type), Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') + : quotient R → Type := + quotient.elim_type H.1 H.2 end quotient -attribute quotient.class_of [constructor] -attribute quotient.rec quotient.elim [unfold-c 7] [recursor 7] -attribute quotient.rec_on quotient.elim_on [unfold-c 4] +attribute quotient.rec [recursor] +attribute quotient.elim [unfold-c 6] [recursor 6] +attribute quotient.elim_type [unfold-c 5] +attribute quotient.elim_on [unfold-c 4] +attribute quotient.elim_type_on [unfold-c 3] diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean new file mode 100644 index 0000000000..f12a16b35f --- /dev/null +++ b/hott/hit/set_quotient.hlean @@ -0,0 +1,75 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn + +Declaration of set-quotients, i.e. quotient of a mere relation which is then set-truncated. +-/ + +import .quotient .trunc + +open eq is_trunc trunc quotient equiv + +namespace set_quotient +section +parameters {A : Type} (R : A → A → hprop) + -- set-quotients are just truncations of (type) quotients + definition set_quotient : Type := trunc 0 (quotient (λa a', trunctype.carrier (R a a'))) + + definition class_of (a : A) : set_quotient := + tr (class_of _ a) + + definition eq_of_rel {a a' : A} (H : R a a') : class_of a = class_of a' := + ap tr (eq_of_rel _ H) + + theorem is_hset_set_quotient : is_hset set_quotient := + begin unfold set_quotient, exact _ end + + protected definition rec {P : set_quotient → Type} [Pt : Πaa, is_hset (P aa)] + (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') + (x : set_quotient) : P x := + begin + apply (@trunc.rec_on _ _ P x), + { intro x', apply Pt}, + { intro y, fapply (quotient.rec_on y), + { exact Pc}, + { intros, apply equiv.to_inv !(pathover_compose _ tr), apply Pp}} + end + + protected definition rec_on [reducible] {P : set_quotient → Type} (x : set_quotient) + [Pt : Πaa, is_hset (P aa)] (Pc : Π(a : A), P (class_of a)) + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') : P x := + rec Pc Pp x + + theorem rec_eq_of_rel {P : set_quotient → Type} [Pt : Πaa, is_hset (P aa)] + (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') + {a a' : A} (H : R a a') : apdo (rec Pc Pp) (eq_of_rel H) = Pp H := + !is_hset.elimo + + protected definition elim {P : Type} [Pt : is_hset P] (Pc : A → P) + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : set_quotient) : P := + rec Pc (λa a' H, pathover_of_eq (Pp H)) x + + protected definition elim_on [reducible] {P : Type} (x : set_quotient) [Pt : is_hset P] + (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P := + elim Pc Pp x + + theorem elim_eq_of_rel {P : Type} [Pt : is_hset P] (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) = Pp H := + begin + apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel H)), + rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel], + end + + /- + there are no theorems to eliminate to the universe here, + because the universe is generally not a set + -/ + +end +end set_quotient + +attribute set_quotient.class_of [constructor] +attribute set_quotient.rec set_quotient.elim [unfold-c 7] [recursor 7] +attribute set_quotient.rec_on set_quotient.elim_on [unfold-c 4] diff --git a/hott/hit/type_quotient.hlean b/hott/hit/type_quotient.hlean deleted file mode 100644 index 5efba863e8..0000000000 --- a/hott/hit/type_quotient.hlean +++ /dev/null @@ -1,60 +0,0 @@ -/- -Copyright (c) 2015 Floris van Doorn. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn - -Type quotients (quotient without truncation) --/ - -/- - The hit type_quotient is primitive, declared in init.hit. - The constructors are - class_of : A → A / R (A implicit, R explicit) - eq_of_rel : Π{a a' : A}, R a a' → class_of a = class_of a' (R explicit) --/ - -open eq equiv sigma.ops - -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 := - type_quotient.rec Pc (λa a' H, pathover_of_eq (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 := - type_quotient.elim Pc Pp x - - theorem 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 (type_quotient.elim Pc Pp) (eq_of_rel R H) = Pp H := - begin - apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel R H)), - rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑type_quotient.elim,rec_eq_of_rel], - end - - protected definition elim_type (Pc : A → Type) - (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : type_quotient R → Type := - type_quotient.elim Pc (λa a' H, ua (Pp H)) - - protected definition elim_type_on [reducible] (x : type_quotient R) (Pc : A → Type) - (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : Type := - type_quotient.elim_type Pc Pp x - - theorem elim_type_eq_of_rel (Pc : A → Type) - (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a') - : transport (type_quotient.elim_type Pc Pp) (eq_of_rel R H) = to_fun (Pp H) := - by rewrite [tr_eq_cast_ap_fn, ↑type_quotient.elim_type, elim_eq_of_rel];apply cast_ua_fn - - definition elim_type_uncurried (H : Σ(Pc : A → Type), Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') - : type_quotient R → Type := - type_quotient.elim_type H.1 H.2 -end type_quotient - -attribute type_quotient.rec [recursor] -attribute type_quotient.elim [unfold-c 6] [recursor 6] -attribute type_quotient.elim_type [unfold-c 5] -attribute type_quotient.elim_on [unfold-c 4] -attribute type_quotient.elim_type_on [unfold-c 3] diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean index 4573904a73..4eb56e024b 100644 --- a/hott/init/hit.hlean +++ b/hott/init/hit.hlean @@ -16,7 +16,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 - - type quotients (non-truncated quotients) + - quotients (non-truncated quotients) For each of the hits we add the following constants: - the type formation - the term and path constructors @@ -45,27 +45,27 @@ namespace trunc trunc.rec H aa end trunc -constant type_quotient.{u v} {A : Type.{u}} (R : A → A → Type.{v}) : Type.{max u v} +constant quotient.{u v} {A : Type.{u}} (R : A → A → Type.{v}) : Type.{max u v} -namespace type_quotient +namespace quotient - constant class_of {A : Type} (R : A → A → Type) (a : A) : type_quotient R + constant class_of {A : Type} (R : A → A → Type) (a : A) : quotient R 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' - protected constant rec {A : Type} {R : A → A → Type} {P : type_quotient R → Type} + protected constant rec {A : Type} {R : A → A → Type} {P : quotient R → Type} (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a') - (x : type_quotient R) : P x + (x : quotient R) : P x - 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)) + protected definition rec_on [reducible] {A : Type} {R : A → A → Type} {P : quotient R → Type} + (x : quotient R) (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a') : P x := - type_quotient.rec Pc Pp x + quotient.rec Pc Pp x -end type_quotient +end quotient -init_hits -- Initialize builtin computational rules for trunc and type_quotient +init_hits -- Initialize builtin computational rules for trunc and quotient namespace trunc definition rec_tr [reducible] {n : trunc_index} {A : Type} {P : trunc n A → Type} @@ -73,17 +73,17 @@ namespace trunc idp end trunc -namespace type_quotient - definition rec_class_of {A : Type} {R : A → A → Type} {P : type_quotient R → Type} +namespace quotient + definition rec_class_of {A : Type} {R : A → A → Type} {P : quotient R → Type} (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a') - (a : A) : type_quotient.rec Pc Pp (class_of R a) = Pc a := + (a : A) : quotient.rec Pc Pp (class_of R a) = Pc a := idp - constant rec_eq_of_rel {A : Type} {R : A → A → Type} {P : type_quotient R → Type} + constant rec_eq_of_rel {A : Type} {R : A → A → Type} {P : quotient R → Type} (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a') - {a a' : A} (H : R a a') : apdo (type_quotient.rec Pc Pp) (eq_of_rel R H) = Pp H -end type_quotient + {a a' : A} (H : R a a') : apdo (quotient.rec Pc Pp) (eq_of_rel R H) = Pp H +end quotient -attribute type_quotient.class_of trunc.tr [constructor] -attribute type_quotient.rec trunc.rec [unfold-c 6] -attribute type_quotient.rec_on trunc.rec_on [unfold-c 4] +attribute quotient.class_of trunc.tr [constructor] +attribute quotient.rec trunc.rec [unfold-c 6] +attribute quotient.rec_on trunc.rec_on [unfold-c 4] diff --git a/src/kernel/hits/hits.cpp b/src/kernel/hits/hits.cpp index 8c70dca73e..550a82aa27 100644 --- a/src/kernel/hits/hits.cpp +++ b/src/kernel/hits/hits.cpp @@ -14,16 +14,16 @@ Builtin HITs: #include "kernel/hits/hits.h" namespace lean { -static name * g_hits_extension = nullptr; -static name * g_trunc = nullptr; -static name * g_trunc_tr = nullptr; -static name * g_trunc_rec = nullptr; -static name * g_trunc_is_trunc_trunc = nullptr; -static name * g_type_quotient = nullptr; -static name * g_type_quotient_class_of = nullptr; -static name * g_type_quotient_rec = nullptr; -static name * g_type_quotient_eq_of_rel = nullptr; -static name * g_type_quotient_rec_eq_of_rel = nullptr; +static name * g_hits_extension = nullptr; +static name * g_trunc = nullptr; +static name * g_trunc_tr = nullptr; +static name * g_trunc_rec = nullptr; +static name * g_trunc_is_trunc_trunc = nullptr; +static name * g_hit_quotient = nullptr; +static name * g_hit_quotient_class_of = nullptr; +static name * g_hit_quotient_rec = nullptr; +static name * g_hit_quotient_eq_of_rel = nullptr; +static name * g_hit_quotient_rec_eq_of_rel = nullptr; struct hits_env_ext : public environment_extension { bool m_initialized; @@ -69,9 +69,9 @@ optional> hits_normalizer_extension::operator()(expr mk_pos = 5; mk_name = g_trunc_tr; f_pos = 4; - } else if (const_name(fn) == *g_type_quotient_rec) { + } else if (const_name(fn) == *g_hit_quotient_rec) { mk_pos = 5; - mk_name = g_type_quotient_class_of; + mk_name = g_hit_quotient_class_of; f_pos = 3; } else { return none_ecs(); @@ -106,7 +106,7 @@ optional is_hits_meta_app_core(Ctx & ctx, expr const & e) { unsigned mk_pos; if (const_name(fn) == *g_trunc_rec) { mk_pos = 5; - } else if (const_name(fn) == *g_type_quotient_rec) { + } else if (const_name(fn) == *g_hit_quotient_rec) { mk_pos = 5; } else { return none_expr(); @@ -130,7 +130,7 @@ bool hits_normalizer_extension::supports(name const & feature) const { } bool hits_normalizer_extension::is_recursor(environment const &, name const & n) const { - return n == *g_trunc_rec || n == *g_type_quotient_rec; + return n == *g_trunc_rec || n == *g_hit_quotient_rec; } bool hits_normalizer_extension::is_builtin(environment const & env, name const & n) const { @@ -143,23 +143,23 @@ bool is_hits_decl(environment const & env, name const & n) { return n == *g_trunc || n == *g_trunc_tr || n == *g_trunc_rec || n == *g_trunc_is_trunc_trunc || - n == *g_type_quotient || n == *g_type_quotient_class_of || - n == *g_type_quotient_rec || n == *g_type_quotient_eq_of_rel || - n == *g_type_quotient_rec_eq_of_rel; + n == *g_hit_quotient || n == *g_hit_quotient_class_of || + n == *g_hit_quotient_rec || n == *g_hit_quotient_eq_of_rel || + n == *g_hit_quotient_rec_eq_of_rel; } void initialize_hits_module() { - g_hits_extension = new name("hits_extension"); - g_trunc = new name{"trunc"}; - g_trunc_tr = new name{"trunc", "tr"}; - g_trunc_rec = new name{"trunc", "rec"}; - g_trunc_is_trunc_trunc = new name{"trunc", "is_trunc_trunc"}; - g_type_quotient = new name{"type_quotient"}; - g_type_quotient_class_of = new name{"type_quotient", "class_of"}; - g_type_quotient_rec = new name{"type_quotient", "rec"}; - g_type_quotient_eq_of_rel = new name{"type_quotient", "eq_of_rel"}; - g_type_quotient_rec_eq_of_rel = new name{"type_quotient", "rec_eq_of_rel"}; - g_ext = new hits_env_ext_reg(); + g_hits_extension = new name("hits_extension"); + g_trunc = new name{"trunc"}; + g_trunc_tr = new name{"trunc", "tr"}; + g_trunc_rec = new name{"trunc", "rec"}; + g_trunc_is_trunc_trunc = new name{"trunc", "is_trunc_trunc"}; + g_hit_quotient = new name{"quotient"}; + g_hit_quotient_class_of = new name{"quotient", "class_of"}; + g_hit_quotient_rec = new name{"quotient", "rec"}; + g_hit_quotient_eq_of_rel = new name{"quotient", "eq_of_rel"}; + g_hit_quotient_rec_eq_of_rel = new name{"quotient", "rec_eq_of_rel"}; + g_ext = new hits_env_ext_reg(); } void finalize_hits_module() { @@ -169,10 +169,10 @@ void finalize_hits_module() { delete g_trunc_tr; delete g_trunc_rec; delete g_trunc_is_trunc_trunc; - delete g_type_quotient; - delete g_type_quotient_class_of; - delete g_type_quotient_rec; - delete g_type_quotient_eq_of_rel; - delete g_type_quotient_rec_eq_of_rel; + delete g_hit_quotient; + delete g_hit_quotient_class_of; + delete g_hit_quotient_rec; + delete g_hit_quotient_eq_of_rel; + delete g_hit_quotient_rec_eq_of_rel; } } diff --git a/tests/lean/640.hlean b/tests/lean/640.hlean index 8cfc31f34f..b705939309 100644 --- a/tests/lean/640.hlean +++ b/tests/lean/640.hlean @@ -1,10 +1,10 @@ -import hit.type_quotient +import hit.quotient -open type_quotient eq sum +open quotient eq sum constants {A : Type} (R : A → A → Type) - local abbreviation C := type_quotient R + local abbreviation C := quotient R definition f [unfold-c 2] (a : A) (x : unit) : C := !class_of a @@ -15,7 +15,7 @@ open type_quotient eq sum set_option pp.notation false set_option pp.beta false - definition rec {P : type_quotient S → Type} (x : type_quotient S) : P x := + definition rec {P : quotient S → Type} (x : quotient S) : P x := begin induction x with c c c' H, { induction c with b b b' H, diff --git a/tests/lean/640.hlean.expected.out b/tests/lean/640.hlean.expected.out index c82f5c9bab..2a713b0fb7 100644 --- a/tests/lean/640.hlean.expected.out +++ b/tests/lean/640.hlean.expected.out @@ -1,17 +1,17 @@ 640.hlean:25:8: proof state -P : type_quotient S → Type, +P : quotient S → Type, c c' : C, a : A -⊢ pathover P (type_quotient.rec (λ (b : A), sorry) (λ (b b' : A) (H : R b b'), sorry) (f a unit.star)) +⊢ pathover P (quotient.rec (λ (b : A), sorry) (λ (b b' : A) (H : R b b'), sorry) (f a unit.star)) (eq_of_rel S (S.Rmk a unit.star)) sorry 640.hlean:25:22: proof state -P : type_quotient S → Type, +P : quotient S → Type, c c' : C, a : A ⊢ pathover P sorry (eq_of_rel S (S.Rmk a unit.star)) sorry 640.hlean:25:36: proof state -P : type_quotient S → Type, +P : quotient S → Type, c c' : C, a : A ⊢ pathover P sorry (eq_of_rel S (S.Rmk a unit.star)) sorry diff --git a/tests/lean/extra/616a.hlean b/tests/lean/extra/616a.hlean index 32edb4a9d2..0f6869261b 100644 --- a/tests/lean/extra/616a.hlean +++ b/tests/lean/extra/616a.hlean @@ -1 +1 @@ -attribute type_quotient.rec [recursor] +attribute quotient.rec [recursor] diff --git a/tests/lean/extra/616b.hlean b/tests/lean/extra/616b.hlean index 257e176c77..7416663be9 100644 --- a/tests/lean/extra/616b.hlean +++ b/tests/lean/extra/616b.hlean @@ -1,7 +1,7 @@ import .f616a open eq definition my_elim {A P : Type} {R : A → A → Type} (Pc : A → P) - (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : type_quotient R) : P := + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : quotient R) : P := begin induction x, exact (Pc a), diff --git a/tests/lean/extra/616c.hlean b/tests/lean/extra/616c.hlean index 2527a4eb55..cbb536dbfb 100644 --- a/tests/lean/extra/616c.hlean +++ b/tests/lean/extra/616c.hlean @@ -1,6 +1,6 @@ open eq definition my_elim {A P : Type} {R : A → A → Type} (Pc : A → P) - (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : type_quotient R) : P := + (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : quotient R) : P := begin induction x, exact (Pc a), diff --git a/tests/lean/hott/610.hlean b/tests/lean/hott/610.hlean index feacb7de51..b9525c4c8c 100644 --- a/tests/lean/hott/610.hlean +++ b/tests/lean/hott/610.hlean @@ -1,7 +1,7 @@ -import hit.type_quotient -attribute type_quotient.elim [recursor 6] +import hit.quotient +attribute quotient.elim [recursor 6] -definition my_elim_on {A : Type} {R : A → A → Type} {P : Type} (x : type_quotient R) +definition my_elim_on {A : Type} {R : A → A → Type} {P : Type} (x : quotient R) (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P := begin induction x, diff --git a/tests/lean/hott/ind_tac2.hlean b/tests/lean/hott/ind_tac2.hlean index 40c6f68b01..14f3137e66 100644 --- a/tests/lean/hott/ind_tac2.hlean +++ b/tests/lean/hott/ind_tac2.hlean @@ -6,8 +6,8 @@ attribute trunc.rec_on [recursor] print [recursor] trunc.rec_on -check @type_quotient.rec_on +check @quotient.rec_on -attribute type_quotient.rec_on [recursor] +attribute quotient.rec_on [recursor] -print [recursor] type_quotient.rec_on +print [recursor] quotient.rec_on