From f51353863166e53471d030518e49484ac0d94537 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 26 Feb 2015 13:19:54 -0500 Subject: [PATCH] feat(hott): more cleanup of HoTT library remove funext class, remove a couple of sorry's, add characterization of equality in trunctypes, use Jeremy's format for headers everywhere in the HoTT library, continue working on Yoneda embedding --- hott/algebra/category/basic.hlean | 84 +++++---- hott/algebra/category/constructions.hlean | 33 ++++ hott/algebra/category/set.hlean | 70 ------- hott/algebra/groupoid.hlean | 189 +++++++++++-------- hott/algebra/precategory/basic.hlean | 100 +++++----- hott/algebra/precategory/constructions.hlean | 62 +++--- hott/algebra/precategory/functor.hlean | 26 ++- hott/algebra/precategory/iso.hlean | 14 +- hott/algebra/precategory/morphism.hlean | 18 +- hott/algebra/precategory/nat_trans.hlean | 29 ++- hott/algebra/precategory/yoneda.hlean | 21 ++- hott/equiv_precomp.hlean | 3 +- hott/init/axioms/funext.hlean | 31 --- hott/init/axioms/funext_of_ua.hlean | 16 +- hott/init/axioms/funext_varieties.hlean | 18 +- hott/init/axioms/ua.hlean | 14 +- hott/init/bool.hlean | 1 + hott/init/datatypes.hlean | 1 + hott/init/default.hlean | 3 +- hott/init/equiv.hlean | 42 +++-- hott/init/function.hlean | 1 + hott/init/hedberg.hlean | 1 + hott/init/logic.hlean | 1 + hott/init/num.hlean | 1 + hott/init/path.hlean | 7 +- hott/init/priority.hlean | 1 + hott/init/relation.hlean | 1 + hott/init/reserved_notation.hlean | 1 + hott/init/tactic.hlean | 1 + hott/init/trunc.hlean | 2 +- hott/init/types/prod.hlean | 1 + hott/init/types/sigma.hlean | 1 + hott/init/types/sum.hlean | 1 + hott/init/util.hlean | 1 + hott/init/wf.hlean | 1 + hott/logic.hlean | 11 -- hott/truncation.hlean | 10 +- hott/types/W.hlean | 2 + hott/types/path.hlean | 23 ++- hott/types/pi.hlean | 7 +- hott/types/prod.hlean | 6 +- hott/types/sigma.hlean | 7 +- hott/types/trunc.hlean | 38 +++- 43 files changed, 488 insertions(+), 413 deletions(-) create mode 100644 hott/algebra/category/constructions.hlean delete mode 100644 hott/algebra/category/set.hlean delete mode 100644 hott/init/axioms/funext.hlean delete mode 100644 hott/logic.hlean diff --git a/hott/algebra/category/basic.hlean b/hott/algebra/category/basic.hlean index 01e5b8f31..7a7842fec 100644 --- a/hott/algebra/category/basic.hlean +++ b/hott/algebra/category/basic.hlean @@ -1,33 +1,45 @@ --- Copyright (c) 2014 Jakob von Raumer. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jakob von Raumer +/- +Copyright (c) 2014 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. -import ..precategory.basic ..precategory.morphism ..precategory.iso +Module: algebra.category.basic +Author: Jakob von Raumer +-/ -open precategory morphism is_equiv eq is_trunc nat sigma sigma.ops +import algebra.precategory.iso --- A category is a precategory extended by a witness, --- that the function assigning to each isomorphism a path, +open morphism is_equiv eq is_trunc + +-- A category is a precategory extended by a witness +-- that the function from paths to isomorphisms, -- is an equivalecnce. -structure category [class] (ob : Type) extends (precategory ob) := - (iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b)) - -attribute category [multiple-instances] - namespace category - variables {ob : Type} {C : category ob} {a b : ob} + + structure category [class] (ob : Type) extends parent : precategory ob := + (iso_of_path_equiv : Π (a b : ob), is_equiv (@iso_of_path ob parent a b)) + + attribute category [multiple-instances] + + abbreviation iso_of_path_equiv := @category.iso_of_path_equiv + + definition category.mk' [reducible] (ob : Type) (C : precategory ob) + (H : Π (a b : ob), is_equiv (@iso_of_path ob C a b)) : category ob := + precategory.rec_on C category.mk H + + section basic + variables {ob : Type} [C : category ob] include C -- Make iso_of_path_equiv a class instance -- TODO: Unsafe class instance? attribute iso_of_path_equiv [instance] - definition path_of_iso {a b : ob} : a ≅ b → a = b := + definition path_of_iso (a b : ob) : a ≅ b → a = b := iso_of_path⁻¹ set_option apply.class_instance false -- disable class instance resolution in the apply tactic - definition ob_1_type : is_trunc (succ nat.zero) ob := + definition ob_1_type : is_trunc 1 ob := begin apply is_trunc_succ_intro, intros (a, b), fapply is_trunc_is_equiv_closed, @@ -35,25 +47,27 @@ namespace category apply is_equiv_inv, apply is_hset_iso, end + end basic + + -- Bundled version of categories + -- we don't use Category.carrier explicitly, but rather use Precategory.carrier (to_Precategory C) + structure Category : Type := + (carrier : Type) + (struct : category carrier) + + attribute Category.struct [instance] [coercion] + -- definition objects [reducible] := Category.objects + -- definition category_instance [instance] [coercion] [reducible] := Category.category_instance + + definition Category.to_Precategory [coercion] [reducible] (C : Category) : Precategory := + Precategory.mk (Category.carrier C) C + + definition category.Mk [reducible] := Category.mk + definition category.MK [reducible] (C : Precategory) + (H : Π (a b : C), is_equiv (@iso_of_path C C a b)) : Category := + Category.mk C (category.mk' C C H) + + definition Category.eta (C : Category) : Category.mk C C = C := + Category.rec (λob c, idp) C end category - --- Bundled version of categories - -structure Category : Type := - (objects : Type) - (category_instance : category objects) - -namespace category - definition Mk {ob} (C) : Category := Category.mk ob C - --definition MK (a b c d e f g h i) : Category := Category.mk a (category.mk b c d e f g h i) - - definition objects [coercion] [reducible] := Category.objects - definition category_instance [instance] [coercion] [reducible] := Category.category_instance - -end category - -open category - -protected definition Category.eta (C : Category) : Category.mk C C = C := -Category.rec (λob c, idp) C diff --git a/hott/algebra/category/constructions.hlean b/hott/algebra/category/constructions.hlean new file mode 100644 index 000000000..e3f36d8fc --- /dev/null +++ b/hott/algebra/category/constructions.hlean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.category.constructions +Authors: Floris van Doorn +-/ + +import .basic algebra.precategory.constructions + +open eq prod eq eq.ops equiv is_trunc funext pi category.ops morphism category + +namespace category + + section hset + definition is_category_hset (a b : Precategory_hset) : is_equiv (@iso_of_path _ _ a b) := + sorry + + definition category_hset [reducible] [instance] : category hset := + category.mk' hset precategory_hset is_category_hset + + definition Category_hset [reducible] : Category := + Category.mk hset category_hset + + --RENAME AND CLEANUP + definition set_category_equiv_iso (a b : Category_hset) : (a ≅ b) = (a ≃ b) := sorry + + end hset + namespace ops + abbreviation set := Category_hset + end ops + +end category diff --git a/hott/algebra/category/set.hlean b/hott/algebra/category/set.hlean deleted file mode 100644 index 8c53ada5a..000000000 --- a/hott/algebra/category/set.hlean +++ /dev/null @@ -1,70 +0,0 @@ --- Copyright (c) 2015 Jakob von Raumer. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Authors: Jakob von Raumer --- Category of sets - -import .basic types.pi types.trunc - -open is_trunc sigma sigma.ops pi function eq morphism precategory -open equiv - -namespace precategory - - universe variable l - - definition set_precategory : precategory.{l+1 l} (Σ (A : Type.{l}), is_hset A) := - begin - fapply precategory.mk.{l+1 l}, - intros (a, a_1), apply (a.1 → a_1.1), - intros, apply is_trunc_pi, intros, apply b.2, - intros, intro x, exact (a_1 (a_2 x)), - intros, exact (λ (x : a.1), x), - intros, apply eq_of_homotopy, intro x, apply idp, - intros, apply eq_of_homotopy, intro x, apply idp, - intros, apply eq_of_homotopy, intro x, apply idp, - end - -end precategory - -namespace category - - universe variable l - local attribute precategory.set_precategory.{l+1 l} [instance] - - definition set_category_equiv_iso (a b : (Σ (A : Type.{l}), is_hset A)) - : (a ≅ b) = (a.1 ≃ b.1) := - /-begin - apply ua, fapply equiv.mk, - intro H, - apply (isomorphic.rec_on H), intros (H1, H2), - apply (is_iso.rec_on H2), intros (H3, H4, H5), - fapply equiv.mk, - apply (isomorphic.rec_on H), intros (H1, H2), - exact H1, - fapply is_equiv.adjointify, exact H3, - exact sorry, - exact sorry, - end-/ sorry - - definition set_category : category.{l+1 l} (Σ (A : Type.{l}), is_hset A) := - /-begin - assert (C : precategory.{l+1 l} (Σ (A : Type.{l}), is_hset A)), - apply precategory.set_precategory, - apply category.mk, - assert (p : (λ A B p, (set_category_equiv_iso A B) ▹ iso_of_path p) = (λ A B p, @equiv_of_eq A.1 B.1 p)), - apply is_equiv.adjointify, - intros, - apply (isomorphic.rec_on a_1), intros (iso', is_iso'), - apply (is_iso.rec_on is_iso'), intros (f', f'sect, f'retr), - fapply sigma_eq, - apply ua, fapply equiv.mk, exact iso', - fapply is_equiv.adjointify, - exact f', - intros, apply (f'retr ▹ _), - intros, apply (f'sect ▹ _), - apply (@is_hprop.elim), - apply is_hprop_is_trunc, - intros, - end -/ sorry - -end category diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean index a3e50df21..dc9eebc91 100644 --- a/hott/algebra/groupoid.hlean +++ b/hott/algebra/groupoid.hlean @@ -1,92 +1,119 @@ --- Copyright (c) 2014 Jakob von Raumer. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jakob von Raumer --- Ported from Coq HoTT -import .precategory.basic .precategory.morphism .group types.pi +/- +Copyright (c) 2014 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. -open eq function prod sigma pi is_trunc morphism nat path_algebra unit prod sigma.ops +Module: algebra.groupoid +Author: Jakob von Raumer -structure foo (A : Type) := (bsp : A) +Ported from Coq HoTT +-/ -structure groupoid [class] (ob : Type) extends parent : precategory ob := -(all_iso : Π ⦃a b : ob⦄ (f : hom a b), - @is_iso ob parent a b f) +import .precategory.morphism .group -namespace groupoid +open eq is_trunc morphism category path_algebra nat unit -attribute all_iso [instance] +namespace category -universe variable l -open precategory -definition groupoid_of_1_type (A : Type.{l}) - (H : is_trunc (nat.zero .+1) A) : groupoid.{l l} A := -groupoid.mk - (λ (a b : A), a = b) - (λ (a b : A), have ish : is_hset (a = b), from is_trunc_eq nat.zero a b, ish) - (λ (a b c : A) (p : b = c) (q : a = b), q ⬝ p) - (λ (a : A), refl a) - (λ (a b c d : A) (p : c = d) (q : b = c) (r : a = b), con.assoc r q p) - (λ (a b : A) (p : a = b), con_idp p) - (λ (a b : A) (p : a = b), idp_con p) - (λ (a b : A) (p : a = b), @is_iso.mk A _ a b p (p⁻¹) - !con.left_inv !con.right_inv) + structure groupoid [class] (ob : Type) extends parent : precategory ob := + (all_iso : Π ⦃a b : ob⦄ (f : hom a b), @is_iso ob parent a b f) --- A groupoid with a contractible carrier is a group -definition group_of_is_contr_groupoid {ob : Type} (H : is_contr ob) - (G : groupoid ob) : group (hom (center ob) (center ob)) := -begin - fapply group.mk, - intros (f, g), apply (comp f g), - apply homH, - intros (f, g, h), apply ((assoc f g h)⁻¹), - apply (ID (center ob)), - intro f, apply id_left, - intro f, apply id_right, - intro f, exact (morphism.inverse f), - intro f, exact (morphism.inverse_compose f), -end + abbreviation all_iso := @groupoid.all_iso + attribute groupoid.all_iso [instance] -definition group_of_unit_groupoid (G : groupoid unit) : group (hom ⋆ ⋆) := -begin - fapply group.mk, - intros (f, g), apply (comp f g), - apply homH, - intros (f, g, h), apply ((assoc f g h)⁻¹), - apply (ID ⋆), - intro f, apply id_left, - intro f, apply id_right, - intro f, exact (morphism.inverse f), - intro f, exact (morphism.inverse_compose f), -end + definition groupoid.mk' [reducible] (ob : Type) (C : precategory ob) + (H : Π (a b : ob) (f : a ⟶ b), is_iso f) : groupoid ob := + precategory.rec_on C groupoid.mk H --- Conversely we can turn each group into a groupoid on the unit type -definition of_group (A : Type.{l}) [G : group A] : groupoid.{l l} unit := -begin - fapply groupoid.mk, - intros, exact A, - intros, apply (@group.carrier_hset A G), - intros (a, b, c, g, h), exact (@group.mul A G g h), - intro a, exact (@group.one A G), - intros, exact ((@group.mul_assoc A G h g f)⁻¹), - intros, exact (@group.one_mul A G f), - intros, exact (@group.mul_one A G f), - intros, apply is_iso.mk, - apply mul_left_inv, - apply mul_right_inv, -end + definition groupoid_of_1_type.{l} (A : Type.{l}) + [H : is_trunc (succ zero) A] : groupoid.{l l} A := + groupoid.mk + (λ (a b : A), a = b) + (λ (a b : A), have ish : is_hset (a = b), from is_trunc_eq nat.zero a b, ish) + (λ (a b c : A) (p : b = c) (q : a = b), q ⬝ p) + (λ (a : A), refl a) + (λ (a b c d : A) (p : c = d) (q : b = c) (r : a = b), con.assoc r q p) + (λ (a b : A) (p : a = b), con_idp p) + (λ (a b : A) (p : a = b), idp_con p) + (λ (a b : A) (p : a = b), @is_iso.mk A _ a b p (p⁻¹) + !con.left_inv !con.right_inv) -protected definition hom_group {A : Type} [G : groupoid A] (a : A) : - group (hom a a) := -begin - fapply group.mk, - intros (f, g), apply (comp f g), - apply homH, - intros (f, g, h), apply ((assoc f g h)⁻¹), - apply (ID a), - intro f, apply id_left, - intro f, apply id_right, - intro f, exact (morphism.inverse f), - intro f, exact (morphism.inverse_compose f), -end + -- A groupoid with a contractible carrier is a group + definition group_of_is_contr_groupoid {ob : Type} [H : is_contr ob] + [G : groupoid ob] : group (hom (center ob) (center ob)) := + begin + fapply group.mk, + intros (f, g), apply (comp f g), + apply homH, + intros (f, g, h), apply ((assoc f g h)⁻¹), + apply (ID (center ob)), + intro f, apply id_left, + intro f, apply id_right, + intro f, exact (morphism.inverse f), + intro f, exact (morphism.inverse_compose f), + end -end groupoid + definition group_of_unit_groupoid [G : groupoid unit] : group (hom ⋆ ⋆) := + begin + fapply group.mk, + intros (f, g), apply (comp f g), + apply homH, + intros (f, g, h), apply ((assoc f g h)⁻¹), + apply (ID ⋆), + intro f, apply id_left, + intro f, apply id_right, + intro f, exact (morphism.inverse f), + intro f, exact (morphism.inverse_compose f), + end + + -- Conversely we can turn each group into a groupoid on the unit type + definition of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{l l} unit := + begin + fapply groupoid.mk, + intros, exact A, + intros, apply (@group.carrier_hset A G), + intros (a, b, c, g, h), exact (@group.mul A G g h), + intro a, exact (@group.one A G), + intros, exact ((@group.mul_assoc A G h g f)⁻¹), + intros, exact (@group.one_mul A G f), + intros, exact (@group.mul_one A G f), + intros, apply is_iso.mk, + apply mul_left_inv, + apply mul_right_inv, + end + + protected definition hom_group {A : Type} [G : groupoid A] (a : A) : + group (hom a a) := + begin + fapply group.mk, + intros (f, g), apply (comp f g), + apply homH, + intros (f, g, h), apply ((assoc f g h)⁻¹), + apply (ID a), + intro f, apply id_left, + intro f, apply id_right, + intro f, exact (morphism.inverse f), + intro f, exact (morphism.inverse_compose f), + end + + -- Bundled version of categories + -- we don't use Groupoid.carrier explicitly, but rather use Groupoid.carrier (to_Precategory C) + structure Groupoid : Type := + (carrier : Type) + (struct : groupoid carrier) + + attribute Groupoid.struct [instance] [coercion] + -- definition objects [reducible] := Category.objects + -- definition category_instance [instance] [coercion] [reducible] := Category.category_instance + + definition Groupoid.to_Precategory [coercion] [reducible] (C : Groupoid) : Precategory := + Precategory.mk (Groupoid.carrier C) C + + definition groupoid.Mk [reducible] := Groupoid.mk + definition category.MK [reducible] (C : Precategory) (H : Π (a b : C) (f : a ⟶ b), is_iso f) + : Groupoid := + Groupoid.mk C (groupoid.mk' C C H) + + definition Groupoid.eta (C : Groupoid) : Groupoid.mk C C = C := + Groupoid.rec (λob c, idp) C + +end category diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean index 6cc2e55ad..051ad9a8d 100644 --- a/hott/algebra/precategory/basic.hlean +++ b/hott/algebra/precategory/basic.hlean @@ -1,46 +1,57 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.precategory.basic +Authors: Floris van Doorn +-/ open eq is_trunc -structure precategory [class] (ob : Type) : Type := - (hom : ob → ob → Type) - (homH : Π {a b : ob}, is_hset (hom a b)) - (comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c) - (ID : Π (a : ob), hom a a) - (assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b), - comp h (comp g f) = comp (comp h g) f) - (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f) - (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f) +namespace category -attribute precategory [multiple-instances] + structure precategory [class] (ob : Type) : Type := + (hom : ob → ob → Type) + (homH : Π(a b : ob), is_hset (hom a b)) + (comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c) + (ID : Π (a : ob), hom a a) + (assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b), + comp h (comp g f) = comp (comp h g) f) + (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f) + (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f) -namespace precategory - variables {ob : Type} [C : precategory ob] - variables {a b c d : ob} - include C - attribute homH [instance] + attribute precategory [multiple-instances] + attribute precategory.homH [instance] - definition compose [reducible] := comp - - definition id [reducible] {a : ob} : hom a a := ID a - - infixr `∘` := comp - infixl [parsing-only] `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→)) + infixr `∘` := precategory.comp + -- input ⟶ using \--> (this is a different arrow than \-> (→)) + infixl [parsing-only] `⟶`:25 := precategory.hom namespace hom - infixl `⟶` := hom -- if you open this namespace, hom a b is printed as a ⟶ b + infixl `⟶` := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b end hom - variables {h : hom c d} {g : hom b c} {f f' : hom a b} {i : hom a a} + abbreviation hom := @precategory.hom + abbreviation homH := @precategory.homH + abbreviation comp := @precategory.comp + abbreviation ID := @precategory.ID + abbreviation assoc := @precategory.assoc + abbreviation id_left := @precategory.id_left + abbreviation id_right := @precategory.id_right - theorem id_compose (a : ob) : ID a ∘ ID a = ID a := !id_left + section basic_lemmas + variables {ob : Type} [C : precategory ob] + variables {a b c d : ob} {h : c ⟶ d} {g : hom b c} {f f' : hom a b} {i : a ⟶ a} + include C - theorem left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id := + definition id [reducible] := ID a + + definition id_compose (a : ob) : ID a ∘ ID a = ID a := !id_left + + definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id := calc i = i ∘ id : id_right ... = id : H - theorem right_id_unique (H : Π{b} {f : hom a b}, f ∘ i = f) : i = id := + definition right_id_unique (H : Π{b} {f : hom a b}, f ∘ i = f) : i = id := calc i = id ∘ i : id_left ... = id : H @@ -49,26 +60,29 @@ namespace precategory definition is_hprop_eq_hom [instance] : is_hprop (f = f') := !is_trunc_eq + end basic_lemmas -end precategory + structure Precategory : Type := + (carrier : Type) + (struct : precategory carrier) -structure Precategory : Type := - (objects : Type) - (category_instance : precategory objects) + definition precategory.Mk [reducible] {ob} (C) : Precategory := Precategory.mk ob C + definition precategory.MK [reducible] (a b c d e f g h) : Precategory := + Precategory.mk a (precategory.mk b c d e f g h) -namespace precategory - definition Mk {ob} (C) : Precategory := Precategory.mk ob C - definition MK (a b c d e f g h) : Precategory := Precategory.mk a (precategory.mk b c d e f g h) + abbreviation carrier := @Precategory.carrier - definition objects [coercion] [reducible] := Precategory.objects - definition category_instance [instance] [coercion] [reducible] := Precategory.category_instance - notation g `∘⁅` C `⁆` f := @compose (objects C) (category_instance C) _ _ _ g f + attribute Precategory.carrier [coercion] + attribute Precategory.struct [instance] [priority 10000] [coercion] + -- definition precategory.carrier [coercion] [reducible] := Precategory.carrier + -- definition precategory.struct [instance] [coercion] [reducible] := Precategory.struct + notation g `∘⁅` C `⁆` f := @comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f -- TODO: make this left associative -- TODO: change this notation? -end precategory + definition Precategory.eta (C : Precategory) : Precategory.mk C C = C := + Precategory.rec (λob c, idp) C -open precategory +end category -protected definition Precategory.eta (C : Precategory) : Precategory.mk C C = C := -Precategory.rec (λob c, idp) C +open category diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean index 7d328e2bb..30392d97c 100644 --- a/hott/algebra/precategory/constructions.hlean +++ b/hott/algebra/precategory/constructions.hlean @@ -13,27 +13,27 @@ import types.prod types.sigma types.pi open eq prod eq eq.ops equiv is_trunc -namespace precategory +namespace category namespace opposite definition opposite [reducible] {ob : Type} (C : precategory ob) : precategory ob := - mk (λ a b, hom b a) - (λ b a, !homH) - (λ a b c f g, g ∘ f) - (λ a, id) - (λ a b c d f g h, !assoc⁻¹) - (λ a b f, !id_right) - (λ a b f, !id_left) + precategory.mk (λ a b, hom b a) + (λ a b, !homH) + (λ a b c f g, g ∘ f) + (λ a, id) + (λ a b c d f g h, !assoc⁻¹) + (λ a b f, !id_right) + (λ a b f, !id_left) - definition Opposite [reducible] (C : Precategory) : Precategory := Mk (opposite C) + definition Opposite [reducible] (C : Precategory) : Precategory := precategory.Mk (opposite C) - infixr `∘op`:60 := @compose _ (opposite _) _ _ _ + infixr `∘op`:60 := @comp _ (opposite _) _ _ _ variables {C : Precategory} {a b c : C} set_option apply.class_instance false -- disable class instance resolution in the apply tactic - theorem compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := idp + definition compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := idp -- TODO: Decide whether just to use funext for this theorem or -- take the trick they use in Coq-HoTT, and introduce a further @@ -91,17 +91,18 @@ namespace precategory section open prod is_trunc - definition prod_precategory [reducible] [instance] {obC obD : Type} (C : precategory obC) (D : precategory obD) + definition prod_precategory [reducible] {obC obD : Type} (C : precategory obC) (D : precategory obD) : precategory (obC × obD) := - mk (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b)) - (λ a b, !is_trunc_prod) - (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) ) - (λ a, (id, id)) - (λ a b c d h g f, pair_eq !assoc !assoc ) - (λ a b f, prod_eq !id_left !id_left ) - (λ a b f, prod_eq !id_right !id_right) + precategory.mk (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b)) + (λ a b, !is_trunc_prod) + (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) ) + (λ a, (id, id)) + (λ a b c d h g f, pair_eq !assoc !assoc ) + (λ a b f, prod_eq !id_left !id_left ) + (λ a b f, prod_eq !id_right !id_right) - definition Prod_precategory [reducible] (C D : Precategory) : Precategory := Mk (prod_precategory C D) + definition Prod_precategory [reducible] (C D : Precategory) : Precategory := + precategory.Mk (prod_precategory C D) end end product @@ -113,8 +114,6 @@ namespace precategory infixr `×c`:30 := product.Prod_precategory --instance [persistent] type_category category_one -- category_two product.prod_category - attribute product.prod_precategory [instance] - end ops open ops @@ -156,16 +155,16 @@ namespace precategory open morphism functor nat_trans definition precategory_functor [instance] [reducible] (C D : Precategory) : precategory (functor C D) := - mk (λa b, nat_trans a b) - (λ a b, @nat_trans.to_hset C D a b) - (λ a b c g f, nat_trans.compose g f) - (λ a, nat_trans.id) - (λ a b c d h g f, !nat_trans.assoc) - (λ a b f, !nat_trans.id_left) - (λ a b f, !nat_trans.id_right) + precategory.mk (λa b, nat_trans a b) + (λ a b, @nat_trans.to_hset C D a b) + (λ a b c g f, nat_trans.compose g f) + (λ a, nat_trans.id) + (λ a b c d h g f, !nat_trans.assoc) + (λ a b f, !nat_trans.id_left) + (λ a b f, !nat_trans.id_right) definition Precategory_functor [reducible] (C D : Precategory) : Precategory := - Mk (precategory_functor C D) + precategory.Mk (precategory_functor C D) definition Precategory_functor_rev [reducible] (C D : Precategory) : Precategory := Precategory_functor D C @@ -206,11 +205,10 @@ namespace precategory end precategory_functor namespace ops - abbreviation set := Precategory_hset infixr `^c`:35 := Precategory_functor_rev infixr `×f`:30 := product.prod_functor infixr `ᵒᵖᶠ`:(max+1) := opposite.opposite_functor end ops -end precategory +end category diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index 7cc58e7f8..007bdda2b 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/hott/algebra/precategory/functor.hlean @@ -1,10 +1,14 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Authors: Floris van Doorn, Jakob von Raumer +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.precategory.functor +Authors: Floris van Doorn, Jakob von Raumer +-/ import .basic types.pi -open function precategory eq prod equiv is_equiv sigma sigma.ops is_trunc funext +open function category eq prod equiv is_equiv sigma sigma.ops is_trunc funext open pi structure functor (C D : Precategory) : Type := @@ -134,7 +138,7 @@ namespace functor end protected definition strict_cat_has_functor_hset - [HD : is_hset (objects D)] : is_hset (functor C D) := + [HD : is_hset D] : is_hset (functor C D) := begin apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv, apply sigma_char, @@ -151,10 +155,12 @@ namespace functor end functor -namespace precategory + +namespace category open functor - definition precat_of_strict_precats : precategory (Σ (C : Precategory), is_hset (objects C)) := + --TODO: make this a structure + definition precat_of_strict_precats : precategory (Σ (C : Precategory), is_hset C) := precategory.mk (λ a b, functor a.1 b.1) (λ a b, @functor.strict_cat_has_functor_hset a.1 b.1 b.2) (λ a b c g f, functor.compose g f) @@ -163,13 +169,13 @@ namespace precategory (λ a b f, !functor.id_left) (λ a b f, !functor.id_right) - definition Precat_of_strict_cats := Mk precat_of_strict_precats + definition Precat_of_strict_cats := precategory.Mk precat_of_strict_precats namespace ops abbreviation PreCat := Precat_of_strict_cats - attribute precat_of_strict_precats [instance] + --attribute precat_of_strict_precats [instance] end ops -end precategory +end category diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean index 6f42ea898..75f6e6184 100644 --- a/hott/algebra/precategory/iso.hlean +++ b/hott/algebra/precategory/iso.hlean @@ -1,10 +1,14 @@ --- Copyright (c) 2014 Jakob von Raumer. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Authors: Floris van Doorn, Jakob von Raumer +/- +Copyright (c) 2014 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.precategory.iso +Authors: Floris van Doorn, Jakob von Raumer +-/ import .basic .morphism types.sigma -open eq precategory sigma sigma.ops equiv is_equiv function is_trunc +open eq category sigma sigma.ops equiv is_equiv function is_trunc open prod namespace morphism @@ -62,7 +66,7 @@ namespace morphism end -- In a precategory, equal objects are isomorphic - definition iso_of_path (p : a = b) : isomorphic a b := + definition iso_of_path (p : a = b) : a ≅ b := eq.rec_on p (isomorphic.mk id) end morphism diff --git a/hott/algebra/precategory/morphism.hlean b/hott/algebra/precategory/morphism.hlean index b6eee3aa1..49802096c 100644 --- a/hott/algebra/precategory/morphism.hlean +++ b/hott/algebra/precategory/morphism.hlean @@ -1,14 +1,20 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Authors: Floris van Doorn, Jakob von Raumer +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.precategory.morphism +Authors: Floris van Doorn, Jakob von Raumer +-/ import .basic -open eq precategory sigma sigma.ops equiv is_equiv function is_trunc +open eq category sigma sigma.ops equiv is_equiv function is_trunc namespace morphism - variables {ob : Type} [C : precategory ob] include C + variables {ob : Type} [C : precategory ob] variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a} + include C + inductive is_section [class] (f : a ⟶ b) : Type := mk : ∀{g}, g ∘ f = id → is_section f inductive is_retraction [class] (f : a ⟶ b) : Type @@ -80,7 +86,7 @@ namespace morphism theorem inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' := inverse_eq_intro_left !inverse_compose - theorem inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ = f := + theorem inverse_involutive (f : a ⟶ b) [H1 : is_iso f] [H2 : is_iso (f⁻¹)] : (f⁻¹)⁻¹ = f := inverse_eq_intro_right !inverse_compose theorem retraction_of_id : retraction_of (ID a) = id := diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean index e578a0891..500d552a8 100644 --- a/hott/algebra/precategory/nat_trans.hlean +++ b/hott/algebra/precategory/nat_trans.hlean @@ -1,25 +1,24 @@ --- Copyright (c) 2014 Floris van Doorn. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Floris van Doorn, Jakob von Raumer +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: algebra.precategory.nat_trans +Author: Floris van Doorn, Jakob von Raumer +-/ import .functor .morphism -open eq precategory functor is_trunc equiv sigma.ops sigma is_equiv function pi funext +open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext -inductive nat_trans {C D : Precategory} (F G : C ⇒ D) : Type := -mk : Π (η : Π (a : C), hom (F a) (G a)) - (nat : Π {a b : C} (f : hom a b), G f ∘ η a = η b ∘ F f), - nat_trans F G +structure nat_trans {C D : Precategory} (F G : C ⇒ D) := + (natural_map : Π (a : C), hom (F a) (G a)) + (naturality : Π {a b : C} (f : hom a b), G f ∘ natural_map a = natural_map b ∘ F f) namespace nat_trans infixl `⟹`:25 := nat_trans -- \==> variables {C D : Precategory} {F G H I : C ⇒ D} - definition natural_map [coercion] (η : F ⟹ G) : Π (a : C), F a ⟶ G a := - nat_trans.rec (λ x y, x) η - - theorem naturality (η : F ⟹ G) : Π⦃a b : C⦄ (f : a ⟶ b), G f ∘ η a = η b ∘ F f := - nat_trans.rec (λ x y, y) η + attribute natural_map [coercion] protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := nat_trans.mk @@ -84,10 +83,10 @@ namespace nat_trans begin apply is_trunc_is_equiv_closed, apply (equiv.to_is_equiv !sigma_char), apply is_trunc_sigma, - apply is_trunc_pi, intro a, exact (@homH (objects D) _ (F a) (G a)), + apply is_trunc_pi, intro a, exact (@homH (Precategory.carrier D) _ (F a) (G a)), intro η, apply is_trunc_pi, intro a, apply is_trunc_pi, intro b, apply is_trunc_pi, intro f, - apply is_trunc_eq, apply is_trunc_succ, exact (@homH (objects D) _ (F a) (G b)), + apply is_trunc_eq, apply is_trunc_succ, exact (@homH (Precategory.carrier D) _ (F a) (G b)), end end nat_trans diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean index df6ab1215..200025792 100644 --- a/hott/algebra/precategory/yoneda.hlean +++ b/hott/algebra/precategory/yoneda.hlean @@ -7,22 +7,23 @@ Author: Floris van Doorn -/ --note: modify definition in category.set -import .constructions .morphism +import algebra.category.constructions .morphism -open eq precategory functor is_trunc equiv is_equiv pi -open is_trunc.trunctype funext precategory.ops prod.ops +open category eq category.ops functor prod.ops is_trunc set_option pp.beta true - namespace yoneda set_option class.conservative false - definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C} (f1 : a5 ⟶ a6) (f2 : a4 ⟶ a5) (f3 : a3 ⟶ a4) (f4 : a2 ⟶ a3) (f5 : a1 ⟶ a2) : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 := + --TODO: why does this take so much steps? (giving more information than "assoc" hardly helps) + definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C} + (f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2) + : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 := calc - (f1 ∘ f2) ∘ f3 ∘ f4 ∘ f5 = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5 : assoc - ... = f1 ∘ (f2 ∘ f3) ∘ f4 ∘ f5 : assoc - ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : assoc - ... = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 : assoc + _ = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5 : assoc + ... = f1 ∘ (f2 ∘ f3) ∘ f4 ∘ f5 : assoc + ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : assoc + ... = _ : assoc --disturbing behaviour: giving the type of f "(x ⟶ y)" explicitly makes the unifier loop definition representable_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set := @@ -37,7 +38,7 @@ namespace yoneda end yoneda - +open is_equiv equiv namespace functor open prod nat_trans diff --git a/hott/equiv_precomp.hlean b/hott/equiv_precomp.hlean index cc3ded13d..6dc438e8f 100644 --- a/hott/equiv_precomp.hlean +++ b/hott/equiv_precomp.hlean @@ -7,7 +7,8 @@ Author: Jakob von Raumer Ported from Coq HoTT -/ -exit + +-- This file is nowhere used. Do we want to keep it? open eq function funext namespace is_equiv diff --git a/hott/init/axioms/funext.hlean b/hott/init/axioms/funext.hlean deleted file mode 100644 index 61bbda69c..000000000 --- a/hott/init/axioms/funext.hlean +++ /dev/null @@ -1,31 +0,0 @@ --- Copyright (c) 2014 Microsoft Corporation. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad, Jakob von Raumer --- Ported from Coq HoTT -prelude -import ..path ..equiv -open eq - --- Funext --- ------ - --- Define function extensionality as a type class --- structure funext [class] : Type := --- (elim : Π (A : Type) (P : A → Type ) (f g : Π x, P x), is_equiv (@apD10 A P f g)) --- set_option pp.universes true --- check @funext.mk --- check @funext.elim -exit - -namespace funext - - attribute elim [instance] - - definition eq_of_homotopy [F : funext] {A : Type} {P : A → Type} {f g : Π x, P x} : f ∼ g → f = g := - is_equiv.inv (@apD10 A P f g) - - definition eq_of_homotopy2 [F : funext] {A B : Type} {P : A → B → Type} - (f g : Πx y, P x y) : (Πx y, f x y = g x y) → f = g := - λ E, eq_of_homotopy (λx, eq_of_homotopy (E x)) - -end funext diff --git a/hott/init/axioms/funext_of_ua.hlean b/hott/init/axioms/funext_of_ua.hlean index a4900e33e..3be24218e 100644 --- a/hott/init/axioms/funext_of_ua.hlean +++ b/hott/init/axioms/funext_of_ua.hlean @@ -1,10 +1,16 @@ --- Copyright (c) 2014 Jakob von Raumer. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jakob von Raumer --- Ported from Coq HoTT +/- +Copyright (c) 2014 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: init.axioms.funext_of_ua +Author: Jakob von Raumer + +Ported from Coq HoTT +-/ + prelude import ..equiv ..datatypes ..types.prod -import .funext_varieties .ua .funext +import .funext_varieties .ua open eq function prod is_trunc sigma equiv is_equiv unit diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean index 1be1e94e7..776a8bf01 100644 --- a/hott/init/axioms/funext_varieties.hlean +++ b/hott/init/axioms/funext_varieties.hlean @@ -1,9 +1,15 @@ --- Copyright (c) 2014 Jakob von Raumer. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Authors: Jakob von Raumer --- Ported from Coq HoTT +/- +Copyright (c) 2014 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: init.axioms.funext_varieties +Authors: Jakob von Raumer + +Ported from Coq HoTT +-/ + prelude -import ..path ..trunc ..equiv .funext +import ..path ..trunc ..equiv open eq is_trunc sigma function @@ -46,7 +52,7 @@ definition weak_funext_of_naive_funext : naive_funext → weak_funext := context universes l k - parameters (wf : weak_funext.{l k}) {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x) + parameters [wf : weak_funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x) definition is_contr_sigma_homotopy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) := is_contr.mk (sigma.mk f (homotopy.refl f)) diff --git a/hott/init/axioms/ua.hlean b/hott/init/axioms/ua.hlean index 9379e5a31..5c4dca18f 100644 --- a/hott/init/axioms/ua.hlean +++ b/hott/init/axioms/ua.hlean @@ -1,7 +1,13 @@ --- Copyright (c) 2014 Jakob von Raumer. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jakob von Raumer --- Ported from Coq HoTT +/- +Copyright (c) 2014 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: init.axioms.ua +Author: Jakob von Raumer + +Ported from Coq HoTT +-/ + prelude import ..path ..equiv open eq equiv is_equiv diff --git a/hott/init/bool.hlean b/hott/init/bool.hlean index 38ca46b77..a2310e8ac 100644 --- a/hott/init/bool.hlean +++ b/hott/init/bool.hlean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.bool Author: Leonardo de Moura -/ + prelude import init.datatypes init.reserved_notation diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean index b9fa335ec..bd07460a9 100644 --- a/hott/init/datatypes.hlean +++ b/hott/init/datatypes.hlean @@ -7,6 +7,7 @@ Authors: Leonardo de Moura, Jakob von Raumer Basic datatypes -/ + prelude notation [parsing-only] `Type'` := Type.{_+1} notation [parsing-only] `Type₊` := Type.{_+1} diff --git a/hott/init/default.hlean b/hott/init/default.hlean index 90835e8c9..9da50a761 100644 --- a/hott/init/default.hlean +++ b/hott/init/default.hlean @@ -5,10 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.default Authors: Leonardo de Moura, Jakob von Raumer -/ + prelude import init.datatypes init.reserved_notation init.tactic init.logic import init.bool init.num init.priority init.relation init.wf import init.types.sigma init.types.prod init.types.empty import init.trunc init.path init.equiv init.util -import init.axioms.ua init.axioms.funext init.axioms.funext_of_ua +import init.axioms.ua init.axioms.funext_of_ua import init.hedberg init.nat diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index d402f2618..af41e6108 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -218,37 +218,45 @@ end is_equiv open is_equiv namespace equiv - + namespace ops + attribute to_fun [coercion] + end ops + open equiv.ops attribute to_is_equiv [instance] infix `≃`:25 := equiv - context - parameters {A B C : Type} (eqf : A ≃ B) + variables {A B C : Type} - private definition f : A → B := to_fun eqf - private definition Hf [instance] : is_equiv f := to_is_equiv eqf + protected definition MK (f : A → B) (g : B → A) (retr : f ∘ g ∼ id) (sect : g ∘ f ∼ id) : A ≃ B := + equiv.mk f (adjointify f g retr sect) + definition to_inv (f : A ≃ B) : B → A := + f⁻¹ - protected definition refl : A ≃ A := equiv.mk id is_equiv.is_equiv_id + protected definition refl : A ≃ A := + equiv.mk id !is_equiv_id - definition trans (eqg: B ≃ C) : A ≃ C := - equiv.mk ((to_fun eqg) ∘ f) - (is_equiv_compose f (to_fun eqg)) + protected definition symm (f : A ≃ B) : B ≃ A := + equiv.mk (f⁻¹) !is_equiv_inv - definition equiv_of_eq_of_equiv (f' : A → B) (Heq : to_fun eqf = f') : A ≃ B := - equiv.mk f' (is_equiv.is_equiv_eq_closed f Heq) + protected definition trans (f : A ≃ B) (g: B ≃ C) : A ≃ C := + equiv.mk (g ∘ f) !is_equiv_compose - definition symm : B ≃ A := - equiv.mk (is_equiv.inv f) !is_equiv.is_equiv_inv + definition equiv_of_eq_of_equiv (f : A ≃ B) (f' : A → B) (Heq : f = f') : A ≃ B := + equiv.mk f' (is_equiv_eq_closed f Heq) - definition equiv_ap (P : A → Type) {x y : A} {p : x = y} : (P x) ≃ (P y) := - equiv.mk (eq.transport P p) (is_equiv_tr P p) + definition eq_equiv_fn_eq (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) := + equiv.mk (ap f) !is_equiv_ap - end + definition eq_equiv_fn_eq_of_equiv (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) := + equiv.mk (ap f) !is_equiv_ap + + definition equiv_ap (P : A → Type) {a b : A} (p : a = b) : (P a) ≃ (P b) := + equiv.mk (transport P p) !is_equiv_tr --we need this theorem for the funext_of_ua proof theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ := - eq.rec_on p idp + eq.rec_on p idp -- calc enviroment -- Note: Calculating with substitutions needs univalence diff --git a/hott/init/function.hlean b/hott/init/function.hlean index c31852931..803f1aea3 100644 --- a/hott/init/function.hlean +++ b/hott/init/function.hlean @@ -7,6 +7,7 @@ Author: Leonardo de Moura General operations on functions. -/ + prelude import init.reserved_notation diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean index 55906d24b..f22be3193 100644 --- a/hott/init/hedberg.hlean +++ b/hott/init/hedberg.hlean @@ -6,6 +6,7 @@ Author: Leonardo de Moura Hedberg's Theorem: every type with decidable equality is a hset -/ + prelude import init.trunc open eq eq.ops nat is_trunc sigma diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 655b148ec..1c8972d9a 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.logic Authors: Leonardo de Moura -/ + prelude import init.datatypes init.reserved_notation diff --git a/hott/init/num.hlean b/hott/init/num.hlean index c2d8d9bd4..c5142ffa0 100644 --- a/hott/init/num.hlean +++ b/hott/init/num.hlean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module init.num Authors: Leonardo de Moura -/ + prelude import init.logic init.bool open bool diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 8f3746e26..9bd2d1a55 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -3,7 +3,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Module: init.path -Author: Jeremy Avigad, Jakob von Raumer +Author: Jeremy Avigad, Jakob von Raumer, Floris van Doorn Ported from Coq HoTT -/ @@ -549,10 +549,10 @@ namespace eq -- Unwhiskering, a.k.a. cancelling definition cancel_left {x y z : A} (p : x = y) (q r : y = z) : (p ⬝ q = p ⬝ r) → (q = r) := - eq.rec_on p (take r, eq.rec_on r (take q a, (idp_con q)⁻¹ ⬝ a)) r q + eq.rec_on p (λq r s, !idp_con⁻¹ ⬝ s ⬝ !idp_con) q r definition cancel_right {x y z : A} (p q : x = y) (r : y = z) : (p ⬝ r = q ⬝ r) → (p = q) := - eq.rec_on r (eq.rec_on p (take q a, a ⬝ con_idp q)) q + eq.rec_on r (λs, !con_idp⁻¹ ⬝ s ⬝ !con_idp) -- Whiskering and identity paths. @@ -580,7 +580,6 @@ namespace eq idp ◾ h = whisker_left idp h :> (idp ⬝ p = idp ⬝ q) := eq.rec_on h idp - -- TODO: note, 4 inductions -- The interchange law for concatenation. definition con2_con_con2 {p p' p'' : x = y} {q q' q'' : y = z} (a : p = p') (b : p' = p'') (c : q = q') (d : q' = q'') : diff --git a/hott/init/priority.hlean b/hott/init/priority.hlean index 705ecd779..01d5fcffd 100644 --- a/hott/init/priority.hlean +++ b/hott/init/priority.hlean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.priority Authors: Leonardo de Moura -/ + prelude import init.datatypes definition std.priority.default : num := 1000 diff --git a/hott/init/relation.hlean b/hott/init/relation.hlean index c7ef20ae0..e68f545cb 100644 --- a/hott/init/relation.hlean +++ b/hott/init/relation.hlean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.relation Authors: Leonardo de Moura -/ + prelude import init.logic diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean index a3ffbb31d..b89770425 100644 --- a/hott/init/reserved_notation.hlean +++ b/hott/init/reserved_notation.hlean @@ -7,6 +7,7 @@ Authors: Leonardo de Moura Basic datatypes -/ + prelude import init.datatypes diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index fa8b79600..a568012e8 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -10,6 +10,7 @@ expression. We should view 'tactic' as automation that when execute produces a term. tactic.builtin is just a "dummy" for creating the definitions that are actually implemented in C++ -/ + prelude import init.datatypes init.reserved_notation diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index fbbda02d3..71c218935 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -196,7 +196,7 @@ namespace is_trunc notation n `-Type` := trunctype n abbreviation hprop := -1-Type - abbreviation hset := (-1.+1)-Type + abbreviation hset := 0-Type protected definition hprop.mk := @trunctype.mk -1 protected definition hset.mk := @trunctype.mk (-1.+1) diff --git a/hott/init/types/prod.hlean b/hott/init/types/prod.hlean index 4df8007d2..77885a0ee 100644 --- a/hott/init/types/prod.hlean +++ b/hott/init/types/prod.hlean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.types.prod Author: Leonardo de Moura, Jeremy Avigad -/ + prelude import ..wf ..num diff --git a/hott/init/types/sigma.hlean b/hott/init/types/sigma.hlean index c09367b15..53d2600ab 100644 --- a/hott/init/types/sigma.hlean +++ b/hott/init/types/sigma.hlean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.types.sigma Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -/ + prelude import init.num diff --git a/hott/init/types/sum.hlean b/hott/init/types/sum.hlean index abf0c335d..231aacada 100644 --- a/hott/init/types/sum.hlean +++ b/hott/init/types/sum.hlean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.types.sum Author: Leonardo de Moura, Jeremy Avigad -/ + prelude import init.datatypes init.reserved_notation diff --git a/hott/init/util.hlean b/hott/init/util.hlean index 259d755f5..650904a28 100644 --- a/hott/init/util.hlean +++ b/hott/init/util.hlean @@ -7,6 +7,7 @@ Author: Leonardo de Moura Auxiliary definitions used by automation -/ + prelude import init.trunc diff --git a/hott/init/wf.hlean b/hott/init/wf.hlean index 9928e15b3..79ae373f5 100644 --- a/hott/init/wf.hlean +++ b/hott/init/wf.hlean @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Module: init.wf Author: Leonardo de Moura -/ + prelude import init.relation init.tactic diff --git a/hott/logic.hlean b/hott/logic.hlean deleted file mode 100644 index 879fbb80d..000000000 --- a/hott/logic.hlean +++ /dev/null @@ -1,11 +0,0 @@ -exit ---javra: Maybe this should go somewhere else - -open eq - -inductive tdecidable [class] (A : Type) : Type := -inl : A → tdecidable A, -inr : ¬A → tdecidable A - -structure decidable_paths [class] (A : Type) := -(elim : ∀(x y : A), tdecidable (x = y)) diff --git a/hott/truncation.hlean b/hott/truncation.hlean index 696594d23..7dbafdd5c 100644 --- a/hott/truncation.hlean +++ b/hott/truncation.hlean @@ -1,6 +1,10 @@ --- Copyright (c) 2014 Jakob von Raumer. All rights reserved. --- Released under Apache 2.0 license as described in the file LICENSE. --- Authors: Jakob von Raumer +/- +Copyright (c) 2014 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Module: truncation +Authors: Jakob von Raumer +-/ open is_trunc diff --git a/hott/types/W.hlean b/hott/types/W.hlean index 057dcc133..8f2abbc0d 100644 --- a/hott/types/W.hlean +++ b/hott/types/W.hlean @@ -1,6 +1,8 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. + +Module: types.W Author: Floris van Doorn Theorems about W-types (well-founded trees) diff --git a/hott/types/path.hlean b/hott/types/path.hlean index 468e3f726..9f994a9dc 100644 --- a/hott/types/path.hlean +++ b/hott/types/path.hlean @@ -1,9 +1,11 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Floris van Doorn -Ported from Coq HoTT +Module: types.path +Author: Floris van Doorn + +Ported from Coq HoTT Theorems about path types (identity types) -/ @@ -133,11 +135,18 @@ namespace path equiv.trans (equiv_concat_l p a3) (equiv_concat_r q a2) /- BELOW STILL NEEDS TO BE PORTED FROM COQ HOTT -/ - - -- definition isequiv_whiskerL [instance] (p : a1 = a2) (q r : a2 = a3) - -- : is_equiv (@whisker_left A a1 a2 a3 p q r) := - -- begin - +-- set_option pp.beta true +-- check @cancel_left +-- set_option pp.full_names true +-- definition isequiv_whiskerL [instance] (p : a1 = a2) (q r : a2 = a3) +-- : is_equiv (@whisker_left A a1 a2 a3 p q r) := +-- begin +-- fapply adjointify, +-- intro H, apply (!cancel_left H), +-- intro s, esimp {function.compose, function.id}, unfold eq.cancel_left, +-- -- reverts (q,r,a), apply (eq.rec_on p), esimp {whisker_left,concat2, idp, cancel_left, eq.rec_on}, intros, esimp, +-- end +-- check @whisker_right_con_whisker_left -- end -- /-begin -- refine (isequiv_adjointify _ _ _ _). diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 836ea1eb0..97a640f38 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -1,11 +1,14 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Floris van Doorn -Ported from Coq HoTT +Module: types.pi +Author: Floris van Doorn + +Ported from Coq HoTT Theorems about pi-types (dependent function spaces) -/ + import types.sigma open eq equiv is_equiv funext diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index c84905a49..6fc6197a1 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -1,9 +1,11 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Floris van Doorn -Ported from Coq HoTT +Module: types.prod +Author: Floris van Doorn + +Ported from Coq HoTT Theorems about products -/ diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index ff22e89a0..a81c02dc0 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -1,11 +1,14 @@ /- Copyright (c) 2014 Floris van Doorn. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Floris van Doorn -Ported from Coq HoTT +Module: types.sigma +Author: Floris van Doorn + +Ported from Coq HoTT Theorems about sigma-types (dependent sums) -/ + import types.prod open eq sigma sigma.ops equiv is_equiv diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 49cc848b3..c52fd85ec 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -29,17 +29,16 @@ namespace is_trunc definition is_trunc.pi_char (n : trunc_index) (A : Type) : (Π (x y : A), is_trunc n (x = y)) ≃ (is_trunc (n .+1) A) := begin - fapply equiv.mk, + fapply equiv.MK, {intro H, apply is_trunc_succ_intro}, - {fapply is_equiv.adjointify, - {intros (H, x, y), apply is_trunc_eq}, - {intro H, apply (is_trunc.rec_on H), intro Hint, apply idp}, - {intro P, - unfold compose, apply eq_of_homotopy, - exact sorry}}, + {intros (H, x, y), apply is_trunc_eq}, + {intro H, apply (is_trunc.rec_on H), intro Hint, apply idp}, + {intro P, apply eq_of_homotopy, intro a, apply eq_of_homotopy, intro b, + esimp {function.id,compose,is_trunc_succ_intro,is_trunc_eq}, + generalize (P a b), intro H, apply (is_trunc.rec_on H), intro H', apply idp}, end - definition is_hprop_is_trunc {n : trunc_index} : + definition is_hprop_is_trunc [instance] (n : trunc_index) : Π (A : Type), is_hprop (is_trunc n A) := begin apply (trunc_index.rec_on n), @@ -84,7 +83,7 @@ namespace is_trunc have H2 : transport (λx, R a x → a = x) p (@imp a a) = @imp a a, from !apD, have H3 : Π(r : R a a), transport (λx, a = x) p (imp r) = imp (transport (λx, R a x) p r), from - to_fun (symm !heq_pi) H2, + to_fun (equiv.symm !heq_pi) H2, have H4 : imp (refl a) ⬝ p = imp (refl a), from calc imp (refl a) ⬝ p = transport (λx, a = x) p (imp (refl a)) : transport_paths_r @@ -117,4 +116,25 @@ namespace is_trunc (K : Π(a : A), is_trunc n (a = a)) : is_trunc (n.+1) A := @is_trunc_succ_intro _ _ (λa b, is_trunc_of_imp_is_trunc_of_leq H (λp, eq.rec_on p !K)) + open trunctype equiv equiv.ops + + protected definition trunctype.sigma_char.{l} (n : trunc_index) : + (trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) := + begin + fapply equiv.MK, + /--/ intro A, exact (⟨trunctype_type A, is_trunc_trunctype_type A⟩), + /--/ intro S, exact (trunctype.mk S.1 S.2), + /--/ intro S, apply (sigma.rec_on S), intros (S1, S2), apply idp, + intro A, apply (trunctype.rec_on A), intros (A1, A2), apply idp, + end + +-- set_option pp.notation false + protected definition trunctype.eq (n : trunc_index) (A B : n-Type) : + (A = B) ≃ (trunctype_type A = trunctype_type B) := + calc + (A = B) ≃ (trunctype.sigma_char n A = trunctype.sigma_char n B) : eq_equiv_fn_eq_of_equiv + ... ≃ ((trunctype.sigma_char n A).1 = (trunctype.sigma_char n B).1) : equiv.symm (!equiv_subtype) + ... ≃ (trunctype_type A = trunctype_type B) : equiv.refl + + end is_trunc