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).
This commit is contained in:
Floris van Doorn
parent
06528c4791
commit
ff01774fd7
17 changed files with 210 additions and 208 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
* [circle](circle.hlean) (defined as sphere 1)
|
||||
* [interval](interval.hlean) (defined as the suspension of unit)
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
75
hott/hit/set_quotient.hlean
Normal file
75
hott/hit/set_quotient.hlean
Normal file
|
|
@ -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]
|
||||
|
|
@ -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]
|
||||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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<pair<expr, constraint_seq>> 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<expr> 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;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
attribute type_quotient.rec [recursor]
|
||||
attribute quotient.rec [recursor]
|
||||
|
|
|
|||
|
|
@ -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),
|
||||
|
|
|
|||
|
|
@ -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),
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue