From 5fe8ee606f715415dcc38ab6c4d36e366527e435 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Sun, 30 Nov 2014 19:56:32 -0500 Subject: [PATCH] feat(library/hott): port Floris' category implementation --- library/hott/algebra/category/basic.lean | 79 ++ .../hott/algebra/category/constructions.lean | 355 ++++++ library/hott/algebra/category/functor.lean | 149 +++ library/hott/algebra/category/morphism.lean | 267 +++++ .../category/natural_transformation.lean | 54 + library/hott/path.lean | 1037 +++++++++-------- 6 files changed, 1425 insertions(+), 516 deletions(-) create mode 100644 library/hott/algebra/category/basic.lean create mode 100644 library/hott/algebra/category/constructions.lean create mode 100644 library/hott/algebra/category/functor.lean create mode 100644 library/hott/algebra/category/morphism.lean create mode 100644 library/hott/algebra/category/natural_transformation.lean diff --git a/library/hott/algebra/category/basic.lean b/library/hott/algebra/category/basic.lean new file mode 100644 index 000000000..7489b1ae3 --- /dev/null +++ b/library/hott/algebra/category/basic.lean @@ -0,0 +1,79 @@ +-- 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 + +import hott.axioms.funext hott.trunc hott.equiv + +open path truncation + +inductive precategory [class] (ob : Type) : Type := +mk : Π (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), + (Π ⦃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) → + (Π ⦃a b : ob⦄ {f : hom a b}, comp id f ≈ f) → + (Π ⦃a b : ob⦄ {f : hom a b}, comp f id ≈ f) → + precategory ob + +namespace precategory + variables {ob : Type} [C : precategory ob] + variables {a b c d : ob} + include C + + definition hom [reducible] : ob → ob → Type := rec (λ hom homH compose id assoc idr idl, hom) C + + definition homH [instance] : Π {a b : ob}, is_hset (hom a b) := rec (λ hom homH compose id assoc idr idl, homH) C + + -- note: needs to be reducible to typecheck composition in opposite category + definition compose [reducible] : Π {a b c : ob}, hom b c → hom a b → hom a c := + rec (λ hom homH compose id assoc idr idl, compose) C + + definition id [reducible] : Π {a : ob}, hom a a := rec (λ hom homH compose id assoc idr idl, id) C + definition ID [reducible] (a : ob) : hom a a := id + + infixr `∘` := compose + infixl `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→)) + + variables {h : hom c d} {g : hom b c} {f : hom a b} {i : hom a a} + + theorem assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b), + h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f := + rec (λ hom homH comp id assoc idr idl, assoc) C + + theorem id_left : Π ⦃a b : ob⦄ (f : hom a b), id ∘ f ≈ f := + rec (λ hom homH comp id assoc idl idr, idl) C + theorem id_right : Π ⦃a b : ob⦄ (f : hom a b), f ∘ id ≈ f := + rec (λ hom homH comp id assoc idl idr, idr) C + + --the following is the only theorem for which "include C" is necessary if C is a variable (why?) + theorem id_compose (a : ob) : (ID a) ∘ id ≈ id := !id_left + + theorem 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 := + calc i ≈ id ∘ i : id_left + ... ≈ id : H +end precategory + +inductive Precategory : Type := mk : Π (ob : Type), precategory ob → Precategory + +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) + + definition objects [coercion] [reducible] (C : Precategory) : Type + := Precategory.rec (fun c s, c) C + + definition category_instance [instance] [coercion] [reducible] (C : Precategory) : precategory (objects C) + := Precategory.rec (fun c s, s) C + +end precategory + +open precategory + +theorem Category.equal (C : Precategory) : Precategory.mk C C = C := + Precategory.rec (λ ob c, rfl) C diff --git a/library/hott/algebra/category/constructions.lean b/library/hott/algebra/category/constructions.lean new file mode 100644 index 000000000..5697d90b1 --- /dev/null +++ b/library/hott/algebra/category/constructions.lean @@ -0,0 +1,355 @@ +-- 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 + +-- This file contains basic constructions on precategories, including common categories + + +import .natural_transformation +import data.unit data.sigma data.prod data.empty data.bool + +open eq eq.ops prod +namespace category + namespace opposite + section + definition opposite {ob : Type} (C : category ob) : category ob := + mk (λa b, hom b a) + (λ a b c f g, g ∘ f) + (λ a, id) + (λ a b c d f g h, symm !assoc) + (λ a b f, !id_right) + (λ a b f, !id_left) + + definition Opposite (C : Category) : Category := Mk (opposite C) + --direct construction: + -- MK C + -- (λa b, hom b a) + -- (λ a b c f g, g ∘ f) + -- (λ a, id) + -- (λ a b c d f g h, symm !assoc) + -- (λ a b f, !id_right) + -- (λ a b f, !id_left) + + infixr `∘op`:60 := @compose _ (opposite _) _ _ _ + + variables {C : Category} {a b c : C} + + theorem compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := rfl + + theorem op_op' {ob : Type} (C : category ob) : opposite (opposite C) = C := + category.rec (λ hom comp id assoc idl idr, refl (mk _ _ _ _ _ _)) C + + theorem op_op : Opposite (Opposite C) = C := + (@congr_arg _ _ _ _ (Category.mk C) (op_op' C)) ⬝ !Category.equal + + end + end opposite + + definition type_category : category Type := + mk (λa b, a → b) + (λ a b c, function.compose) + (λ a, function.id) + (λ a b c d h g f, symm (function.compose_assoc h g f)) + (λ a b f, function.compose_id_left f) + (λ a b f, function.compose_id_right f) + + definition Type_category : Category := Mk type_category + + section + open decidable unit empty + variables {A : Type} [H : decidable_eq A] + include H + definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty) + theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _ + definition set_compose {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c := + decidable.rec_on + (H b c) + (λ Hbc g, decidable.rec_on + (H a b) + (λ Hab f, rec_on_true (trans Hab Hbc) ⋆) + (λh f, empty.rec _ f) f) + (λh (g : empty), empty.rec _ g) g + omit H + definition discrete_category (A : Type) [H : decidable_eq A] : category A := + mk (λa b, set_hom a b) + (λ a b c g f, set_compose g f) + (λ a, decidable.rec_on_true rfl ⋆) + (λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _) + (λ a b f, @subsingleton.elim (set_hom a b) _ _ _) + (λ a b f, @subsingleton.elim (set_hom a b) _ _ _) + definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A) + end + section + open unit bool + definition category_one := discrete_category unit + definition Category_one := Mk category_one + definition category_two := discrete_category bool + definition Category_two := Mk category_two + end + + namespace product + section + open prod + definition prod_category {obC obD : Type} (C : category obC) (D : category obD) + : category (obC × obD) := + mk (λa b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b)) + (λ 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.equal !id_left !id_left ) + (λ a b f, prod.equal !id_right !id_right) + + definition Prod_category (C D : Category) : Category := Mk (prod_category C D) + + end + end product + + namespace ops + notation `type`:max := Type_category + notation 1 := Category_one --it was confusing for me (Floris) that no ``s are needed here + notation 2 := Category_two + postfix `ᵒᵖ`:max := opposite.Opposite + infixr `×c`:30 := product.Prod_category + instance [persistent] type_category category_one + category_two product.prod_category + end ops + + open ops + namespace opposite + section + open ops functor + definition opposite_functor {C D : Category} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ := + @functor.mk (Cᵒᵖ) (Dᵒᵖ) + (λ a, F a) + (λ a b f, F f) + (λ a, !respect_id) + (λ a b c g f, !respect_comp) + end + end opposite + + namespace product + section + open ops functor + definition prod_functor {C C' D D' : Category} (F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' := + functor.mk (λ a, pair (F (pr1 a)) (G (pr2 a))) + (λ a b f, pair (F (pr1 f)) (G (pr2 f))) + (λ a, pair_eq !respect_id !respect_id) + (λ a b c g f, pair_eq !respect_comp !respect_comp) + end + end product + + namespace ops + infixr `×f`:30 := product.prod_functor + infixr `ᵒᵖᶠ`:max := opposite.opposite_functor + end ops + + section functor_category + variables (C D : Category) + definition functor_category : category (functor C D) := + mk (λa b, natural_transformation a b) + (λ a b c g f, natural_transformation.compose g f) + (λ a, natural_transformation.id) + (λ a b c d h g f, !natural_transformation.assoc) + (λ a b f, !natural_transformation.id_left) + (λ a b f, !natural_transformation.id_right) + end functor_category + + namespace slice + open sigma function + variables {ob : Type} {C : category ob} {c : ob} + protected definition slice_obs (C : category ob) (c : ob) := Σ(b : ob), hom b c + variables {a b : slice_obs C c} + protected definition to_ob (a : slice_obs C c) : ob := dpr1 a + protected definition to_ob_def (a : slice_obs C c) : to_ob a = dpr1 a := rfl + protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := dpr2 a + -- protected theorem slice_obs_equal (H₁ : to_ob a = to_ob b) + -- (H₂ : eq.drec_on H₁ (ob_hom a) = ob_hom b) : a = b := + -- sigma.equal H₁ H₂ + + + protected definition slice_hom (a b : slice_obs C c) : Type := + Σ(g : hom (to_ob a) (to_ob b)), ob_hom b ∘ g = ob_hom a + + protected definition hom_hom (f : slice_hom a b) : hom (to_ob a) (to_ob b) := dpr1 f + protected definition commute (f : slice_hom a b) : ob_hom b ∘ (hom_hom f) = ob_hom a := dpr2 f + -- protected theorem slice_hom_equal (f g : slice_hom a b) (H : hom_hom f = hom_hom g) : f = g := + -- sigma.equal H !proof_irrel + + definition slice_category (C : category ob) (c : ob) : category (slice_obs C c) := + mk (λa b, slice_hom a b) + (λ a b c g f, dpair (hom_hom g ∘ hom_hom f) + (show ob_hom c ∘ (hom_hom g ∘ hom_hom f) = ob_hom a, + proof + calc + ob_hom c ∘ (hom_hom g ∘ hom_hom f) = (ob_hom c ∘ hom_hom g) ∘ hom_hom f : !assoc + ... = ob_hom b ∘ hom_hom f : {commute g} + ... = ob_hom a : {commute f} + qed)) + (λ a, dpair id !id_right) + (λ a b c d h g f, dpair_eq !assoc !proof_irrel) + (λ a b f, sigma.equal !id_left !proof_irrel) + (λ a b f, sigma.equal !id_right !proof_irrel) + -- We use !proof_irrel instead of rfl, to give the unifier an easier time + + -- definition slice_category {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom b c) + -- := + -- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), dpr2 b ∘ g = dpr2 a) + -- (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) + -- (show dpr2 c ∘ (dpr1 g ∘ dpr1 f) = dpr2 a, + -- proof + -- calc + -- dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : !assoc + -- ... = dpr2 b ∘ dpr1 f : {dpr2 g} + -- ... = dpr2 a : {dpr2 f} + -- qed)) + -- (λ a, dpair id !id_right) + -- (λ a b c d h g f, dpair_eq !assoc !proof_irrel) + -- (λ a b f, sigma.equal !id_left !proof_irrel) + -- (λ a b f, sigma.equal !id_right !proof_irrel) + -- We use !proof_irrel instead of rfl, to give the unifier an easier time + + definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c) + open category.ops + instance [persistent] slice_category + variables {D : Category} + definition forgetful (x : D) : (Slice_category D x) ⇒ D := + functor.mk (λ a, to_ob a) + (λ a b f, hom_hom f) + (λ a, rfl) + (λ a b c g f, rfl) + + definition postcomposition_functor {x y : D} (h : x ⟶ y) + : Slice_category D x ⇒ Slice_category D y := + functor.mk (λ a, dpair (to_ob a) (h ∘ ob_hom a)) + (λ a b f, dpair (hom_hom f) + (calc + (h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : assoc h (ob_hom b) (hom_hom f)⁻¹ + ... = h ∘ ob_hom a : congr_arg (λx, h ∘ x) (commute f))) + (λ a, rfl) + (λ a b c g f, dpair_eq rfl !proof_irrel) + + -- -- in the following comment I tried to have (A = B) in the type of a == b, but that doesn't solve the problems + -- definition heq2 {A B : Type} (H : A = B) (a : A) (b : B) := a == b + -- definition heq2.intro {A B : Type} {a : A} {b : B} (H : a == b) : heq2 (heq.type_eq H) a b := H + -- definition heq2.elim {A B : Type} {a : A} {b : B} (H : A = B) (H2 : heq2 H a b) : a == b := H2 + -- definition heq2.proof_irrel {A B : Prop} (a : A) (b : B) (H : A = B) : heq2 H a b := + -- hproof_irrel H a b + -- theorem functor.mk_eq2 {C D : Category} {obF obG : C → D} {homF homG idF idG compF compG} + -- (Hob : ∀x, obF x = obG x) + -- (Hmor : ∀(a b : C) (f : a ⟶ b), heq2 (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (homF a b f) (homG a b f)) + -- : functor.mk obF homF idF compF = functor.mk obG homG idG compG := + -- hddcongr_arg4 functor.mk + -- (funext Hob) + -- (hfunext (λ a, hfunext (λ b, hfunext (λ f, !Hmor)))) + -- !proof_irrel + -- !proof_irrel + +-- set_option pp.implicit true +-- set_option pp.coercions true + + -- definition slice_functor : D ⇒ Category_of_categories := + -- functor.mk (λ a, Category.mk (slice_obs D a) (slice_category D a)) + -- (λ a b f, postcomposition_functor f) + -- (λ a, functor.mk_heq + -- (λx, sigma.equal rfl !id_left) + -- (λb c f, sigma.hequal sorry !heq.refl (hproof_irrel sorry _ _))) + -- (λ a b c g f, functor.mk_heq + -- (λx, sigma.equal (sorry ⬝ refl (dpr1 x)) sorry) + -- (λb c f, sorry)) + + --the error message generated here is really confusing: the type of the above refl should be + -- "@dpr1 D (λ (a_1 : D), a_1 ⟶ a) x = @dpr1 D (λ (a_1 : D), a_1 ⟶ c) x", but the second dpr1 is not even well-typed + + end slice + + -- section coslice + -- open sigma + + -- definition coslice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom c b) := + -- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), g ∘ dpr2 a = dpr2 b) + -- (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) + -- (show (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr2 c, + -- proof + -- calc + -- (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr1 g ∘ (dpr1 f ∘ dpr2 a): symm !assoc + -- ... = dpr1 g ∘ dpr2 b : {dpr2 f} + -- ... = dpr2 c : {dpr2 g} + -- qed)) + -- (λ a, dpair id !id_left) + -- (λ a b c d h g f, dpair_eq !assoc !proof_irrel) + -- (λ a b f, sigma.equal !id_left !proof_irrel) + -- (λ a b f, sigma.equal !id_right !proof_irrel) + + -- -- theorem slice_coslice_opp {ob : Type} (C : category ob) (c : ob) : + -- -- coslice C c = opposite (slice (opposite C) c) := + -- -- sorry + -- end coslice + + section arrow + open sigma eq.ops + -- theorem concat_commutative_squares {ob : Type} {C : category ob} {a1 a2 a3 b1 b2 b3 : ob} + -- {f1 : a1 => b1} {f2 : a2 => b2} {f3 : a3 => b3} {g2 : a2 => a3} {g1 : a1 => a2} + -- {h2 : b2 => b3} {h1 : b1 => b2} (H1 : f2 ∘ g1 = h1 ∘ f1) (H2 : f3 ∘ g2 = h2 ∘ f2) + -- : f3 ∘ (g2 ∘ g1) = (h2 ∘ h1) ∘ f1 := + -- calc + -- f3 ∘ (g2 ∘ g1) = (f3 ∘ g2) ∘ g1 : assoc + -- ... = (h2 ∘ f2) ∘ g1 : {H2} + -- ... = h2 ∘ (f2 ∘ g1) : symm assoc + -- ... = h2 ∘ (h1 ∘ f1) : {H1} + -- ... = (h2 ∘ h1) ∘ f1 : assoc + + -- definition arrow {ob : Type} (C : category ob) : category (Σ(a b : ob), hom a b) := + -- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)) (h : hom (dpr2' a) (dpr2' b)), + -- dpr3 b ∘ g = h ∘ dpr3 a) + -- (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) (dpair (dpr2' g ∘ dpr2' f) (concat_commutative_squares (dpr3 f) (dpr3 g)))) + -- (λ a, dpair id (dpair id (id_right ⬝ (symm id_left)))) + -- (λ a b c d h g f, dtrip_eq2 assoc assoc !proof_irrel) + -- (λ a b f, trip.equal2 id_left id_left !proof_irrel) + -- (λ a b f, trip.equal2 id_right id_right !proof_irrel) + + -- make these definitions private? + variables {ob : Type} {C : category ob} + protected definition arrow_obs (ob : Type) (C : category ob) := Σ(a b : ob), hom a b + variables {a b : arrow_obs ob C} + protected definition src (a : arrow_obs ob C) : ob := dpr1 a + protected definition dst (a : arrow_obs ob C) : ob := dpr2' a + protected definition to_hom (a : arrow_obs ob C) : hom (src a) (dst a) := dpr3 a + + protected definition arrow_hom (a b : arrow_obs ob C) : Type := + Σ (g : hom (src a) (src b)) (h : hom (dst a) (dst b)), to_hom b ∘ g = h ∘ to_hom a + + protected definition hom_src (m : arrow_hom a b) : hom (src a) (src b) := dpr1 m + protected definition hom_dst (m : arrow_hom a b) : hom (dst a) (dst b) := dpr2' m + protected definition commute (m : arrow_hom a b) : to_hom b ∘ (hom_src m) = (hom_dst m) ∘ to_hom a + := dpr3 m + + definition arrow (ob : Type) (C : category ob) : category (arrow_obs ob C) := + mk (λa b, arrow_hom a b) + (λ a b c g f, dpair (hom_src g ∘ hom_src f) (dpair (hom_dst g ∘ hom_dst f) + (show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a, + proof + calc + to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : !assoc + ... = (hom_dst g ∘ to_hom b) ∘ hom_src f : {commute g} + ... = hom_dst g ∘ (to_hom b ∘ hom_src f) : symm !assoc + ... = hom_dst g ∘ (hom_dst f ∘ to_hom a) : {commute f} + ... = (hom_dst g ∘ hom_dst f) ∘ to_hom a : !assoc + qed) + )) + (λ a, dpair id (dpair id (!id_right ⬝ (symm !id_left)))) + (λ a b c d h g f, ndtrip_eq !assoc !assoc !proof_irrel) + (λ a b f, ndtrip_equal !id_left !id_left !proof_irrel) + (λ a b f, ndtrip_equal !id_right !id_right !proof_irrel) + + end arrow + +end category + + -- definition foo + -- : category (sorry) := + -- mk (λa b, sorry) + -- (λ a b c g f, sorry) + -- (λ a, sorry) + -- (λ a b c d h g f, sorry) + -- (λ a b f, sorry) + -- (λ a b f, sorry) diff --git a/library/hott/algebra/category/functor.lean b/library/hott/algebra/category/functor.lean new file mode 100644 index 000000000..6da585f85 --- /dev/null +++ b/library/hott/algebra/category/functor.lean @@ -0,0 +1,149 @@ +-- 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 + +import .basic +import hott.path +open function +open precategory path heq + +inductive functor (C D : Precategory) : Type := +mk : Π (obF : C → D) (homF : Π(a b : C), hom a b → hom (obF a) (obF b)), + (Π (a : C), homF a a (ID a) ≈ ID (obF a)) → + (Π (a b c : C) {g : hom b c} {f : hom a b}, homF a c (g ∘ f) ≈ homF b c g ∘ homF a b f) → + functor C D + +infixl `⇒`:25 := functor + +-- I think we only have a precategory of stict catetories. +-- Maybe better implement this using univalence. +namespace functor + variables {C D E : Precategory} + definition object [coercion] (F : functor C D) : C → D := rec (λ obF homF Hid Hcomp, obF) F + + definition morphism [coercion] (F : functor C D) : Π⦃a b : C⦄, hom a b → hom (F a) (F b) := + rec (λ obF homF Hid Hcomp, homF) F + + theorem respect_id (F : functor C D) : Π (a : C), F (ID a) ≈ id := + rec (λ obF homF Hid Hcomp, Hid) F + + theorem respect_comp (F : functor C D) : Π ⦃a b c : C⦄ (g : hom b c) (f : hom a b), + F (g ∘ f) ≈ F g ∘ F f := + rec (λ obF homF Hid Hcomp, Hcomp) F + + protected definition compose (G : functor D E) (F : functor C D) : functor C E := + functor.mk + (λx, G (F x)) + (λ a b f, G (F f)) + (λ a, calc + G (F (ID a)) ≈ G id : {respect_id F a} --not giving the braces explicitly makes the elaborator compute a couple more seconds + ... ≈ id : respect_id G (F a)) + (λ a b c g f, calc + G (F (g ∘ f)) ≈ G (F g ∘ F f) : respect_comp F g f + ... ≈ G (F g) ∘ G (F f) : respect_comp G (F g) (F f)) + + infixr `∘f`:60 := compose + + /- + protected theorem assoc {A B C D : Precategory} (H : functor C D) (G : functor B C) (F : functor A B) : + H ∘f (G ∘f F) ≈ (H ∘f G) ∘f F := + sorry + -/ + + /-protected definition id {C : Precategory} : functor C C := + mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp) + protected definition ID (C : Precategory) : functor C C := id + + protected theorem id_left (F : functor C D) : id ∘f F ≈ F := + functor.rec (λ obF homF idF compF, dcongr_arg4 mk idp idp !proof_irrel !proof_irrel) F + protected theorem id_right (F : functor C D) : F ∘f id ≈ F := + functor.rec (λ obF homF idF compF, dcongr_arg4 mk idp idp !proof_irrel !proof_irrel) F-/ + +end functor + +/- +namespace category + open functor + definition category_of_categories [reducible] : category Category := + mk (λ a b, functor a b) + (λ a b c g f, functor.compose g f) + (λ a, functor.id) + (λ a b c d h g f, !functor.assoc) + (λ a b f, !functor.id_left) + (λ a b f, !functor.id_right) + definition Category_of_categories [reducible] := Mk category_of_categories + + namespace ops + notation `Cat`:max := Category_of_categories + instance [persistent] category_of_categories + end ops +end category-/ + +namespace functor +-- open category.ops +-- universes l m + variables {C D : Precategory} +-- check hom C D +-- variables (F : C ⟶ D) (G : D ⇒ C) +-- check G ∘ F +-- check F ∘f G +-- variables (a b : C) (f : a ⟶ b) +-- check F a +-- check F b +-- check F f +-- check G (F f) +-- print "---" +-- -- check (G ∘ F) f --error +-- check (λ(x : functor C C), x) (G ∘ F) f +-- check (G ∘f F) f +-- print "---" +-- -- check (G ∘ F) a --error +-- check (G ∘f F) a +-- print "---" +-- -- check λ(H : hom C D) (x : C), H x --error +-- check λ(H : @hom _ Cat C D) (x : C), H x +-- check λ(H : C ⇒ D) (x : C), H x +-- print "---" +-- -- variables {obF obG : C → D} (Hob : ∀x, obF x = obG x) (homF : Π(a b : C) (f : a ⟶ b), obF a ⟶ obF b) (homG : Π(a b : C) (f : a ⟶ b), obG a ⟶ obG b) +-- -- check eq.rec_on (funext Hob) homF = homG + + /-theorem mk_heq {obF obG : C → D} {homF homG idF idG compF compG} (Hob : ∀x, obF x = obG x) + (Hmor : ∀(a b : C) (f : a ⟶ b), homF a b f == homG a b f) + : mk obF homF idF compF = mk obG homG idG compG := + hddcongr_arg4 mk + (funext Hob) + (hfunext (λ a, hfunext (λ b, hfunext (λ f, !Hmor)))) + !proof_irrel + !proof_irrel + + protected theorem hequal {F G : C ⇒ D} : Π (Hob : ∀x, F x = G x) + (Hmor : ∀a b (f : a ⟶ b), F f == G f), F = G := + functor.rec + (λ obF homF idF compF, + functor.rec + (λ obG homG idG compG Hob Hmor, mk_heq Hob Hmor) + G) + F-/ + +-- theorem mk_eq {obF obG : C → D} {homF homG idF idG compF compG} (Hob : ∀x, obF x = obG x) +-- (Hmor : ∀(a b : C) (f : a ⟶ b), cast (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (homF a b f) +-- = homG a b f) +-- : mk obF homF idF compF = mk obG homG idG compG := +-- dcongr_arg4 mk +-- (funext Hob) +-- (funext (λ a, funext (λ b, funext (λ f, sorry ⬝ Hmor a b f)))) +-- -- to fill this sorry use (a generalization of) cast_pull +-- !proof_irrel +-- !proof_irrel + +-- protected theorem equal {F G : C ⇒ D} : Π (Hob : ∀x, F x = G x) +-- (Hmor : ∀a b (f : a ⟶ b), cast (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (F f) = G f), F = G := +-- functor.rec +-- (λ obF homF idF compF, +-- functor.rec +-- (λ obG homG idG compG Hob Hmor, mk_eq Hob Hmor) +-- G) +-- F + + +end functor diff --git a/library/hott/algebra/category/morphism.lean b/library/hott/algebra/category/morphism.lean new file mode 100644 index 000000000..909ae07cf --- /dev/null +++ b/library/hott/algebra/category/morphism.lean @@ -0,0 +1,267 @@ +-- 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 + +import .basic + +open path precategory + +namespace morphism + variables {ob : Type} [C : precategory ob] include C + variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a} + inductive is_section [class] (f : a ⟶ b) : Type + := mk : ∀{g}, g ∘ f ≈ id → is_section f + inductive is_retraction [class] (f : a ⟶ b) : Type + := mk : ∀{g}, f ∘ g ≈ id → is_retraction f + inductive is_iso [class] (f : a ⟶ b) : Type + := mk : ∀{g}, g ∘ f ≈ id → f ∘ g ≈ id → is_iso f + + definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a := + is_section.rec (λg h, g) H + definition section_of (f : a ⟶ b) [H : is_retraction f] : hom b a := + is_retraction.rec (λg h, g) H + definition inverse (f : a ⟶ b) [H : is_iso f] : hom b a := + is_iso.rec (λg h1 h2, g) H + + postfix `⁻¹` := inverse + + theorem inverse_compose (f : a ⟶ b) [H : is_iso f] : f⁻¹ ∘ f ≈ id := + is_iso.rec (λg h1 h2, h1) H + + theorem compose_inverse (f : a ⟶ b) [H : is_iso f] : f ∘ f⁻¹ ≈ id := + is_iso.rec (λg h1 h2, h2) H + + theorem retraction_compose (f : a ⟶ b) [H : is_section f] : retraction_of f ∘ f ≈ id := + is_section.rec (λg h, h) H + + theorem compose_section (f : a ⟶ b) [H : is_retraction f] : f ∘ section_of f ≈ id := + is_retraction.rec (λg h, h) H + + theorem iso_imp_retraction [instance] (f : a ⟶ b) [H : is_iso f] : is_section f := + is_section.mk !inverse_compose + + theorem iso_imp_section [instance] (f : a ⟶ b) [H : is_iso f] : is_retraction f := + is_retraction.mk !compose_inverse + + theorem id_is_iso [instance] : is_iso (ID a) := + is_iso.mk !id_compose !id_compose + + theorem inverse_is_iso [instance] (f : a ⟶ b) [H : is_iso f] : is_iso (f⁻¹) := + is_iso.mk !compose_inverse !inverse_compose + + theorem left_inverse_eq_right_inverse {f : a ⟶ b} {g g' : hom b a} + (Hl : g ∘ f ≈ id) (Hr : f ∘ g' ≈ id) : g ≈ g' := + calc + g ≈ g ∘ id : !id_right + ... ≈ g ∘ f ∘ g' : Hr + ... ≈ (g ∘ f) ∘ g' : assoc + ... ≈ id ∘ g' : Hl + ... ≈ g' : id_left + + theorem retraction_eq_intro [H : is_section f] (H2 : f ∘ h ≈ id) : retraction_of f ≈ h + := left_inverse_eq_right_inverse !retraction_compose H2 + + theorem section_eq_intro [H : is_retraction f] (H2 : h ∘ f ≈ id) : section_of f ≈ h + := (left_inverse_eq_right_inverse H2 !compose_section)⁻¹ + + theorem inverse_eq_intro_right [H : is_iso f] (H2 : f ∘ h ≈ id) : f⁻¹ ≈ h + := left_inverse_eq_right_inverse !inverse_compose H2 + + theorem inverse_eq_intro_left [H : is_iso f] (H2 : h ∘ f ≈ id) : f⁻¹ ≈ h + := (left_inverse_eq_right_inverse H2 !compose_inverse)⁻¹ + + theorem section_eq_retraction (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f] : + retraction_of f ≈ section_of f := + retraction_eq_intro !compose_section + + theorem section_retraction_imp_iso (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f] + : is_iso f := + is_iso.mk ((section_eq_retraction f) ▹ (retraction_compose f)) (compose_section f) + + 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 := + inverse_eq_intro_right !inverse_compose + + theorem retraction_of_id : retraction_of (ID a) ≈ id := + retraction_eq_intro !id_compose + + theorem section_of_id : section_of (ID a) ≈ id := + section_eq_intro !id_compose + + theorem iso_of_id : ID a⁻¹ ≈ id := + inverse_eq_intro_left !id_compose + + theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g] + : is_section (g ∘ f) := + is_section.mk + (calc + (retraction_of f ∘ retraction_of g) ∘ g ∘ f + ≈ retraction_of f ∘ retraction_of g ∘ g ∘ f : assoc _ _ (g ∘ f) + ... ≈ retraction_of f ∘ (retraction_of g ∘ g) ∘ f : assoc _ g f + ... ≈ retraction_of f ∘ id ∘ f : retraction_compose g + ... ≈ retraction_of f ∘ f : id_left f + ... ≈ id : retraction_compose) + + theorem composition_is_retraction [instance] (Hf : is_retraction f) (Hg : is_retraction g) + : is_retraction (g ∘ f) := + is_retraction.mk + (calc + (g ∘ f) ∘ section_of f ∘ section_of g ≈ g ∘ f ∘ section_of f ∘ section_of g : assoc + ... ≈ g ∘ (f ∘ section_of f) ∘ section_of g : assoc f _ _ + ... ≈ g ∘ id ∘ section_of g : compose_section f + ... ≈ g ∘ section_of g : id_left (section_of g) + ... ≈ id : compose_section) + + theorem composition_is_inverse [instance] (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) := + !section_retraction_imp_iso + + inductive isomorphic (a b : ob) : Type := mk : ∀(g : a ⟶ b) [H : is_iso g], isomorphic a b +/- + namespace isomorphic + open relation + -- should these be coercions? + definition iso [coercion] (H : isomorphic a b) : a ⟶ b := + isomorphic.rec (λg h, g) H + theorem is_iso [instance] (H : isomorphic a b) : is_iso (isomorphic.iso H) := + isomorphic.rec (λg h, h) H + infix `≅`:50 := isomorphic + + theorem refl (a : ob) : a ≅ a := mk id + theorem symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := mk (inverse (iso H)) + theorem trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := mk (iso H2 ∘ iso H1) + theorem is_equivalence_eq [instance] (T : Type) : is_equivalence isomorphic := + is_equivalence.mk (is_reflexive.mk refl) (is_symmetric.mk symm) (is_transitive.mk trans) + end isomorphic +-/ + inductive is_mono [class] (f : a ⟶ b) : Type := + mk : (∀c (g h : hom c a), f ∘ g ≈ f ∘ h → g ≈ h) → is_mono f + inductive is_epi [class] (f : a ⟶ b) : Type := + mk : (∀c (g h : hom b c), g ∘ f ≈ h ∘ f → g ≈ h) → is_epi f + + theorem mono_elim [H : is_mono f] {g h : c ⟶ a} (H2 : f ∘ g ≈ f ∘ h) : g ≈ h + := is_mono.rec (λH3, H3 c g h H2) H + theorem epi_elim [H : is_epi f] {g h : b ⟶ c} (H2 : g ∘ f ≈ h ∘ f) : g ≈ h + := is_epi.rec (λH3, H3 c g h H2) H + + theorem section_is_mono [instance] (f : a ⟶ b) [H : is_section f] : is_mono f := + is_mono.mk + (λ c g h H, + calc + g ≈ id ∘ g : id_left + ... ≈ (retraction_of f ∘ f) ∘ g : retraction_compose f + ... ≈ retraction_of f ∘ f ∘ g : assoc + ... ≈ retraction_of f ∘ f ∘ h : H + ... ≈ (retraction_of f ∘ f) ∘ h : assoc + ... ≈ id ∘ h : retraction_compose f + ... ≈ h : id_left) + + theorem retraction_is_epi [instance] (f : a ⟶ b) [H : is_retraction f] : is_epi f := + is_epi.mk + (λ c g h H, + calc + g ≈ g ∘ id : id_right + ... ≈ g ∘ f ∘ section_of f : compose_section f + ... ≈ (g ∘ f) ∘ section_of f : assoc + ... ≈ (h ∘ f) ∘ section_of f : H + ... ≈ h ∘ f ∘ section_of f : assoc + ... ≈ h ∘ id : compose_section f + ... ≈ h : id_right) + + --these theorems are now proven automatically using type classes + --should they be instances? + theorem id_is_mono : is_mono (ID a) + theorem id_is_epi : is_epi (ID a) + + theorem composition_is_mono [instance] [Hf : is_mono f] [Hg : is_mono g] : is_mono (g ∘ f) := + is_mono.mk + (λ d h₁ h₂ H, + have H2 : g ∘ (f ∘ h₁) ≈ g ∘ (f ∘ h₂), from (assoc g f h₁)⁻¹ ▹ (assoc g f h₂)⁻¹ ▹ H, + mono_elim (mono_elim H2)) + + theorem composition_is_epi [instance] [Hf : is_epi f] [Hg : is_epi g] : is_epi (g ∘ f) := + is_epi.mk + (λ d h₁ h₂ H, + have H2 : (h₁ ∘ g) ∘ f ≈ (h₂ ∘ g) ∘ f, from assoc h₁ g f ▹ assoc h₂ g f ▹ H, + epi_elim (epi_elim H2)) + +end morphism +namespace morphism +--rewrite lemmas for inverses, modified from +--https://github.com/JasonGross/HoTT-categories/blob/master/theories/Categories/Category/Morphisms.v + namespace iso + section + variables {ob : Type} [C : precategory ob] include C + variables {a b c d : ob} (f : b ⟶ a) + (r : c ⟶ d) (q : b ⟶ c) (p : a ⟶ b) + (g : d ⟶ c) + variable [Hq : is_iso q] include Hq + theorem compose_pV : q ∘ q⁻¹ ≈ id := !compose_inverse + theorem compose_Vp : q⁻¹ ∘ q ≈ id := !inverse_compose + theorem compose_V_pp : q⁻¹ ∘ (q ∘ p) ≈ p := + calc + q⁻¹ ∘ (q ∘ p) ≈ (q⁻¹ ∘ q) ∘ p : assoc (q⁻¹) q p + ... ≈ id ∘ p : inverse_compose q + ... ≈ p : id_left p + theorem compose_p_Vp : q ∘ (q⁻¹ ∘ g) ≈ g := + calc + q ∘ (q⁻¹ ∘ g) ≈ (q ∘ q⁻¹) ∘ g : assoc q (q⁻¹) g + ... ≈ id ∘ g : compose_inverse q + ... ≈ g : id_left g + theorem compose_pp_V : (r ∘ q) ∘ q⁻¹ ≈ r := + calc + (r ∘ q) ∘ q⁻¹ ≈ r ∘ q ∘ q⁻¹ : assoc r q (q⁻¹)⁻¹ + ... ≈ r ∘ id : compose_inverse q + ... ≈ r : id_right r + theorem compose_pV_p : (f ∘ q⁻¹) ∘ q ≈ f := + calc + (f ∘ q⁻¹) ∘ q ≈ f ∘ q⁻¹ ∘ q : assoc f (q⁻¹) q⁻¹ + ... ≈ f ∘ id : inverse_compose q + ... ≈ f : id_right f + + theorem inv_pp [H' : is_iso p] : (q ∘ p)⁻¹ ≈ p⁻¹ ∘ q⁻¹ := + have H1 : (p⁻¹ ∘ q⁻¹) ∘ q ∘ p ≈ p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)), from assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹, + have H2 : (p⁻¹) ∘ (q⁻¹ ∘ (q ∘ p)) ≈ p⁻¹ ∘ p, from ap _ (compose_V_pp q p), + have H3 : p⁻¹ ∘ p ≈ id, from inverse_compose p, + inverse_eq_intro_left (H1 ⬝ H2 ⬝ H3) + --the proof using calc is hard for the unifier (needs ~90k steps) + -- inverse_eq_intro_left + -- (calc + -- (p⁻¹ ∘ (q⁻¹)) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)) : assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹ + -- ... = (p⁻¹) ∘ p : congr_arg (λx, p⁻¹ ∘ x) (compose_V_pp q p) + -- ... = id : inverse_compose p) + theorem inv_Vp [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ ≈ g⁻¹ ∘ q := inverse_involutive q ▹ inv_pp (q⁻¹) g + theorem inv_pV [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ ≈ f ∘ q⁻¹ := inverse_involutive f ▹ inv_pp q (f⁻¹) + theorem inv_VV [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ ≈ r ∘ q := inverse_involutive r ▹ inv_Vp q (r⁻¹) + end + section + variables {ob : Type} {C : precategory ob} include C + variables {d c b a : ob} + {i : b ⟶ c} {f : b ⟶ a} + {r : c ⟶ d} {q : b ⟶ c} {p : a ⟶ b} + {g : d ⟶ c} {h : c ⟶ b} + {x : b ⟶ d} {z : a ⟶ c} + {y : d ⟶ b} {w : c ⟶ a} + variable [Hq : is_iso q] include Hq + + theorem moveR_Mp (H : y ≈ q⁻¹ ∘ g) : q ∘ y ≈ g := H⁻¹ ▹ compose_p_Vp q g + theorem moveR_pM (H : w ≈ f ∘ q⁻¹) : w ∘ q ≈ f := H⁻¹ ▹ compose_pV_p f q + theorem moveR_Vp (H : z ≈ q ∘ p) : q⁻¹ ∘ z ≈ p := H⁻¹ ▹ compose_V_pp q p + theorem moveR_pV (H : x ≈ r ∘ q) : x ∘ q⁻¹ ≈ r := H⁻¹ ▹ compose_pp_V r q + theorem moveL_Mp (H : q⁻¹ ∘ g ≈ y) : g ≈ q ∘ y := moveR_Mp (H⁻¹)⁻¹ + theorem moveL_pM (H : f ∘ q⁻¹ ≈ w) : f ≈ w ∘ q := moveR_pM (H⁻¹)⁻¹ + theorem moveL_Vp (H : q ∘ p ≈ z) : p ≈ q⁻¹ ∘ z := moveR_Vp (H⁻¹)⁻¹ + theorem moveL_pV (H : r ∘ q ≈ x) : r ≈ x ∘ q⁻¹ := moveR_pV (H⁻¹)⁻¹ + theorem moveL_1V (H : h ∘ q ≈ id) : h ≈ q⁻¹ := inverse_eq_intro_left H⁻¹ + theorem moveL_V1 (H : q ∘ h ≈ id) : h ≈ q⁻¹ := inverse_eq_intro_right H⁻¹ + theorem moveL_1M (H : i ∘ q⁻¹ ≈ id) : i ≈ q := moveL_1V H ⬝ inverse_involutive q + theorem moveL_M1 (H : q⁻¹ ∘ i ≈ id) : i ≈ q := moveL_V1 H ⬝ inverse_involutive q + theorem moveR_1M (H : id ≈ i ∘ q⁻¹) : q ≈ i := moveL_1M (H⁻¹)⁻¹ + theorem moveR_M1 (H : id ≈ q⁻¹ ∘ i) : q ≈ i := moveL_M1 (H⁻¹)⁻¹ + theorem moveR_1V (H : id ≈ h ∘ q) : q⁻¹ ≈ h := moveL_1V (H⁻¹)⁻¹ + theorem moveR_V1 (H : id ≈ q ∘ h) : q⁻¹ ≈ h := moveL_V1 (H⁻¹)⁻¹ + end + end iso + +end morphism diff --git a/library/hott/algebra/category/natural_transformation.lean b/library/hott/algebra/category/natural_transformation.lean new file mode 100644 index 000000000..3b488183b --- /dev/null +++ b/library/hott/algebra/category/natural_transformation.lean @@ -0,0 +1,54 @@ +-- 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 + +import .functor hott.axioms.funext +open precategory path functor + +inductive natural_transformation {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), + natural_transformation F G + +infixl `⟹`:25 := natural_transformation -- \==> + +namespace natural_transformation + variables {C D : Precategory} {F G H I : functor C D} + + definition natural_map [coercion] (η : F ⟹ G) : Π(a : C), F a ⟶ G a := + rec (λ x y, x) η + + theorem naturality (η : F ⟹ G) : Π⦃a b : C⦄ (f : a ⟶ b), G f ∘ η a ≈ η b ∘ F f := + rec (λ x y, y) η + + protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H := + natural_transformation.mk + (λ a, η a ∘ θ a) + (λ a b f, + calc + H f ∘ (η a ∘ θ a) ≈ (H f ∘ η a) ∘ θ a : assoc + ... ≈(η b ∘ G f) ∘ θ a : naturality η f + ... ≈ η b ∘ (G f ∘ θ a) : assoc + ... ≈ η b ∘ (θ b ∘ F f) : naturality θ f + ... ≈ (η b ∘ θ b) ∘ F f : assoc) +--congr_arg (λx, η b ∘ x) (naturality θ f) -- this needed to be explicit for some reason (on Oct 24) + + infixr `∘n`:60 := compose + + definition foo (C : Precategory) (a b : C) (f g : hom a b) (p q : f ≈ g) : p ≈ q := + @truncation.is_hset.elim _ !homH f g p q + + protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) [fext : funext.{l_1 l_4}] : + η₃ ∘n (η₂ ∘n η₁) ≈ (η₃ ∘n η₂) ∘n η₁ := + dcongr_arg2 mk (funext.path_forall _ _ (λ x, !assoc)) sorry + + protected definition id {C D : Precategory} {F : functor C D} : natural_transformation F F := + mk (λa, id) (λa b f, !id_right ⬝ (!id_left⁻¹)) + protected definition ID {C D : Precategory} (F : functor C D) : natural_transformation F F := id + + protected theorem id_left (η : F ⟹ G) [fext : funext] : natural_transformation.compose id η ≈ η := + rec (λf H, path.dcongr_arg2 mk (funext.path_forall _ _ (λ x, !id_left)) sorry) η + + protected theorem id_right (η : F ⟹ G) [fext : funext] : natural_transformation.compose η id ≈ η := + rec (λf H, path.dcongr_arg2 mk (funext.path_forall _ _ (λ x, !id_right)) sorry) η +end natural_transformation diff --git a/library/hott/path.lean b/library/hott/path.lean index 4c933d7ed..16044d262 100644 --- a/library/hott/path.lean +++ b/library/hott/path.lean @@ -19,674 +19,679 @@ inductive path.{l} {A : Type.{l}} (a : A) : A → Type.{l} := idpath : path a a namespace path - variables {A B C : Type} {P : A → Type} {x y z t : A} +notation a ≈ b := path a b +notation x ≈ y `:>`:50 A:49 := @path A x y +definition idp {A : Type} {a : A} := idpath a - notation a ≈ b := path a b - notation x ≈ y `:>`:50 A:49 := @path A x y - definition idp {a : A} := idpath a +-- unbased path induction +definition rec' [reducible] {A : Type} {P : Π (a b : A), (a ≈ b) -> Type} + (H : Π (a : A), P a a idp) {a b : A} (p : a ≈ b) : P a b p := +path.rec (H a) p - -- unbased path induction - definition rec' [reducible] {P : Π (a b : A), (a ≈ b) -> Type} - (H : Π (a : A), P a a idp) {a b : A} (p : a ≈ b) : P a b p := - path.rec (H a) p +definition rec_on' [reducible] {A : Type} {P : Π (a b : A), (a ≈ b) -> Type} {a b : A} (p : a ≈ b) + (H : Π (a : A), P a a idp) : P a b p := +path.rec (H a) p - definition rec_on' [reducible] {P : Π (a b : A), (a ≈ b) -> Type} {a b : A} (p : a ≈ b) - (H : Π (a : A), P a a idp) : P a b p := - path.rec (H a) p +-- Concatenation and inverse +-- ------------------------- - -- Concatenation and inverse - -- ------------------------- +definition concat {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : x ≈ z := +path.rec (λu, u) q p - definition concat (p : x ≈ y) (q : y ≈ z) : x ≈ z := - path.rec (λu, u) q p +definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x := +path.rec (idpath x) p - definition inverse (p : x ≈ y) : y ≈ x := - path.rec (idpath x) p +notation p₁ ⬝ p₂ := concat p₁ p₂ +notation p ⁻¹ := inverse p - notation p₁ ⬝ p₂ := concat p₁ p₂ - notation p ⁻¹ := inverse p +-- In Coq, these are not needed, because concat and inv are kept transparent +-- definition inv_1 {A : Type} (x : A) : (idpath x)⁻¹ ≈ idpath x := idp - -- The 1-dimensional groupoid structure - -- ------------------------------------ +-- definition concat_11 {A : Type} (x : A) : idpath x ⬝ idpath x ≈ idpath x := idp - -- The identity path is a right unit. - definition concat_p1 (p : x ≈ y) : p ⬝ idp ≈ p := - rec_on p idp - -- The identity path is a right unit. - definition concat_1p (p : x ≈ y) : idp ⬝ p ≈ p := - rec_on p idp +-- The 1-dimensional groupoid structure +-- ------------------------------------ - -- Concatenation is associative. - definition concat_p_pp (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : - p ⬝ (q ⬝ r) ≈ (p ⬝ q) ⬝ r := - rec_on r (rec_on q idp) +-- The identity path is a right unit. +definition concat_p1 {A : Type} {x y : A} (p : x ≈ y) : p ⬝ idp ≈ p := +rec_on p idp - definition concat_pp_p (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : - (p ⬝ q) ⬝ r ≈ p ⬝ (q ⬝ r) := - rec_on r (rec_on q idp) +-- The identity path is a right unit. +definition concat_1p {A : Type} {x y : A} (p : x ≈ y) : idp ⬝ p ≈ p := +rec_on p idp - -- The left inverse law. - definition concat_pV (p : x ≈ y) : p ⬝ p⁻¹ ≈ idp := - rec_on p idp +-- Concatenation is associative. +definition concat_p_pp {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : + p ⬝ (q ⬝ r) ≈ (p ⬝ q) ⬝ r := +rec_on r (rec_on q idp) - -- The right inverse law. - definition concat_Vp (p : x ≈ y) : p⁻¹ ⬝ p ≈ idp := - rec_on p idp +definition concat_pp_p {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : + (p ⬝ q) ⬝ r ≈ p ⬝ (q ⬝ r) := +rec_on r (rec_on q idp) - -- Several auxiliary theorems about canceling inverses across associativity. These are somewhat - -- redundant, following from earlier theorems. +-- The left inverse law. +definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p ⬝ p⁻¹ ≈ idp := +rec_on p idp - definition concat_V_pp (p : x ≈ y) (q : y ≈ z) : p⁻¹ ⬝ (p ⬝ q) ≈ q := - rec_on q (rec_on p idp) +-- The right inverse law. +definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p⁻¹ ⬝ p ≈ idp := +rec_on p idp - definition concat_p_Vp (p : x ≈ y) (q : x ≈ z) : p ⬝ (p⁻¹ ⬝ q) ≈ q := - rec_on q (rec_on p idp) +-- Several auxiliary theorems about canceling inverses across associativity. These are somewhat +-- redundant, following from earlier theorems. - definition concat_pp_V (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q⁻¹ ≈ p := - rec_on q (rec_on p idp) +definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p⁻¹ ⬝ (p ⬝ q) ≈ q := +rec_on q (rec_on p idp) - definition concat_pV_p (p : x ≈ z) (q : y ≈ z) : (p ⬝ q⁻¹) ⬝ q ≈ p := - rec_on q (take p, rec_on p idp) p +definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p ⬝ (p⁻¹ ⬝ q) ≈ q := +rec_on q (rec_on p idp) - -- Inverse distributes over concatenation - definition inv_pp (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p⁻¹ := - rec_on q (rec_on p idp) +definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q⁻¹ ≈ p := +rec_on q (rec_on p idp) - definition inv_Vp (p : y ≈ x) (q : y ≈ z) : (p⁻¹ ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p := - rec_on q (rec_on p idp) +definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q⁻¹) ⬝ q ≈ p := +rec_on q (take p, rec_on p idp) p - -- universe metavariables - definition inv_pV (p : x ≈ y) (q : z ≈ y) : (p ⬝ q⁻¹)⁻¹ ≈ q ⬝ p⁻¹ := - rec_on p (take q, rec_on q idp) q +-- Inverse distributes over concatenation +definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p⁻¹ := +rec_on q (rec_on p idp) - definition inv_VV (p : y ≈ x) (q : z ≈ y) : (p⁻¹ ⬝ q⁻¹)⁻¹ ≈ q ⬝ p := - rec_on p (rec_on q idp) +definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p⁻¹ ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p := +rec_on q (rec_on p idp) - -- Inverse is an involution. - definition inv_V (p : x ≈ y) : p⁻¹⁻¹ ≈ p := - rec_on p idp +-- universe metavariables +definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p ⬝ q⁻¹)⁻¹ ≈ q ⬝ p⁻¹ := +rec_on p (take q, rec_on q idp) q - -- Theorems for moving things around in equations - -- ---------------------------------------------- +definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p⁻¹ ⬝ q⁻¹)⁻¹ ≈ q ⬝ p := +rec_on p (rec_on q idp) - definition moveR_Mp (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : - p ≈ (r⁻¹ ⬝ q) → (r ⬝ p) ≈ q := - rec_on r (take p h, concat_1p _ ⬝ h ⬝ concat_1p _) p +-- Inverse is an involution. +definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p⁻¹⁻¹ ≈ p := +rec_on p idp - definition moveR_pM (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : - r ≈ q ⬝ p⁻¹ → r ⬝ p ≈ q := - rec_on p (take q h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q +-- Theorems for moving things around in equations +-- ---------------------------------------------- - definition moveR_Vp (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : - p ≈ r ⬝ q → r⁻¹ ⬝ p ≈ q := - rec_on r (take q h, concat_1p _ ⬝ h ⬝ concat_1p _) q +definition moveR_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : + p ≈ (r⁻¹ ⬝ q) → (r ⬝ p) ≈ q := +rec_on r (take p h, concat_1p _ ⬝ h ⬝ concat_1p _) p - definition moveR_pV (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : - r ≈ q ⬝ p → r ⬝ p⁻¹ ≈ q := - rec_on p (take r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) r +definition moveR_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : + r ≈ q ⬝ p⁻¹ → r ⬝ p ≈ q := +rec_on p (take q h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q - definition moveL_Mp (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : - r⁻¹ ⬝ q ≈ p → q ≈ r ⬝ p := - rec_on r (take p h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) p +definition moveR_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : + p ≈ r ⬝ q → r⁻¹ ⬝ p ≈ q := +rec_on r (take q h, concat_1p _ ⬝ h ⬝ concat_1p _) q - definition moveL_pM (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : - q ⬝ p⁻¹ ≈ r → q ≈ r ⬝ p := - rec_on p (take q h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) q +definition moveR_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : + r ≈ q ⬝ p → r ⬝ p⁻¹ ≈ q := +rec_on p (take r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) r - definition moveL_Vp (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : - r ⬝ q ≈ p → q ≈ r⁻¹ ⬝ p := - rec_on r (take q h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) q +definition moveL_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : + r⁻¹ ⬝ q ≈ p → q ≈ r ⬝ p := +rec_on r (take p h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) p - definition moveL_pV (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : - q ⬝ p ≈ r → q ≈ r ⬝ p⁻¹ := - rec_on p (take r h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) r +definition moveL_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : + q ⬝ p⁻¹ ≈ r → q ≈ r ⬝ p := +rec_on p (take q h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) q - definition moveL_1M (p q : x ≈ y) : - p ⬝ q⁻¹ ≈ idp → p ≈ q := - rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p +definition moveL_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : + r ⬝ q ≈ p → q ≈ r⁻¹ ⬝ p := +rec_on r (take q h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) q - definition moveL_M1 (p q : x ≈ y) : - q⁻¹ ⬝ p ≈ idp → p ≈ q := - rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p +definition moveL_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : + q ⬝ p ≈ r → q ≈ r ⬝ p⁻¹ := +rec_on p (take r h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) r - definition moveL_1V (p : x ≈ y) (q : y ≈ x) : - p ⬝ q ≈ idp → p ≈ q⁻¹ := - rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p +definition moveL_1M {A : Type} {x y : A} (p q : x ≈ y) : + p ⬝ q⁻¹ ≈ idp → p ≈ q := +rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p - definition moveL_V1 (p : x ≈ y) (q : y ≈ x) : - q ⬝ p ≈ idp → p ≈ q⁻¹ := - rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p +definition moveL_M1 {A : Type} {x y : A} (p q : x ≈ y) : + q⁻¹ ⬝ p ≈ idp → p ≈ q := +rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p - definition moveR_M1 (p q : x ≈ y) : - idp ≈ p⁻¹ ⬝ q → p ≈ q := - rec_on p (take q h, h ⬝ (concat_1p _)) q +definition moveL_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : + p ⬝ q ≈ idp → p ≈ q⁻¹ := +rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p - definition moveR_1M (p q : x ≈ y) : - idp ≈ q ⬝ p⁻¹ → p ≈ q := - rec_on p (take q h, h ⬝ (concat_p1 _)) q +definition moveL_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : + q ⬝ p ≈ idp → p ≈ q⁻¹ := +rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p - definition moveR_1V (p : x ≈ y) (q : y ≈ x) : - idp ≈ q ⬝ p → p⁻¹ ≈ q := - rec_on p (take q h, h ⬝ (concat_p1 _)) q +definition moveR_M1 {A : Type} {x y : A} (p q : x ≈ y) : + idp ≈ p⁻¹ ⬝ q → p ≈ q := +rec_on p (take q h, h ⬝ (concat_1p _)) q - definition moveR_V1 (p : x ≈ y) (q : y ≈ x) : - idp ≈ p ⬝ q → p⁻¹ ≈ q := - rec_on p (take q h, h ⬝ (concat_1p _)) q +definition moveR_1M {A : Type} {x y : A} (p q : x ≈ y) : + idp ≈ q ⬝ p⁻¹ → p ≈ q := +rec_on p (take q h, h ⬝ (concat_p1 _)) q +definition moveR_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : + idp ≈ q ⬝ p → p⁻¹ ≈ q := +rec_on p (take q h, h ⬝ (concat_p1 _)) q - -- Transport - -- --------- +definition moveR_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) : + idp ≈ p ⬝ q → p⁻¹ ≈ q := +rec_on p (take q h, h ⬝ (concat_1p _)) q - definition transport [reducible] (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := - path.rec_on p u - -- This idiom makes the operation right associative. - notation p `▹`:65 x:64 := transport _ p x +-- Transport +-- --------- - definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x ≈ y) : f x ≈ f y := - path.rec_on p idp +definition transport [reducible] {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := +path.rec_on p u - definition ap01 := ap +-- This idiom makes the operation right associative. +notation p `▹`:65 x:64 := transport _ p x - definition homotopy [reducible] (f g : Πx, P x) : Type := - Πx : A, f x ≈ g x +definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x ≈ y) : f x ≈ f y := +path.rec_on p idp - notation f ∼ g := homotopy f g +definition ap01 := ap - definition apD10 {f g : Πx, P x} (H : f ≈ g) : f ∼ g := - λx, path.rec_on H idp +definition homotopy [reducible] {A : Type} {P : A → Type} (f g : Πx, P x) : Type := +Πx : A, f x ≈ g x - definition ap10 {f g : A → B} (H : f ≈ g) : f ∼ g := apD10 H +notation f ∼ g := homotopy f g - definition ap11 {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y := - rec_on H (rec_on p idp) +definition apD10 {A} {B : A → Type} {f g : Πx, B x} (H : f ≈ g) : f ∼ g := +λx, path.rec_on H idp - definition apD (f : Πa:A, P a) {x y : A} (p : x ≈ y) : p ▹ (f x) ≈ f y := - rec_on p idp +definition ap10 {A B} {f g : A → B} (H : f ≈ g) : f ∼ g := apD10 H +definition ap11 {A B} {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y := +rec_on H (rec_on p idp) - -- calc enviroment - -- --------------- +definition apD {A:Type} {B : A → Type} (f : Πa:A, B a) {x y : A} (p : x ≈ y) : p ▹ (f x) ≈ f y := +rec_on p idp - calc_subst transport - calc_trans concat - calc_refl idpath - calc_symm inverse - -- More theorems for moving things around in equations - -- --------------------------------------------------- +-- calc enviroment +-- --------------- - definition moveR_transport_p (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : - u ≈ p⁻¹ ▹ v → p ▹ u ≈ v := - rec_on p (take v, id) v +calc_subst transport +calc_trans concat +calc_refl idpath +calc_symm inverse - definition moveR_transport_V (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : - u ≈ p ▹ v → p⁻¹ ▹ u ≈ v := - rec_on p (take u, id) u +-- More theorems for moving things around in equations +-- --------------------------------------------------- - definition moveL_transport_V (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : - p ▹ u ≈ v → u ≈ p⁻¹ ▹ v := - rec_on p (take v, id) v +definition moveR_transport_p {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : + u ≈ p⁻¹ ▹ v → p ▹ u ≈ v := +rec_on p (take v, id) v - definition moveL_transport_p (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : - p⁻¹ ▹ u ≈ v → u ≈ p ▹ v := - rec_on p (take u, id) u +definition moveR_transport_V {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : + u ≈ p ▹ v → p⁻¹ ▹ u ≈ v := +rec_on p (take u, id) u - -- Functoriality of functions - -- -------------------------- +definition moveL_transport_V {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : + p ▹ u ≈ v → u ≈ p⁻¹ ▹ v := +rec_on p (take v, id) v - -- Here we prove that functions behave like functors between groupoids, and that [ap] itself is - -- functorial. +definition moveL_transport_p {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : + p⁻¹ ▹ u ≈ v → u ≈ p ▹ v := +rec_on p (take u, id) u - -- Functions take identity paths to identity paths - definition ap_1 (x : A) (f : A → B) : (ap f idp) ≈ idp :> (f x ≈ f x) := idp +-- Functoriality of functions +-- -------------------------- - definition apD_1 (x : A) (f : Π x : A, P x) : apD f idp ≈ idp :> (f x ≈ f x) := idp +-- Here we prove that functions behave like functors between groupoids, and that [ap] itself is +-- functorial. - -- Functions commute with concatenation. - definition ap_pp (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) : - ap f (p ⬝ q) ≈ (ap f p) ⬝ (ap f q) := - rec_on q (rec_on p idp) +-- Functions take identity paths to identity paths +definition ap_1 {A B : Type} (x : A) (f : A → B) : (ap f idp) ≈ idp :> (f x ≈ f x) := idp - definition ap_p_pp (f : A → B) {w x y z : A} (r : f w ≈ f x) (p : x ≈ y) (q : y ≈ z) : - r ⬝ (ap f (p ⬝ q)) ≈ (r ⬝ ap f p) ⬝ (ap f q) := - rec_on q (take p, rec_on p (concat_p_pp r idp idp)) p +definition apD_1 {A B} (x : A) (f : Π x : A, B x) : apD f idp ≈ idp :> (f x ≈ f x) := idp - definition ap_pp_p (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) : - (ap f (p ⬝ q)) ⬝ r ≈ (ap f p) ⬝ (ap f q ⬝ r) := - rec_on q (rec_on p (take r, concat_pp_p _ _ _)) r +-- Functions commute with concatenation. +definition ap_pp {A B : Type} (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) : + ap f (p ⬝ q) ≈ (ap f p) ⬝ (ap f q) := +rec_on q (rec_on p idp) - -- Functions commute with path inverses. - definition inverse_ap (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)⁻¹ ≈ ap f (p⁻¹) := - rec_on p idp +definition ap_p_pp {A B : Type} (f : A → B) {w x y z : A} (r : f w ≈ f x) (p : x ≈ y) (q : y ≈ z) : + r ⬝ (ap f (p ⬝ q)) ≈ (r ⬝ ap f p) ⬝ (ap f q) := +rec_on q (take p, rec_on p (concat_p_pp r idp idp)) p - definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p⁻¹) ≈ (ap f p)⁻¹ := - rec_on p idp +definition ap_pp_p {A B : Type} (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) : + (ap f (p ⬝ q)) ⬝ r ≈ (ap f p) ⬝ (ap f q ⬝ r) := +rec_on q (rec_on p (take r, concat_pp_p _ _ _)) r - -- [ap] itself is functorial in the first argument. +-- Functions commute with path inverses. +definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)⁻¹ ≈ ap f (p⁻¹) := +rec_on p idp - definition ap_idmap (p : x ≈ y) : ap id p ≈ p := - rec_on p idp +definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p⁻¹) ≈ (ap f p)⁻¹ := +rec_on p idp - definition ap_compose (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : - ap (g ∘ f) p ≈ ap g (ap f p) := - rec_on p idp +-- [ap] itself is functorial in the first argument. - -- Sometimes we don't have the actual function [compose]. - definition ap_compose' (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : - ap (λa, g (f a)) p ≈ ap g (ap f p) := - rec_on p idp +definition ap_idmap {A : Type} {x y : A} (p : x ≈ y) : ap id p ≈ p := +rec_on p idp - -- The action of constant maps. - definition ap_const (p : x ≈ y) (z : B) : - ap (λu, z) p ≈ idp := - rec_on p idp +definition ap_compose {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : + ap (g ∘ f) p ≈ ap g (ap f p) := +rec_on p idp - -- Naturality of [ap]. - definition concat_Ap {f g : A → B} (p : Π x, f x ≈ g x) {x y : A} (q : x ≈ y) : - (ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) := - rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) +-- Sometimes we don't have the actual function [compose]. +definition ap_compose' {A B C : Type} (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : + ap (λa, g (f a)) p ≈ ap g (ap f p) := +rec_on p idp - -- Naturality of [ap] at identity. - definition concat_A1p {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) : - (ap f q) ⬝ (p y) ≈ (p x) ⬝ q := - rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) +-- The action of constant maps. +definition ap_const {A B : Type} {x y : A} (p : x ≈ y) (z : B) : + ap (λu, z) p ≈ idp := +rec_on p idp - definition concat_pA1 {f : A → A} (p : Πx, x ≈ f x) {x y : A} (q : x ≈ y) : - (p x) ⬝ (ap f q) ≈ q ⬝ (p y) := - rec_on q (concat_p1 _ ⬝ (concat_1p _)⁻¹) +-- Naturality of [ap]. +definition concat_Ap {A B : Type} {f g : A → B} (p : Π x, f x ≈ g x) {x y : A} (q : x ≈ y) : + (ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) := +rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) - -- Naturality with other paths hanging around. +-- Naturality of [ap] at identity. +definition concat_A1p {A : Type} {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) : + (ap f q) ⬝ (p y) ≈ (p x) ⬝ q := +rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) - definition concat_pA_pp {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) - {w z : B} (r : w ≈ f x) (s : g y ≈ z) : - (r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (ap g q ⬝ s) := - rec_on s (rec_on q idp) +definition concat_pA1 {A : Type} {f : A → A} (p : Πx, x ≈ f x) {x y : A} (q : x ≈ y) : + (p x) ⬝ (ap f q) ≈ q ⬝ (p y) := +rec_on q (concat_p1 _ ⬝ (concat_1p _)⁻¹) - definition concat_pA_p {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) - {w : B} (r : w ≈ f x) : - (r ⬝ ap f q) ⬝ p y ≈ (r ⬝ p x) ⬝ ap g q := - rec_on q idp - - -- TODO: try this using the simplifier, and compare proofs - definition concat_A_pp {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) - {z : B} (s : g y ≈ z) : - (ap f q) ⬝ (p y ⬝ s) ≈ (p x) ⬝ (ap g q ⬝ s) := - rec_on s (rec_on q - (calc - (ap f idp) ⬝ (p x ⬝ idp) ≈ idp ⬝ p x : idp - ... ≈ p x : concat_1p _ - ... ≈ (p x) ⬝ (ap g idp ⬝ idp) : idp)) - -- This also works: - -- rec_on s (rec_on q (concat_1p _ ▹ idp)) - - definition concat_pA1_pp {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) - {w z : A} (r : w ≈ f x) (s : y ≈ z) : - (r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (q ⬝ s) := - rec_on s (rec_on q idp) - - definition concat_pp_A1p {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) - {w z : A} (r : w ≈ x) (s : g y ≈ z) : - (r ⬝ p x) ⬝ (ap g q ⬝ s) ≈ (r ⬝ q) ⬝ (p y ⬝ s) := - rec_on s (rec_on q idp) - - definition concat_pA1_p {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) - {w : A} (r : w ≈ f x) : - (r ⬝ ap f q) ⬝ p y ≈ (r ⬝ p x) ⬝ q := - rec_on q idp - - definition concat_A1_pp {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) - {z : A} (s : y ≈ z) : - (ap f q) ⬝ (p y ⬝ s) ≈ (p x) ⬝ (q ⬝ s) := - rec_on s (rec_on q (concat_1p _ ▹ idp)) - - definition concat_pp_A1 {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) - {w : A} (r : w ≈ x) : - (r ⬝ p x) ⬝ ap g q ≈ (r ⬝ q) ⬝ p y := - rec_on q idp - - definition concat_p_A1p {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) - {z : A} (s : g y ≈ z) : - p x ⬝ (ap g q ⬝ s) ≈ q ⬝ (p y ⬝ s) := - begin - apply (rec_on s), - apply (rec_on q), - apply (concat_1p (p x) ▹ idp) - end - - -- Action of [apD10] and [ap10] on paths - -- ------------------------------------- - - -- Application of paths between functions preserves the groupoid structure - - definition apD10_1 (f : Πx, P x) (x : A) : apD10 (idpath f) x ≈ idp := idp - - definition apD10_pp {f f' f'' : Πx, P x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : - apD10 (h ⬝ h') x ≈ apD10 h x ⬝ apD10 h' x := - rec_on h (take h', rec_on h' idp) h' - - definition apD10_V {f g : Πx : A, P x} (h : f ≈ g) (x : A) : - apD10 (h⁻¹) x ≈ (apD10 h x)⁻¹ := - rec_on h idp - - definition ap10_1 {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp - - definition ap10_pp {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : +-- Naturality with other paths hanging around. + +definition concat_pA_pp {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) + {w z : B} (r : w ≈ f x) (s : g y ≈ z) : + (r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (ap g q ⬝ s) := +rec_on s (rec_on q idp) + +definition concat_pA_p {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) + {w : B} (r : w ≈ f x) : + (r ⬝ ap f q) ⬝ p y ≈ (r ⬝ p x) ⬝ ap g q := +rec_on q idp + +-- TODO: try this using the simplifier, and compare proofs +definition concat_A_pp {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) + {z : B} (s : g y ≈ z) : + (ap f q) ⬝ (p y ⬝ s) ≈ (p x) ⬝ (ap g q ⬝ s) := +rec_on s (rec_on q + (calc + (ap f idp) ⬝ (p x ⬝ idp) ≈ idp ⬝ p x : idp + ... ≈ p x : concat_1p _ + ... ≈ (p x) ⬝ (ap g idp ⬝ idp) : idp)) +-- This also works: +-- rec_on s (rec_on q (concat_1p _ ▹ idp)) + +definition concat_pA1_pp {A : Type} {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) + {w z : A} (r : w ≈ f x) (s : y ≈ z) : + (r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (q ⬝ s) := +rec_on s (rec_on q idp) + +definition concat_pp_A1p {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) + {w z : A} (r : w ≈ x) (s : g y ≈ z) : + (r ⬝ p x) ⬝ (ap g q ⬝ s) ≈ (r ⬝ q) ⬝ (p y ⬝ s) := +rec_on s (rec_on q idp) + +definition concat_pA1_p {A : Type} {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) + {w : A} (r : w ≈ f x) : + (r ⬝ ap f q) ⬝ p y ≈ (r ⬝ p x) ⬝ q := +rec_on q idp + +definition concat_A1_pp {A : Type} {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) + {z : A} (s : y ≈ z) : + (ap f q) ⬝ (p y ⬝ s) ≈ (p x) ⬝ (q ⬝ s) := +rec_on s (rec_on q (concat_1p _ ▹ idp)) + +definition concat_pp_A1 {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) + {w : A} (r : w ≈ x) : + (r ⬝ p x) ⬝ ap g q ≈ (r ⬝ q) ⬝ p y := +rec_on q idp + +definition concat_p_A1p {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) + {z : A} (s : g y ≈ z) : + p x ⬝ (ap g q ⬝ s) ≈ q ⬝ (p y ⬝ s) := +begin + apply (rec_on s), + apply (rec_on q), + apply (concat_1p (p x) ▹ idp) +end + +-- Action of [apD10] and [ap10] on paths +-- ------------------------------------- + +-- Application of paths between functions preserves the groupoid structure + +definition apD10_1 {A} {B : A → Type} (f : Πx, B x) (x : A) : apD10 (idpath f) x ≈ idp := idp + +definition apD10_pp {A} {B : A → Type} {f f' f'' : Πx, B x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : + apD10 (h ⬝ h') x ≈ apD10 h x ⬝ apD10 h' x := +rec_on h (take h', rec_on h' idp) h' + +definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) : + apD10 (h⁻¹) x ≈ (apD10 h x)⁻¹ := +rec_on h idp + +definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp + +definition ap10_pp {A B} {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : ap10 (h ⬝ h') x ≈ ap10 h x ⬝ ap10 h' x := apD10_pp h h' x - definition ap10_V {f g : A → B} (h : f ≈ g) (x : A) : ap10 (h⁻¹) x ≈ (ap10 h x)⁻¹ := - apD10_V h x +definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h⁻¹) x ≈ (ap10 h x)⁻¹ := apD10_V h x - -- [ap10] also behaves nicely on paths produced by [ap] - definition ap_ap10 (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) : - ap h (ap10 p a) ≈ ap10 (ap (λ f', h ∘ f') p) a:= - rec_on p idp +-- [ap10] also behaves nicely on paths produced by [ap] +definition ap_ap10 {A B C} (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) : + ap h (ap10 p a) ≈ ap10 (ap (λ f', h ∘ f') p) a:= +rec_on p idp - -- Transport and the groupoid structure of paths - -- --------------------------------------------- +-- Transport and the groupoid structure of paths +-- --------------------------------------------- - definition transport_1 (P : A → Type) {x : A} (u : P x) : - idp ▹ u ≈ u := idp +definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) : + idp ▹ u ≈ u := idp - definition transport_pp (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) : - p ⬝ q ▹ u ≈ q ▹ p ▹ u := - rec_on q (rec_on p idp) +definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) : + p ⬝ q ▹ u ≈ q ▹ p ▹ u := +rec_on q (rec_on p idp) - definition transport_pV (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) : - p ▹ p⁻¹ ▹ z ≈ z := - (transport_pp P (p⁻¹) p z)⁻¹ ⬝ ap (λr, transport P r z) (concat_Vp p) +definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) : + p ▹ p⁻¹ ▹ z ≈ z := +(transport_pp P (p⁻¹) p z)⁻¹ ⬝ ap (λr, transport P r z) (concat_Vp p) - definition transport_Vp (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : - p⁻¹ ▹ p ▹ z ≈ z := - (transport_pp P p (p⁻¹) z)⁻¹ ⬝ ap (λr, transport P r z) (concat_pV p) +definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : + p⁻¹ ▹ p ▹ z ≈ z := +(transport_pp P p (p⁻¹) z)⁻¹ ⬝ ap (λr, transport P r z) (concat_pV p) - definition transport_p_pp (P : A → Type) - {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : - ap (λe, e ▹ u) (concat_p_pp p q r) ⬝ (transport_pp P (p ⬝ q) r u) ⬝ - ap (transport P r) (transport_pp P p q u) - ≈ (transport_pp P p (q ⬝ r) u) ⬝ (transport_pp P q r (p ▹ u)) - :> ((p ⬝ (q ⬝ r)) ▹ u ≈ r ▹ q ▹ p ▹ u) := - rec_on r (rec_on q (rec_on p idp)) +definition transport_p_pp {A : Type} (P : A → Type) + {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : + ap (λe, e ▹ u) (concat_p_pp p q r) ⬝ (transport_pp P (p ⬝ q) r u) ⬝ + ap (transport P r) (transport_pp P p q u) + ≈ (transport_pp P p (q ⬝ r) u) ⬝ (transport_pp P q r (p ▹ u)) + :> ((p ⬝ (q ⬝ r)) ▹ u ≈ r ▹ q ▹ p ▹ u) := +rec_on r (rec_on q (rec_on p idp)) - -- Here is another coherence lemma for transport. - definition transport_pVp (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : - transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z) := - rec_on p idp +-- Here is another coherence lemma for transport. +definition transport_pVp {A} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : + transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z) := +rec_on p idp - -- Dependent transport in a doubly dependent type. - -- should B, C and y all be explicit here? - definition transportD (P : A → Type) (Q : Π a : A, P a → Type) - {x1 x2 : A} (p : x1 ≈ x2) (y : P x1) (z : Q x1 y) : Q x2 (p ▹ y) := - rec_on p z - -- In Coq the variables B, C and y are explicit, but in Lean we can probably have them implicit using the following notation - notation p `▹D`:65 x:64 := transportD _ _ p _ x +-- Dependent transport in a doubly dependent type. +-- should B, C and y all be explicit here? +definition transportD {A : Type} (B : A → Type) (C : Π a : A, B a → Type) + {x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1 y) : C x2 (p ▹ y) := +rec_on p z +-- In Coq the variables B, C and y are explicit, but in Lean we can probably have them implicit using the following notation +notation p `▹D`:65 x:64 := transportD _ _ p _ x - -- Transporting along higher-dimensional paths - definition transport2 (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) : - p ▹ z ≈ q ▹ z := - ap (λp', p' ▹ z) r +-- Transporting along higher-dimensional paths +definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) : + p ▹ z ≈ q ▹ z := +ap (λp', p' ▹ z) r - notation p `▹2`:65 x:64 := transport2 _ p _ x +notation p `▹2`:65 x:64 := transport2 _ p _ x - -- An alternative definition. - definition transport2_is_ap10 (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) - (z : Q x) : - transport2 Q r z ≈ ap10 (ap (transport Q) r) z := - rec_on r idp +-- An alternative definition. +definition transport2_is_ap10 {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) + (z : Q x) : + transport2 Q r z ≈ ap10 (ap (transport Q) r) z := +rec_on r idp - definition transport2_p2p (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y} - (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) : - transport2 P (r1 ⬝ r2) z ≈ transport2 P r1 z ⬝ transport2 P r2 z := - rec_on r1 (rec_on r2 idp) +definition transport2_p2p {A : Type} (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y} + (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) : + transport2 P (r1 ⬝ r2) z ≈ transport2 P r1 z ⬝ transport2 P r2 z := +rec_on r1 (rec_on r2 idp) - definition transport2_V (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) : - transport2 Q (r⁻¹) z ≈ ((transport2 Q r z)⁻¹) := - rec_on r idp +definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) : + transport2 Q (r⁻¹) z ≈ ((transport2 Q r z)⁻¹) := +rec_on r idp - definition transportD2 (B C : A → Type) (D : Π(a:A), B a → C a → Type) - {x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▹ y) (p ▹ z) := - rec_on p w +definition transportD2 {A : Type} (B C : A → Type) (D : Π(a:A), B a → C a → Type) + {x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▹ y) (p ▹ z) := +rec_on p w - notation p `▹D2`:65 x:64 := transportD2 _ _ _ p _ _ x +notation p `▹D2`:65 x:64 := transportD2 _ _ _ p _ _ x - definition concat_AT (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q) - (s : z ≈ w) : - ap (transport P p) s ⬝ transport2 P r w ≈ transport2 P r z ⬝ ap (transport P q) s := - rec_on r (concat_p1 _ ⬝ (concat_1p _)⁻¹) +definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q) + (s : z ≈ w) : + ap (transport P p) s ⬝ transport2 P r w ≈ transport2 P r z ⬝ ap (transport P q) s := +rec_on r (concat_p1 _ ⬝ (concat_1p _)⁻¹) - -- TODO (from Coq library): What should this be called? - definition ap_transport {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) : - f y (p ▹ z) ≈ (p ▹ (f x z)) := - rec_on p idp +-- TODO (from Coq library): What should this be called? +definition ap_transport {A} {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) : + f y (p ▹ z) ≈ (p ▹ (f x z)) := +rec_on p idp - -- Transporting in particular fibrations - -- ------------------------------------- +-- Transporting in particular fibrations +-- ------------------------------------- - /- - From the Coq HoTT library: +/- +From the Coq HoTT library: - One frequently needs lemmas showing that transport in a certain dependent type is equal to some - more explicitly defined operation, defined according to the structure of that dependent type. - For most dependent types, we prove these lemmas in the appropriate file in the types/ - subdirectory. Here we consider only the most basic cases. - -/ +One frequently needs lemmas showing that transport in a certain dependent type is equal to some +more explicitly defined operation, defined according to the structure of that dependent type. +For most dependent types, we prove these lemmas in the appropriate file in the types/ +subdirectory. Here we consider only the most basic cases. +-/ - -- Transporting in a constant fibration. - definition transport_const (p : x ≈ y) (z : B) : transport (λx, B) p z ≈ z := - rec_on p idp +-- Transporting in a constant fibration. +definition transport_const {A B : Type} {x1 x2 : A} (p : x1 ≈ x2) (y : B) : + transport (λx, B) p y ≈ y := +rec_on p idp - definition transport2_const {p q : x ≈ y} (r : p ≈ q) (z : B) : - transport_const p z ≈ transport2 (λu, B) r z ⬝ transport_const q z := - rec_on r (concat_1p _)⁻¹ +definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 ≈ x2} (r : p ≈ q) (y : B) : + transport_const p y ≈ transport2 (λu, B) r y ⬝ transport_const q y := +rec_on r (concat_1p _)⁻¹ - -- Transporting in a pulled back fibration. - -- TODO: P can probably be implicit - definition transport_compose (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) : - transport (λx, P (f x)) p z ≈ transport P (ap f p) z := - rec_on p idp +-- Transporting in a pulled back fibration. +-- TODO: P can probably be implicit +definition transport_compose {A B} {x y : A} (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) : + transport (λx, P (f x)) p z ≈ transport P (ap f p) z := +rec_on p idp - definition transport_precompose (f : A → B) (g g' : B → C) (p : g ≈ g') : - transport (λh : B → C, g ∘ f ≈ h ∘ f) p idp ≈ ap (λh, h ∘ f) p := - rec_on p idp +definition transport_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') : + transport (λh : B → C, g ∘ f ≈ h ∘ f) p idp ≈ ap (λh, h ∘ f) p := +rec_on p idp - definition apD10_ap_precompose (f : A → B) (g g' : B → C) (p : g ≈ g') (a : A) : - apD10 (ap (λh : B → C, h ∘ f) p) a ≈ apD10 p (f a) := - rec_on p idp +definition apD10_ap_precompose {A B C} (f : A → B) (g g' : B → C) (p : g ≈ g') (a : A) : + apD10 (ap (λh : B → C, h ∘ f) p) a ≈ apD10 p (f a) := +rec_on p idp - definition apD10_ap_postcompose (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) : - apD10 (ap (λh : A → B, f ∘ h) p) a ≈ ap f (apD10 p a) := - rec_on p idp +definition apD10_ap_postcompose {A B C} (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) : + apD10 (ap (λh : A → B, f ∘ h) p) a ≈ ap f (apD10 p a) := +rec_on p idp - -- A special case of [transport_compose] which seems to come up a lot. - definition transport_idmap_ap (P : A → Type) x y (p : x ≈ y) (u : P x) : - transport P p u ≈ transport (λz, z) (ap P p) u := - rec_on p idp +-- A special case of [transport_compose] which seems to come up a lot. +definition transport_idmap_ap A (P : A → Type) x y (p : x ≈ y) (u : P x) : + transport P p u ≈ transport (λz, z) (ap P p) u := +rec_on p idp - -- The behavior of [ap] and [apD] - -- ------------------------------ +-- The behavior of [ap] and [apD] +-- ------------------------------ - -- In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. - definition apD_const (f : A → B) (p: x ≈ y) : - apD f p ≈ transport_const p (f x) ⬝ ap f p := - rec_on p idp +-- In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. +definition apD_const {A B} {x y : A} (f : A → B) (p: x ≈ y) : + apD f p ≈ transport_const p (f x) ⬝ ap f p := +rec_on p idp - -- The 2-dimensional groupoid structure - -- ------------------------------------ +-- The 2-dimensional groupoid structure +-- ------------------------------------ - -- Horizontal composition of 2-dimensional paths. - definition concat2 {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') : - p ⬝ q ≈ p' ⬝ q' := - rec_on h (rec_on h' idp) +-- Horizontal composition of 2-dimensional paths. +definition concat2 {A} {x y z : A} {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') : + p ⬝ q ≈ p' ⬝ q' := +rec_on h (rec_on h' idp) - infixl `◾`:75 := concat2 +infixl `◾`:75 := concat2 - -- 2-dimensional path inversion - definition inverse2 {p q : x ≈ y} (h : p ≈ q) : p⁻¹ ≈ q⁻¹ := - rec_on h idp +-- 2-dimensional path inversion +definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p⁻¹ ≈ q⁻¹ := +rec_on h idp - -- Whiskering - -- ---------- +-- Whiskering +-- ---------- - definition whiskerL (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p ⬝ q ≈ p ⬝ r := - idp ◾ h +definition whiskerL {A : Type} {x y z : A} (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p ⬝ q ≈ p ⬝ r := +idp ◾ h - definition whiskerR {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p ⬝ r ≈ q ⬝ r := - h ◾ idp +definition whiskerR {A : Type} {x y z : A} {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p ⬝ r ≈ q ⬝ r := +h ◾ idp - -- Unwhiskering, a.k.a. cancelling +-- Unwhiskering, a.k.a. cancelling - definition cancelL {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) := - rec_on p (take r, rec_on r (take q a, (concat_1p q)⁻¹ ⬝ a)) r q +definition cancelL {A} {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) := +rec_on p (take r, rec_on r (take q a, (concat_1p q)⁻¹ ⬝ a)) r q - definition cancelR {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) := - rec_on r (rec_on p (take q a, a ⬝ concat_p1 q)) q +definition cancelR {A} {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) := +rec_on r (rec_on p (take q a, a ⬝ concat_p1 q)) q - -- Whiskering and identity paths. +-- Whiskering and identity paths. - definition whiskerR_p1 {p q : x ≈ y} (h : p ≈ q) : - (concat_p1 p)⁻¹ ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h := - rec_on h (rec_on p idp) +definition whiskerR_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : + (concat_p1 p)⁻¹ ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h := +rec_on h (rec_on p idp) - definition whiskerR_1p (p : x ≈ y) (q : y ≈ z) : - whiskerR idp q ≈ idp :> (p ⬝ q ≈ p ⬝ q) := - rec_on q idp +definition whiskerR_1p {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : + whiskerR idp q ≈ idp :> (p ⬝ q ≈ p ⬝ q) := +rec_on q idp - definition whiskerL_p1 (p : x ≈ y) (q : y ≈ z) : - whiskerL p idp ≈ idp :> (p ⬝ q ≈ p ⬝ q) := - rec_on q idp +definition whiskerL_p1 {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : + whiskerL p idp ≈ idp :> (p ⬝ q ≈ p ⬝ q) := +rec_on q idp - definition whiskerL_1p {p q : x ≈ y} (h : p ≈ q) : - (concat_1p p) ⁻¹ ⬝ whiskerL idp h ⬝ concat_1p q ≈ h := - rec_on h (rec_on p idp) +definition whiskerL_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : + (concat_1p p) ⁻¹ ⬝ whiskerL idp h ⬝ concat_1p q ≈ h := +rec_on h (rec_on p idp) - definition concat2_p1 {p q : x ≈ y} (h : p ≈ q) : - h ◾ idp ≈ whiskerR h idp :> (p ⬝ idp ≈ q ⬝ idp) := - rec_on h idp +definition concat2_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : + h ◾ idp ≈ whiskerR h idp :> (p ⬝ idp ≈ q ⬝ idp) := +rec_on h idp - definition concat2_1p {p q : x ≈ y} (h : p ≈ q) : - idp ◾ h ≈ whiskerL idp h :> (idp ⬝ p ≈ idp ⬝ q) := - rec_on h idp +definition concat2_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : + idp ◾ h ≈ whiskerL idp h :> (idp ⬝ p ≈ idp ⬝ q) := +rec_on h idp - -- TODO: note, 4 inductions - -- The interchange law for concatenation. - definition concat_concat2 {p p' p'' : x ≈ y} {q q' q'' : y ≈ z} - (a : p ≈ p') (b : p' ≈ p'') (c : q ≈ q') (d : q' ≈ q'') : - (a ◾ c) ⬝ (b ◾ d) ≈ (a ⬝ b) ◾ (c ⬝ d) := - rec_on d (rec_on c (rec_on b (rec_on a idp))) +-- TODO: note, 4 inductions +-- The interchange law for concatenation. +definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x ≈ y} {q q' q'' : y ≈ z} + (a : p ≈ p') (b : p' ≈ p'') (c : q ≈ q') (d : q' ≈ q'') : + (a ◾ c) ⬝ (b ◾ d) ≈ (a ⬝ b) ◾ (c ⬝ d) := +rec_on d (rec_on c (rec_on b (rec_on a idp))) - definition concat_whisker {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') : - (whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') := - rec_on b (rec_on a (concat_1p _)⁻¹) +definition concat_whisker {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') : + (whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') := +rec_on b (rec_on a (concat_1p _)⁻¹) - -- Structure corresponding to the coherence equations of a bicategory. +-- Structure corresponding to the coherence equations of a bicategory. - -- The "pentagonator": the 3-cell witnessing the associativity pentagon. - definition pentagon {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) : - whiskerL p (concat_p_pp q r s) - ⬝ concat_p_pp p (q ⬝ r) s - ⬝ whiskerR (concat_p_pp p q r) s - ≈ concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s := - rec_on s (rec_on r (rec_on q (rec_on p idp))) +-- The "pentagonator": the 3-cell witnessing the associativity pentagon. +definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) : + whiskerL p (concat_p_pp q r s) + ⬝ concat_p_pp p (q ⬝ r) s + ⬝ whiskerR (concat_p_pp p q r) s + ≈ concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s := +rec_on s (rec_on r (rec_on q (rec_on p idp))) - -- The 3-cell witnessing the left unit triangle. - definition triangulator (p : x ≈ y) (q : y ≈ z) : - concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) := - rec_on q (rec_on p idp) +-- The 3-cell witnessing the left unit triangle. +definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : + concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) := +rec_on q (rec_on p idp) - definition eckmann_hilton {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p := - (!whiskerR_p1 ◾ !whiskerL_1p)⁻¹ - ⬝ (!concat_p1 ◾ !concat_p1) - ⬝ (!concat_1p ◾ !concat_1p) - ⬝ !concat_whisker - ⬝ (!concat_1p ◾ !concat_1p)⁻¹ - ⬝ (!concat_p1 ◾ !concat_p1)⁻¹ - ⬝ (!whiskerL_1p ◾ !whiskerR_p1) +definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p := + (!whiskerR_p1 ◾ !whiskerL_1p)⁻¹ + ⬝ (!concat_p1 ◾ !concat_p1) + ⬝ (!concat_1p ◾ !concat_1p) + ⬝ !concat_whisker + ⬝ (!concat_1p ◾ !concat_1p)⁻¹ + ⬝ (!concat_p1 ◾ !concat_p1)⁻¹ + ⬝ (!whiskerL_1p ◾ !whiskerR_p1) - -- The action of functions on 2-dimensional paths - definition ap02 (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q := - rec_on r idp +-- The action of functions on 2-dimensional paths +definition ap02 {A B : Type} (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q := +rec_on r idp - definition ap02_pp (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') : - ap02 f (r ⬝ r') ≈ ap02 f r ⬝ ap02 f r' := - rec_on r (rec_on r' idp) +definition ap02_pp {A B} (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') : + ap02 f (r ⬝ r') ≈ ap02 f r ⬝ ap02 f r' := +rec_on r (rec_on r' idp) - definition ap02_p2p (f : A → B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p') +definition ap02_p2p {A B} (f : A → B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p') (s : q ≈ q') : - ap02 f (r ◾ s) ≈ ap_pp f p q - ⬝ (ap02 f r ◾ ap02 f s) - ⬝ (ap_pp f p' q')⁻¹ := - rec_on r (rec_on s (rec_on q (rec_on p idp))) - -- rec_on r (rec_on s (rec_on p (rec_on q idp))) + ap02 f (r ◾ s) ≈ ap_pp f p q + ⬝ (ap02 f r ◾ ap02 f s) + ⬝ (ap_pp f p' q')⁻¹ := +rec_on r (rec_on s (rec_on q (rec_on p idp))) - definition apD02 {p q : x ≈ y} (f : Π x, P x) (r : p ≈ q) : - apD f p ≈ transport2 P r (f x) ⬝ apD f q := - rec_on r (concat_1p _)⁻¹ +-- rec_on r (rec_on s (rec_on p (rec_on q idp))) - -- And now for a lemma whose statement is much longer than its proof. - definition apD02_pp (P : A → Type) (f : Π x:A, P x) {x y : A} - {p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) : - apD02 f (r1 ⬝ r2) ≈ apD02 f r1 - ⬝ whiskerL (transport2 P r1 (f x)) (apD02 f r2) - ⬝ concat_p_pp _ _ _ - ⬝ (whiskerR ((transport2_p2p P r1 r2 (f x))⁻¹) (apD f p3)) := - rec_on r2 (rec_on r1 (rec_on p1 idp)) +definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) : + apD f p ≈ transport2 B r (f x) ⬝ apD f q := +rec_on r (concat_1p _)⁻¹ - /- From the Coq version: +-- And now for a lemma whose statement is much longer than its proof. +definition apD02_pp {A} (B : A → Type) (f : Π x:A, B x) {x y : A} + {p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) : + apD02 f (r1 ⬝ r2) ≈ apD02 f r1 + ⬝ whiskerL (transport2 B r1 (f x)) (apD02 f r2) + ⬝ concat_p_pp _ _ _ + ⬝ (whiskerR ((transport2_p2p B r1 r2 (f x))⁻¹) (apD f p3)) := +rec_on r2 (rec_on r1 (rec_on p1 idp)) - -- ** Tactics, hints, and aliases +/- From the Coq version: - -- [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. - -- Given as a notation not a definition so that the resultant terms are literally instances of - -- [concat], with no unfolding required. - Notation concatR := (λp q, concat q p). +-- ** Tactics, hints, and aliases - Hint Resolve - concat_1p concat_p1 concat_p_pp - inv_pp inv_V - : path_hints. +-- [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. +-- Given as a notation not a definition so that the resultant terms are literally instances of +-- [concat], with no unfolding required. +Notation concatR := (λp q, concat q p). - (* First try at a paths db - We want the RHS of the equation to become strictly simpler - Hint Rewrite - ⬝concat_p1 - ⬝concat_1p - ⬝concat_p_pp (* there is a choice here !*) - ⬝concat_pV - ⬝concat_Vp - ⬝concat_V_pp - ⬝concat_p_Vp - ⬝concat_pp_V - ⬝concat_pV_p - (*⬝inv_pp*) (* I am not sure about this one - ⬝inv_V - ⬝moveR_Mp - ⬝moveR_pM - ⬝moveL_Mp - ⬝moveL_pM - ⬝moveL_1M - ⬝moveL_M1 - ⬝moveR_M1 - ⬝moveR_1M - ⬝ap_1 - (* ⬝ap_pp - ⬝ap_p_pp ?*) - ⬝inverse_ap - ⬝ap_idmap - (* ⬝ap_compose - ⬝ap_compose'*) - ⬝ap_const - (* Unsure about naturality of [ap], was absent in the old implementation*) - ⬝apD10_1 - :paths. +Hint Resolve + concat_1p concat_p1 concat_p_pp + inv_pp inv_V + : path_hints. - Ltac hott_simpl := - autorewrite with paths in * |- * ; auto with path_hints. +(* First try at a paths db +We want the RHS of the equation to become strictly simpler +Hint Rewrite +⬝concat_p1 +⬝concat_1p +⬝concat_p_pp (* there is a choice here !*) +⬝concat_pV +⬝concat_Vp +⬝concat_V_pp +⬝concat_p_Vp +⬝concat_pp_V +⬝concat_pV_p +(*⬝inv_pp*) (* I am not sure about this one +⬝inv_V +⬝moveR_Mp +⬝moveR_pM +⬝moveL_Mp +⬝moveL_pM +⬝moveL_1M +⬝moveL_M1 +⬝moveR_M1 +⬝moveR_1M +⬝ap_1 +(* ⬝ap_pp +⬝ap_p_pp ?*) +⬝inverse_ap +⬝ap_idmap +(* ⬝ap_compose +⬝ap_compose'*) +⬝ap_const +(* Unsure about naturality of [ap], was absent in the old implementation*) +⬝apD10_1 +:paths. - -/ +Ltac hott_simpl := + autorewrite with paths in * |- * ; auto with path_hints. + +-/ end path