michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott): various changes in the HoTT library

Browse source
This commit is contained in:
Floris van Doorn 2015-09-10 18:32:52 -04:00 committed by Leonardo de Moura
parent bd3aa9cf54
commit e84b22864f
21 changed files with 467 additions and 172 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

71
hott/algebra/category/adjoint.hlean
View file

@ -20,8 +20,8 @@ namespace category
(G : D ⇒ C)
(η : 1 ⟹ G ∘f F)
(ε : F ∘f G ⟹ 1)
(H : Π(c : C), (ε (F c)) ∘ (F (η c)) = ID (F c))
(K : Π(d : D), (G (ε d)) ∘ (η (G d)) = ID (G d))
(H : Π(c : C), ε (F c) ∘ F (η c) = ID (F c))
(K : Π(d : D), G (ε d) ∘ η (G d) = ID (G d))
abbreviation right_adjoint := @is_left_adjoint.G
abbreviation unit := @is_left_adjoint.η
@ -88,7 +88,7 @@ namespace category
[H : fully_faithful F] (c c' : C) : (c ≅ c') ≃ (F c ≅ F c') :=
begin
fapply equiv.MK,
{ exact preserve_iso F},
{ exact to_fun_iso F},
{ apply iso_of_F_iso_F},
{ exact abstract begin
intro f, induction f with f F', induction F' with g p q, apply iso_eq,
@ -119,18 +119,18 @@ namespace category
to_fun_hom G' (natural_map ε d) ∘
natural_map η' (to_fun_ob G d) = id,
{ intro d, esimp,
rewrite [category.assoc],
rewrite [assoc],
rewrite [-assoc (G (ε' d))],
esimp, rewrite [nf_fn_eq_fn_nf_pt' G' ε η d],
esimp, rewrite [category.assoc],
esimp, rewrite [-category.assoc],
esimp, rewrite [assoc],
esimp, rewrite [-assoc],
rewrite [↑functor.compose, -respect_comp G],
rewrite [nf_fn_eq_fn_nf_pt ε ε' d,nf_fn_eq_fn_nf_pt η' η (G d),▸*],
rewrite [respect_comp G],
rewrite [category.assoc,▸*,-category.assoc (G (ε d))],
rewrite [assoc,▸*,-assoc (G (ε d))],
rewrite [↑functor.compose, -respect_comp G],
rewrite [H' (G d)],
rewrite [respect_id,▸*,category.id_right],
rewrite [respect_id,▸*,id_right],
apply K},
assert lem₃ : Π (d : carrier D),
(to_fun_hom G' (natural_map ε d) ∘
@ -138,17 +138,17 @@ namespace category
to_fun_hom G (natural_map ε' d) ∘
natural_map η (to_fun_ob G' d) = id,
{ intro d, esimp,
rewrite [category.assoc, -assoc (G' (ε d))],
rewrite [assoc, -assoc (G' (ε d))],
esimp, rewrite [nf_fn_eq_fn_nf_pt' G ε' η' d],
esimp, rewrite [category.assoc], esimp, rewrite [-category.assoc],
esimp, rewrite [assoc], esimp, rewrite [-assoc],
rewrite [↑functor.compose, -respect_comp G'],
rewrite [nf_fn_eq_fn_nf_pt ε' ε d,nf_fn_eq_fn_nf_pt η η' (G' d)],
esimp,
rewrite [respect_comp G'],
rewrite [category.assoc,▸*,-category.assoc (G' (ε' d))],
rewrite [assoc,▸*,-assoc (G' (ε' d))],
rewrite [↑functor.compose, -respect_comp G'],
rewrite [H (G' d)],
rewrite [respect_id,▸*,category.id_right],
rewrite [respect_id,▸*,id_right],
apply K'},
fapply lem₁,
{ fapply functor.eq_of_pointwise_iso,
@ -165,7 +165,7 @@ namespace category
rewrite functor.hom_of_eq_eq_of_pointwise_iso,
apply nat_trans_eq, intro c, esimp,
refine !assoc⁻¹ ⬝ ap (λx, _ ∘ x) (nf_fn_eq_fn_nf_pt η η' c) ⬝ !assoc ⬝ _,
esimp, rewrite [-respect_comp G',H c,respect_id G',▸*,category.id_left]},
esimp, rewrite [-respect_comp G',H c,respect_id G',▸*,id_left]},
{ clear lem₁, refine transport_hom_of_eq_left _ ε ⬝ _,
krewrite inv_of_eq_compose_left,
rewrite functor.inv_of_eq_eq_of_pointwise_iso,
@ -175,7 +175,7 @@ namespace category
end
definition full_of_fully_faithful (H : fully_faithful F) : full F :=
λc c', is_surjective.mk (λg, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv))
λc c' g, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv)
definition faithful_of_fully_faithful (H : fully_faithful F) : faithful F :=
λc c' f f' p, is_injective_of_is_embedding p
@ -198,6 +198,36 @@ namespace category
end
/-
section
variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d) -- we need some kind of naturality
include η ε
--definition inverse_of_unit_counit
private definition adj_η (c : C) : G (F c) ≅ c :=
to_fun_iso G (to_fun_iso F (η c)⁻¹ⁱ) ⬝i to_fun_iso G (ε (F c)) ⬝i η c
open iso
private theorem adjointify_adjH (c : C) :
to_hom (ε (F c)) ∘ F (to_hom (adj_η η ε c)⁻¹ⁱ) = id :=
begin
exact sorry
end
private theorem adjointify_adjK (d : D) :
G (to_hom (ε d)) ∘ to_hom (adj_η η ε (G d))⁻¹ⁱ = id :=
begin
exact sorry
end
variables (F G)
definition is_equivalence.mk : is_equivalence F :=
begin
fconstructor,
{ exact G},
{ }
end
end
definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
: fully_faithful F :=
@ -212,19 +242,6 @@ namespace category
{ exact sorry},
end
section
variables (F G)
variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1)
include η ε
--definition inverse_of_unit_counit
definition is_equivalence.mk : is_equivalence F :=
begin
exact sorry
end
end
definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) :=
sorry

1
hott/algebra/category/category.hlean
View file

@ -68,7 +68,6 @@ namespace category
(struct : category carrier)
attribute Category.struct [instance] [coercion]
attribute Category.to.precategory category.to_precategory [constructor]
definition Category.to_Precategory [constructor] [coercion] [reducible] (C : Category)
: Precategory :=

23
hott/algebra/category/functor.hlean
View file

@ -84,30 +84,41 @@ namespace functor
fapply @is_iso.mk, apply (F (f⁻¹)),
repeat (apply concat ; symmetry ; apply (respect_comp F) ;
apply concat ; apply (ap (λ x, to_fun_hom F x)) ;
(apply left_inverse | apply right_inverse);
(apply iso.left_inverse | apply iso.right_inverse);
apply (respect_id F) ),
end
definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f] [H' : is_iso (F f)] :
theorem respect_inv (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f] [H' : is_iso (F f)] :
F (f⁻¹) = (F f)⁻¹ :=
begin
fapply @left_inverse_eq_right_inverse, apply (F f),
transitivity to_fun_hom F (f⁻¹ ∘ f),
{symmetry, apply (respect_comp F)},
{transitivity to_fun_hom F category.id,
{congruence, apply left_inverse},
{congruence, apply iso.left_inverse},
{apply respect_id}},
apply right_inverse
apply iso.right_inverse
end
attribute preserve_is_iso [instance] [priority 100]
definition preserve_iso [constructor] (F : C ⇒ D) {a b : C} (f : a ≅ b) : F a ≅ F b :=
definition to_fun_iso [constructor] (F : C ⇒ D) {a b : C} (f : a ≅ b) : F a ≅ F b :=
iso.mk (F f)
definition respect_inv' (F : C ⇒ D) {a b : C} (f : hom a b) {H : is_iso f} : F (f⁻¹) = (F f)⁻¹ :=
theorem respect_inv' (F : C ⇒ D) {a b : C} (f : hom a b) {H : is_iso f} : F (f⁻¹) = (F f)⁻¹ :=
respect_inv F f
theorem respect_refl (F : C ⇒ D) (a : C) : to_fun_iso F (iso.refl a) = iso.refl (F a) :=
iso_eq !respect_id
theorem respect_symm (F : C ⇒ D) {a b : C} (f : a ≅ b)
: to_fun_iso F f⁻¹ⁱ = (to_fun_iso F f)⁻¹ⁱ :=
iso_eq !respect_inv
theorem respect_trans (F : C ⇒ D) {a b c : C} (f : a ≅ b) (g : b ≅ c)
: to_fun_iso F (f ⬝i g) = to_fun_iso F f ⬝i to_fun_iso F g :=
iso_eq !respect_comp
protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
!functor_mk_eq_constant (λa b f, idp)

3
hott/algebra/category/iso.hlean
View file

@ -160,6 +160,9 @@ namespace iso
protected definition trans [constructor] ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
mk (to_hom H2 ∘ to_hom H1)
infixl `⬝i`:75 := iso.trans
postfix [parsing-only] `⁻¹ⁱ`:(max + 1) := iso.symm
definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')
: iso.mk f = iso.mk f' :=
apd011 iso.mk p !is_hprop.elim

12
hott/algebra/category/yoneda.hlean
View file

@ -199,6 +199,14 @@ open functor
namespace yoneda
open category.set nat_trans lift
/-
These attributes make sure that the fields of the category "set" reduce to the right things
However, we don't want to have them globally, because that will unfold the composition g ∘ f
in a Category to category.category.comp g f
-/
local attribute Category.to.precategory category.to_precategory [constructor]
-- should this be defined as "yoneda_embedding Cᵒᵖ"?
definition contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C :=
functor_curry !hom_functor
@ -270,10 +278,10 @@ namespace yoneda
definition embedding_on_objects_yoneda_embedding (C : Category) :
is_embedding (ɏ : C → Cᵒᵖ ⇒ set) :=
begin
apply is_embedding.mk, intro c c', fapply is_equiv_of_equiv_of_homotopy,
intro c c', fapply is_equiv_of_equiv_of_homotopy,
{ exact !eq_equiv_iso ⬝e !iso_equiv_F_iso_F ⬝e !eq_equiv_iso⁻¹ᵉ},
{ intro p, induction p, esimp [equiv.trans, equiv.symm],
esimp [preserve_iso],
esimp [to_fun_iso],
rewrite -eq_of_iso_refl,
apply ap eq_of_iso, apply iso_eq, esimp,
apply nat_trans_eq, intro c',

51
hott/algebra/e_closure.hlean
View file

@ -31,9 +31,9 @@ section
(R : A → A → Type)
local abbreviation T := e_closure R
variables ⦃a a' : A⦄ {s : R a a'} {r : T a a}
variables ⦃a a' a'' : A⦄ {s : R a a'} {r : T a a} {B C : Type}
parameter {R}
protected definition e_closure.elim [unfold 8] {B : Type} {f : A → B}
protected definition e_closure.elim [unfold 8] {f : A → B}
(e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : f a = f a' :=
begin
induction t,
@ -115,5 +115,52 @@ section
intro a a' a'' t t', exact t ⬝r t',
end
definition e_closure.transport_left {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
(t : e_closure R a a') (p : a = a'')
: e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t :=
by induction p; exact !idp_con⁻¹
definition e_closure.transport_right {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
(t : e_closure R a a') (p : a' = a'')
: e_closure.elim e (p ▸ t) = e_closure.elim e t ⬝ (ap f p) :=
by induction p; reflexivity
definition e_closure.transport_lr {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
(t : e_closure R a a) (p : a = a')
: e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t ⬝ (ap f p) :=
by induction p; esimp; exact !idp_con⁻¹
--dependent elimination:
variables {P : B → Type} {Q : C → Type} {f : A → B} {g : B → C} {f' : Π(a : A), P (f a)}
protected definition e_closure.elimo [unfold 6]
(p : Π⦃a a' : A⦄, R a a' → f a = f a')
(po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a')
(t : T a a') : f' a =[e_closure.elim p t] f' a' :=
begin
induction t,
exact po r,
constructor,
exact v_0⁻¹ᵒ,
exact v_0 ⬝o v_1
end
definition ap_e_closure_elimo_h [unfold 12] {g' : Πb, Q (g b)}
(p : Π⦃a a' : A⦄, R a a' → f a = f a')
--(po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a')
(po : Π⦃a a' : A⦄ (s : R a a'), g' (f a) =[p s] g' (f a'))
(q : Π⦃a a' : A⦄ (s : R a a'), apdo g' (p s) = po s)
(t : T a a') : apdo g' (e_closure.elim p t) = e_closure.elimo p po t :=
begin
induction t,
apply q,
reflexivity,
esimp [e_closure.elim],
exact apdo_inv g' (e_closure.elim p r) ⬝ v_0⁻²ᵒ,
exact apdo_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (v_0 ◾o v_1)
end
end
end relation

6
hott/book.md
View file

@ -19,7 +19,7 @@ The rows indicate the chapters, the columns the sections.
| Ch 2 | + | + | + | + | . | + | + | + | + | + | + | + | + | + | + |
| Ch 3 | + | + | + | + | ½ | + | + | - | + | . | + | | | | |
| Ch 4 | - | + | - | + | . | + | - | - | + | | | | | | |
| Ch 5 | - | . | - | - | - | . | . | ½ | | | | | | | |
| Ch 5 | - | . | ½ | - | - | . | . | ½ | | | | | | | |
| Ch 6 | . | + | + | + | + | ½ | ½ | ¼ | ¼ | ¼ | ¾ | - | . | | |
| Ch 7 | + | + | + | - | - | - | - | | | | | | | | |
| Ch 8 | ¾ | - | - | - | - | - | - | - | - | - | | | | | |
@ -27,7 +27,7 @@ The rows indicate the chapters, the columns the sections.
| Ch 10 | - | - | - | - | - | | | | | | | | | | |
| Ch 11 | - | - | - | - | - | - | | | | | | | | | |
Things not in the book:
Theorems and definitions in the library which are not in the book:
* One major difference is that in this library we heavily use pathovers, so we need less theorems about transports, but instead corresponding theorems about pathovers. These are in [init.pathover](init/pathover.hlean). For higher paths there are [squares](cubical/square.hlean), [squareovers](cubical/squareover.hlean), and the rudiments of [cubes](cubical/cube.hlean) and [cubeovers](cubical/cubeover.hlean).
@ -99,7 +99,7 @@ Chapter 5: Induction
- 5.1 (Introduction to inductive types): not formalized
- 5.2 (Uniqueness of inductive types): no formalizable content
- 5.3 (W-types): related: [types.W](types/W.hlean)
- 5.3 (W-types): [types.W](types/W.hlean) defines W-types.
- 5.4 (Inductive types are initial algebras): not formalized
- 5.5 (Homotopy-inductive types): not formalized
- 5.6 (The general syntax of inductive definitions): no formalizable content

5
hott/cubical/square.hlean
View file

@ -64,7 +64,7 @@ namespace eq
square p p₁₂ p₀₁ p₂₁ :=
by induction r; exact s₁₁
definition vconcat_eq [unfold 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) :
definition vconcat_eq [unfold 12] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) :
square p₁₀ p p₀₁ p₂₁ :=
by induction r; exact s₁₁
@ -72,11 +72,10 @@ namespace eq
square p₁₀ p₁₂ p p₂₁ :=
by induction r; exact s₁₁
definition hconcat_eq [unfold 11] {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) :
definition hconcat_eq [unfold 12] {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) :
square p₁₀ p₁₂ p₀₁ p :=
by induction r; exact s₁₁
infix `⬝h`:75 := hconcat
infix `⬝v`:75 := vconcat
infix `⬝hp`:75 := hconcat_eq

60
hott/cubical/squareover.hlean
View file

@ -32,7 +32,9 @@ namespace eq
/-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
{p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
/-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/
{s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁}
{s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁}
{s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃}
{b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₄₀ : B a₄₀}
{b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {b₄₂ : B a₄₂}
{b₀₄ : B a₀₄} {b₂₄ : B a₂₄} {b₄₄ : B a₄₄}
@ -58,12 +60,66 @@ namespace eq
definition vdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀} (r : q₁₀ = q₁₀')
: squareover B vrfl q₁₀ q₁₀' idpo idpo :=
by induction r;exact vrflo
by induction r; exact vrflo
definition hdeg_squareover {q₀₁' : b₀₀ =[p₀₁] b₀₂} (r : q₀₁ = q₀₁')
: squareover B hrfl idpo idpo q₀₁ q₀₁' :=
by induction r; exact hrflo
definition hconcato
(t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (t₃₁ : squareover B s₃₁ q₃₀ q₃₂ q₂₁ q₄₁)
: squareover B (hconcat s₁₁ s₃₁) (q₁₀ ⬝o q₃₀) (q₁₂ ⬝o q₃₂) q₀₁ q₄₁ :=
by induction t₃₁; exact t₁₁
definition vconcato
(t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (t₁₃ : squareover B s₁₃ q₁₂ q₁₄ q₀₃ q₂₃)
: squareover B (vconcat s₁₁ s₁₃) q₁₀ q₁₄ (q₀₁ ⬝o q₀₃) (q₂₁ ⬝o q₂₃) :=
by induction t₁₃; exact t₁₁
definition hinverseo (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁)
: squareover B (hinverse s₁₁) q₁₀⁻¹ᵒ q₁₂⁻¹ᵒ q₂₁ q₀₁ :=
by induction t₁₁; constructor
definition vinverseo (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁)
: squareover B (vinverse s₁₁) q₁₂ q₁₀ q₀₁⁻¹ᵒ q₂₁⁻¹ᵒ :=
by induction t₁₁; constructor
definition eq_vconcato {q : b₀₀ =[p₁₀] b₂₀}
(r : q = q₁₀) (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) : squareover B s₁₁ q q₁₂ q₀₁ q₂₁ :=
by induction r; exact t₁₁
definition vconcato_eq {q : b₀₂ =[p₁₂] b₂₂}
(t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : q₁₂ = q) : squareover B s₁₁ q₁₀ q q₀₁ q₂₁ :=
by induction r; exact t₁₁
definition eq_hconcato {q : b₀₀ =[p₀₁] b₀₂}
(r : q = q₀₁) (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) : squareover B s₁₁ q₁₀ q₁₂ q q₂₁ :=
by induction r; exact t₁₁
definition hconcato_eq {q : b₂₀ =[p₂₁] b₂₂}
(t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : q₂₁ = q) : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q :=
by induction r; exact t₁₁
definition pathover_vconcato {p : a₀₀ = a₂₀} {sp : p = p₁₀} {q : b₀₀ =[p] b₂₀}
(r : change_path sp q = q₁₀) (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁)
: squareover B (sp ⬝pv s₁₁) q q₁₂ q₀₁ q₂₁ :=
by induction sp; induction r; exact t₁₁
definition vconcato_pathover {p : a₀₂ = a₂₂} {sp : p₁₂ = p} {q : b₀₂ =[p] b₂₂}
(t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : change_path sp q₁₂ = q)
: squareover B (s₁₁ ⬝vp sp) q₁₀ q q₀₁ q₂₁ :=
by induction sp; induction r; exact t₁₁
definition pathover_hconcato {p : a₀₀ = a₀₂} {sp : p = p₀₁} {q : b₀₀ =[p] b₀₂}
(r : change_path sp q = q₀₁) (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) :
squareover B (sp ⬝ph s₁₁) q₁₀ q₁₂ q q₂₁ :=
by induction sp; induction r; exact t₁₁
definition hconcato_pathover {p : a₂₀ = a₂₂} {sp : p₂₁ = p} {q : b₂₀ =[p] b₂₂}
(t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : change_path sp q₂₁ = q) :
squareover B (s₁₁ ⬝hp sp) q₁₀ q₁₂ q₀₁ q :=
by induction sp; induction r; exact t₁₁
-- relating squareovers to squares
definition square_of_squareover (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) :
square (!con_tr ⬝ ap (λa, p₂₁ ▸ a) (tr_eq_of_pathover q₁₀))

10
hott/eq2.hlean
View file

@ -12,8 +12,8 @@ open function
namespace eq
variables {A B C : Type} {f : A → B} {a a' a₁ a₂ a₃ a₄ : A} {b b' : B}
theorem ap_weakly_constant_eq (p : Πx, f x = b) (q : a = a') :
ap_weakly_constant p q =
theorem ap_is_constant_eq (p : Πx, f x = b) (q : a = a') :
ap_is_constant p q =
eq_con_inv_of_con_eq ((eq_of_square (square_of_pathover (apdo p q)))⁻¹ ⬝
whisker_left (p a) (ap_constant q b)) :=
begin
@ -48,10 +48,10 @@ namespace eq
idp :=
by cases p;apply vrefl
theorem ap_ap_weakly_constant {A B C : Type} (g : B → C) {f : A → B} {b : B}
theorem ap_ap_is_constant {A B C : Type} (g : B → C) {f : A → B} {b : B}
(p : Πx, f x = b) {x y : A} (q : x = y) :
square (ap (ap g) (ap_weakly_constant p q))
(ap_weakly_constant (λa, ap g (p a)) q)
square (ap (ap g) (ap_is_constant p q))
(ap_is_constant (λa, ap g (p a)) q)
(ap_compose g f q)⁻¹
(!ap_con ⬝ whisker_left _ !ap_inv) :=
begin

239
hott/function.hlean
View file

@ -7,39 +7,48 @@ Ported from Coq HoTT
Theorems about embeddings and surjections
-/
import hit.trunc types.equiv
import hit.trunc types.equiv cubical.square
open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod
variables {A B : Type} {f : A → B} {b : B}
variables {A B : Type} (f : A → B) {b : B}
structure is_embedding [class] (f : A → B) :=
(elim : Π(a a' : A), is_equiv (ap f : a = a' → f a = f a'))
definition is_embedding [class] (f : A → B) := Π(a a' : A), is_equiv (ap f : a = a' → f a = f a')
structure is_surjective [class] (f : A → B) :=
(elim : Π(b : B), ∥ fiber f b ∥)
definition is_surjective [class] (f : A → B) := Π(b : B), ∥ fiber f b ∥
structure is_split_surjective [class] (f : A → B) :=
(elim : Π(b : B), fiber f b)
definition is_split_surjective [class] (f : A → B) := Π(b : B), fiber f b
structure is_retraction [class] (f : A → B) :=
(sect : B → A)
(right_inverse : Π(b : B), f (sect b) = b)
definition is_weakly_constant [class] (f : A → B) (a a' : A) := f a = f a'
structure is_section [class] (f : A → B) :=
(retr : B → A)
(left_inverse : Π(a : A), retr (f a) = a)
definition is_weakly_constant [class] (f : A → B) := Π(a a' : A), f a = f a'
structure is_constant [class] (f : A → B) :=
(pt : B)
(eq : Π(a : A), f a = pt)
structure conditionally_constant [class] (f : A → B) :=
structure is_conditionally_constant [class] (f : A → B) :=
(g : ∥A∥ → B)
(eq : Π(a : A), f a = g (tr a))
namespace function
attribute is_embedding.elim [instance]
abbreviation sect [unfold 4] := @is_retraction.sect
abbreviation right_inverse [unfold 4] := @is_retraction.right_inverse
abbreviation retr [unfold 4] := @is_section.retr
abbreviation left_inverse [unfold 4] := @is_section.left_inverse
definition is_equiv_ap_of_embedding [instance] [H : is_embedding f] (a a' : A)
: is_equiv (ap f : a = a' → f a = f a') :=
H a a'
variable {f}
definition is_injective_of_is_embedding [reducible] [H : is_embedding f] {a a' : A}
: f a = f a' → a = a' :=
(ap f)⁻¹
@ -47,29 +56,18 @@ namespace function
definition is_embedding_of_is_injective [HA : is_hset A] [HB : is_hset B]
(H : Π(a a' : A), f a = f a' → a = a') : is_embedding f :=
begin
fapply is_embedding.mk,
intro a a',
fapply adjointify,
{exact (H a a')},
{intro p, apply is_hset.elim},
{intro p, apply is_hset.elim}
end
variable (f)
definition is_hprop_is_embedding [instance] (f : A → B) : is_hprop (is_embedding f) :=
begin
have H : (Π(a a' : A), is_equiv (@ap A B f a a')) ≃ is_embedding f,
begin
fapply equiv.MK,
{exact is_embedding.mk},
{intro h, cases h, exact elim},
{intro h, cases h, apply idp},
{intro p, apply idp},
end,
apply is_trunc_equiv_closed,
exact H,
end
definition is_hprop_is_embedding [instance] : is_hprop (is_embedding f) :=
by unfold is_embedding; exact _
definition is_hprop_fiber_of_is_embedding (f : A → B) [H : is_embedding f] (b : B) :
definition is_hprop_fiber_of_is_embedding [H : is_embedding f] (b : B) :
is_hprop (fiber f b) :=
begin
apply is_hprop.mk, intro v w,
@ -79,65 +77,72 @@ namespace function
{ esimp [is_injective_of_is_embedding], symmetry, apply right_inv}
end
variable {f}
definition is_surjective_rec_on {P : Type} (H : is_surjective f) (b : B) [Pt : is_hprop P]
(IH : fiber f b → P) : P :=
trunc.rec_on (is_surjective.elim f b) IH
trunc.rec_on (H b) IH
variable (f)
definition is_surjective_of_is_split_surjective [instance] [H : is_split_surjective f]
: is_surjective f :=
is_surjective.mk (λb, tr (is_split_surjective.elim f b))
λb, tr (H b)
definition is_hprop_is_surjective [instance] (f : A → B) : is_hprop (is_surjective f) :=
definition is_hprop_is_surjective [instance] : is_hprop (is_surjective f) :=
by unfold is_surjective; exact _
definition is_weakly_constant_ap [instance] [H : is_weakly_constant f] (a a' : A) :
is_weakly_constant (ap f : a = a' → f a = f a') :=
take p q : a = a',
have Π{b c : A} {r : b = c}, (H a b)⁻¹ ⬝ H a c = ap f r, from
(λb c r, eq.rec_on r !con.left_inv),
this⁻¹ ⬝ this
definition is_constant_ap [unfold 4] [instance] [H : is_constant f] (a a' : A)
: is_constant (ap f : a = a' → f a = f a') :=
begin
have H : (Π(b : B), merely (fiber f b)) ≃ is_surjective f,
begin
fapply equiv.MK,
{exact is_surjective.mk},
{intro h, cases h, exact elim},
{intro h, cases h, apply idp},
{intro p, apply idp},
end,
apply is_trunc_equiv_closed,
exact H,
induction H with b q,
fapply is_constant.mk,
{ exact q a ⬝ (q a')⁻¹},
{ intro p, induction p, exact !con.right_inv⁻¹}
end
-- definition is_hprop_is_split_surjective [instance] (f : A → B) : is_hprop (is_split_surjective f) :=
-- begin
-- have H : (Π(b : B), fiber f b) ≃ is_split_surjective f,
-- begin
-- fapply equiv.MK,
-- {exact is_split_surjective.mk},
-- {intro h, cases h, exact elim},
-- {intro h, cases h, apply idp},
-- {intro p, apply idp},
-- end,
-- apply is_trunc_equiv_closed,
-- exact H,
-- apply is_trunc_pi, intro b,
-- apply is_trunc_equiv_closed_rev,
-- apply fiber.sigma_char,
-- end
definition is_contr_is_retraction [instance] [H : is_equiv f] : is_contr (is_retraction f) :=
begin
have H2 : (Σ(g : B → A), Πb, f (g b) = b) ≃ is_retraction f,
begin
fapply equiv.MK,
{intro x, induction x with g p, constructor, exact p},
{intro h, induction h, apply sigma.mk, assumption},
{intro h, induction h, reflexivity},
{intro x, induction x, reflexivity},
end,
apply is_trunc_equiv_closed, exact H2,
apply is_equiv.is_contr_right_inverse
end
-- definition is_hprop_is_retraction [instance] (f : A → B) : is_hprop (is_retraction f) :=
-- begin
-- have H : (Σ(g : B → A), Πb, f (g b) = b) ≃ is_retraction f,
-- begin
-- fapply equiv.MK,
-- {intro x, induction x with g p, constructor, exact p},
-- {intro h, induction h, apply sigma.mk, assumption},
-- {intro h, induction h, reflexivity},
-- {intro x, induction x, reflexivity},
-- end,
-- apply is_trunc_equiv_closed,
-- exact H,
-- apply is_trunc_of_imp_is_trunc, intro x, induction x with g p,
-- apply is_contr_right_inverse
-- end
definition is_contr_is_section [instance] [H : is_equiv f] : is_contr (is_section f) :=
begin
have H2 : (Σ(g : B → A), Πa, g (f a) = a) ≃ is_section f,
begin
fapply equiv.MK,
{intro x, induction x with g p, constructor, exact p},
{intro h, induction h, apply sigma.mk, assumption},
{intro h, induction h, reflexivity},
{intro x, induction x, reflexivity},
end,
apply is_trunc_equiv_closed, exact H2,
fapply is_trunc_equiv_closed,
{apply sigma_equiv_sigma_id, intro g, apply eq_equiv_homotopy},
fapply is_trunc_equiv_closed,
{apply fiber.sigma_char},
fapply is_contr_fiber_of_is_equiv,
exact to_is_equiv (arrow_equiv_arrow_left_rev A (equiv.mk f H)),
end
definition is_embedding_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_embedding f :=
is_embedding.mk _
definition is_embedding_of_is_equiv [instance] [H : is_equiv f] : is_embedding f :=
λa a', _
definition is_equiv_of_is_surjective_of_is_embedding (f : A → B)
definition is_equiv_of_is_surjective_of_is_embedding
[H : is_embedding f] [H' : is_surjective f] : is_equiv f :=
@is_equiv_of_is_contr_fun _ _ _
(λb, is_surjective_rec_on H' b
@ -146,4 +151,92 @@ namespace function
fiber_eq ((ap f)⁻¹ ((point_eq a) ⬝ (point_eq a')⁻¹))
(by rewrite (right_inv (ap f)); rewrite inv_con_cancel_right))))
definition is_split_surjective_of_is_retraction [H : is_retraction f] : is_split_surjective f :=
λb, fiber.mk (sect f b) (right_inverse f b)
definition is_constant_compose_point [constructor] [instance] (b : B)
: is_constant (f ∘ point : fiber f b → B) :=
is_constant.mk b (λv, by induction v with a p;exact p)
definition is_embedding_of_is_hprop_fiber [H : Π(b : B), is_hprop (fiber f b)] : is_embedding f :=
begin
intro a a',
fapply adjointify,
{ intro p, exact ap point (is_hprop.elim (fiber.mk a p) (fiber.mk a' idp))},
{ exact abstract begin
intro p, rewrite [-ap_compose],
apply @is_constant.eq _ _ _ (is_constant_ap (f ∘ point) (fiber.mk a p) (fiber.mk a' idp))
end end },
{ intro p, induction p, rewrite [▸*,is_hprop_elim_self]},
end
-- definition is_embedding_of_is_section_inv' [H : is_section f] {a : A} {b : B} (p : f a = b) :
-- a = retr f b :=
-- (left_inverse f a)⁻¹ ⬝ ap (retr f) p
-- definition is_embedding_of_is_section_inv [H : is_section f] {a a' : A} (p : f a = f a') :
-- a = a' :=
-- is_embedding_of_is_section_inv' f p ⬝ left_inverse f a'
-- definition is_embedding_of_is_section [constructor] [instance] [H : is_section f]
-- : is_embedding f :=
-- begin
-- intro a a',
-- fapply adjointify,
-- { exact is_embedding_of_is_section_inv f},
-- { exact abstract begin
-- assert H2 : Π {b : B} (p : f a = b), ap f (is_embedding_of_is_section_inv' f p) = p ⬝ _,
-- { }
-- -- intro p, rewrite [+ap_con,-ap_compose],
-- -- check_expr natural_square (left_inverse f),
-- -- induction H with g q, esimp,
-- end end },
-- { intro p, induction p, esimp, apply con.left_inv},
-- end
definition is_retraction_of_is_equiv [instance] [H : is_equiv f] : is_retraction f :=
is_retraction.mk f⁻¹ (right_inv f)
definition is_section_of_is_equiv [instance] [H : is_equiv f] : is_section f :=
is_section.mk f⁻¹ (left_inv f)
definition is_equiv_of_is_section_of_is_retraction [H1 : is_retraction f] [H2 : is_section f]
: is_equiv f :=
let g := sect f in let h := retr f in
adjointify f
(g)
(right_inverse f)
(λa, calc
g (f a) = h (f (g (f a))) : left_inverse
... = h (f a) : right_inverse f
... = a : left_inverse)
section
local attribute is_equiv_of_is_section_of_is_retraction [instance]
variable (f)
definition is_hprop_is_retraction_prod_is_section : is_hprop (is_retraction f × is_section f) :=
begin
apply is_hprop_of_imp_is_contr, intro H, induction H with H1 H2,
exact _,
end
end
variable {f}
local attribute is_hprop_is_retraction_prod_is_section [instance]
definition is_retraction_prod_is_section_equiv_is_equiv
: (is_retraction f × is_section f) ≃ is_equiv f :=
begin
apply equiv_of_is_hprop,
intro H, induction H, apply is_equiv_of_is_section_of_is_retraction,
intro H, split, repeat exact _
end
/-
The definitions
is_surjective_of_is_equiv
is_equiv_equiv_is_embedding_times_is_surjective
are in types.trunc
-/
end function

31
hott/hit/two_quotient.hlean
View file

@ -9,6 +9,26 @@ import hit.circle eq2 algebra.e_closure cubical.cube
open quotient eq circle sum sigma equiv function relation
/-
This files defines a general class of nonrecursive HITs using just quotients.
We can define any HIT X which has
- a single 0-constructor
f : A → X (for some type A)
- a single 1-constructor
e : Π{a a' : A}, R a a' → a = a' (for some (type-valued) relation R on A)
and furthermore has 2-constructors which are all of the form
p = p'
where p, p' are of the form
- refl (f a), for some a : A;
- e r, for some r : R a a';
- ap f q, where q : a = a';
- inverses of such paths;
- concatenations of such paths.
so an example 2-constructor could be (as long as it typechecks):
ap f q' ⬝ ((e r)⁻¹ ⬝ ap f q)⁻¹ ⬝ e r' = idp
-/
namespace simple_two_quotient
section
@ -73,7 +93,8 @@ namespace simple_two_quotient
ap_e_closure_elim_h e (elim_e Pj Pa Pe) t
inductive simple_two_quotient_rel : C → C → Type :=
| Rmk {} : Π{a : A} {r : T a a} (q : Q r) (x : circle), simple_two_quotient_rel (f q x) (pre_aux q)
| Rmk {} : Π{a : A} {r : T a a} (q : Q r) (x : circle),
simple_two_quotient_rel (f q x) (pre_aux q)
open simple_two_quotient_rel
definition simple_two_quotient := quotient simple_two_quotient_rel
@ -84,7 +105,7 @@ namespace simple_two_quotient
definition incl1 (s : R a a') : incl0 a = incl0 a' := ap i (e s)
definition inclt (t : T a a') : incl0 a = incl0 a' := e_closure.elim incl1 t
-- "wrong" version inclt, which is ap i (p ⬝ q) instead of ap i p ⬝ ap i q
-- it is used in the proof, because inclt is easier to work with
-- it is used in the proof, because incltw is easier to work with
protected definition incltw (t : T a a') : incl0 a = incl0 a' := ap i (et t)
protected definition inclt_eq_incltw (t : T a a') : inclt t = incltw t :=
@ -96,7 +117,7 @@ namespace simple_two_quotient
protected definition incl2w (q : Q r) : incltw r = idp :=
(ap02 i (elim_loop (j a) (et r))⁻¹) ⬝
(ap_compose i (f q) loop)⁻¹ ⬝
ap_weakly_constant (incl2' q) loop ⬝
ap_is_constant (incl2' q) loop ⬝
!con.right_inv
definition incl2 (q : Q r) : inclt r = idp :=
@ -187,11 +208,11 @@ namespace simple_two_quotient
xrewrite [eq_top_of_square
((ap_compose_natural (elim P0 P1 P2) i (elim_loop (j a) (et r)))⁻¹ʰ⁻¹ᵛ ⬝h
(ap_ap_compose (elim P0 P1 P2) i (f q) loop)⁻¹ʰ⁻¹ᵛ ⬝h
ap_ap_weakly_constant (elim P0 P1 P2) (incl2' q) loop ⬝h
ap_ap_is_constant (elim P0 P1 P2) (incl2' q) loop ⬝h
ap_con_right_inv_sq (elim P0 P1 P2) (incl2' q base)),
↑[elim_incltw]],
apply whisker_tl,
rewrite [ap_weakly_constant_eq],
rewrite [ap_is_constant_eq],
xrewrite [naturality_apdo_eq (λx, !elim_eq_of_rel) loop],
rewrite [↑elim_2,rec_loop,square_of_pathover_concato_eq,square_of_pathover_eq_concato,
eq_of_square_vconcat_eq,eq_of_square_eq_vconcat],

2
hott/init/equiv.hlean
View file

@ -72,7 +72,7 @@ namespace is_equiv
private abbreviation adjointify_left_inv' (a : A) : g (f a) = a :=
ap g (ap f (inverse (sec a))) ⬝ ap g (ret (f a)) ⬝ sec a
private definition adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
private theorem adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
let fgretrfa := ap f (ap g (ret (f a))) in
let fgfinvsect := ap f (ap g (ap f (sec a)⁻¹)) in
let fgfa := f (g (f a)) in

84
hott/init/pathover.hlean
View file

@ -9,9 +9,9 @@ Basic theorems about pathovers
prelude
import .path .equiv
open equiv is_equiv equiv.ops
open equiv is_equiv equiv.ops function
variables {A A' : Type} {B B' : A → Type} {C : Π⦃a⦄, B a → Type}
variables {A A' : Type} {B B' : A → Type} {B'' : A' → Type} {C : Π⦃a⦄, B a → Type}
{a a₂ a₃ a₄ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄}
{b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄}
{c : C b} {c₂ : C b₂}
@ -27,16 +27,16 @@ namespace eq
/- equivalences with equality using transport -/
definition pathover_of_tr_eq [unfold 5 8] (r : p ▸ b = b₂) : b =[p] b₂ :=
by cases p; cases r; exact idpo
by cases p; cases r; constructor
definition pathover_of_eq_tr [unfold 5 8] (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ :=
by cases p; cases r; exact idpo
by cases p; cases r; constructor
definition tr_eq_of_pathover [unfold 8] (r : b =[p] b₂) : p ▸ b = b₂ :=
by cases r; exact idp
by cases r; reflexivity
definition eq_tr_of_pathover [unfold 8] (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ :=
by cases r; exact idp
by cases r; reflexivity
definition pathover_equiv_tr_eq [constructor] (p : a = a₂) (b : B a) (b₂ : B a₂)
: (b =[p] b₂) ≃ (p ▸ b = b₂) :=
@ -59,10 +59,10 @@ namespace eq
end
definition pathover_tr [unfold 5] (p : a = a₂) (b : B a) : b =[p] p ▸ b :=
by cases p;exact idpo
by cases p;constructor
definition tr_pathover [unfold 5] (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b :=
by cases p;exact idpo
by cases p;constructor
definition concato [unfold 12] (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ :=
pathover.rec_on r₂ r
@ -73,9 +73,6 @@ namespace eq
definition apdo [unfold 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ :=
eq.rec_on p idpo
definition oap [unfold 6] {C : A → Type} (f : Πa, B a → C a) (p : a = a₂) : f a =[p] f a₂ :=
eq.rec_on p idpo
definition concato_eq [unfold 10] (r : b =[p] b₂) (q : b₂ = b₂') : b =[p] b₂' :=
eq.rec_on q r
@ -115,15 +112,15 @@ namespace eq
by cases q;reflexivity
definition pathover_of_eq {a' a₂' : A'} (q : a' = a₂') : a' =[p] a₂' :=
by cases p;cases q;exact idpo
by cases p;cases q;constructor
definition pathover_constant [constructor] (p : a = a₂) (a' a₂' : A') : a' =[p] a₂' ≃ a' = a₂' :=
begin
fapply equiv.MK,
{ exact eq_of_pathover},
{ exact pathover_of_eq},
{ intro r, cases p, cases r, exact idp},
{ intro r, cases r, exact idp},
{ intro r, cases p, cases r, reflexivity},
{ intro r, cases r, reflexivity},
end
definition eq_of_pathover_idp [unfold 6] {b' : B a} (q : b =[idpath a] b') : b = b' :=
@ -166,7 +163,7 @@ namespace eq
--pathover with fibration B' ∘ f
definition pathover_ap [unfold 10] (B' : A' → Type) (f : A → A') {p : a = a₂}
{b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[p] b₂) : b =[ap f p] b₂ :=
by cases q; exact idpo
by cases q; constructor
definition pathover_of_pathover_ap (B' : A' → Type) (f : A → A') {p : a = a₂}
{b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[ap f p] b₂) : b =[p] b₂ :=
@ -179,15 +176,15 @@ namespace eq
{ apply pathover_ap},
{ apply pathover_of_pathover_ap},
{ intro q, cases p, esimp, apply (idp_rec_on q), apply idp},
{ intro q, cases q, exact idp},
{ intro q, cases q, reflexivity},
end
definition apdo_con (f : Πa, B a) (p : a = a₂) (q : a₂ = a₃)
: apdo f (p ⬝ q) = apdo f p ⬝o apdo f q :=
by cases p; cases q; exact idp
by cases p; cases q; reflexivity
definition apdo_inv (f : Πa, B a) (p : a = a₂) : apdo f p⁻¹ = (apdo f p)⁻¹ᵒ :=
by cases p; exact idp
by cases p; reflexivity
definition apdo_eq_pathover_of_eq_ap (f : A → A') (p : a = a₂) :
apdo f p = pathover_of_eq (ap f p) :=
@ -215,13 +212,13 @@ namespace eq
by induction q;reflexivity
variable {C}
definition apo (f : Πa, B a → B' a) {Ha : a = a₂} (Hb : b =[Ha] b₂)
: f a b =[Ha] f a₂ b₂ :=
by induction Hb; exact idpo
definition apo {f : A → A'} (g : Πa, B a → B'' (f a))
(q : b =[p] b₂) : g a b =[p] g a₂ b₂ :=
by induction q; constructor
definition apo011 (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
: f a b = f a₂ b₂ :=
by cases Hb; exact idp
by cases Hb; reflexivity
definition apo0111 (f : Πa b, C b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
(Hc : c =[apo011 C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ :=
@ -229,15 +226,23 @@ namespace eq
definition apo11 {f : Πb, C b} {g : Πb₂, C b₂} (r : f =[p] g)
{b : B a} {b₂ : B a₂} (q : b =[p] b₂) : f b =[apo011 C p q] g b₂ :=
by cases r; apply (idp_rec_on q); exact idpo
by cases r; apply (idp_rec_on q); constructor
definition apdo10 {f : Πb, C b} {g : Πb₂, C b₂} (r : f =[p] g)
(b : B a) : f b =[apo011 C p !pathover_tr] g (p ▸ b) :=
by cases r; exact idpo
by cases r; constructor
definition apo10 {f : B a → B' a} {g : B a₂ → B' a₂} (r : f =[p] g)
(b : B a) : f b =[p] g (p ▸ b) :=
by cases r; exact idpo
by cases r; constructor
definition apdo_compose1 (g : Πa, B a → B' a) (f : Πa, B a) (p : a = a₂)
: apdo (g ∘' f) p = apo g (apdo f p) :=
by induction p; reflexivity
definition apdo_compose2 (g : Πa', B'' a') (f : A → A') (p : a = a₂)
: apdo (λa, g (f a)) p = pathover_of_pathover_ap B'' f (apdo g (ap f p)) :=
by induction p; reflexivity
definition cono.right_inv_eq (q : b = b')
: concato_eq (pathover_idp_of_eq q) q⁻¹ = (idpo : b =[refl a] b) :=
@ -263,4 +268,33 @@ namespace eq
definition change_path_equiv' (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ :=
(left_inv f b)⁻¹ ⬝po change_path_equiv (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂
definition change_path_of_pathover (s : p = p') (r : b =[p] b₂) (r' : b =[p'] b₂)
(q : r =[s] r') : change_path s r = r' :=
by induction s; eapply idp_rec_on q; reflexivity
definition pathover_of_change_path (s : p = p') (r : b =[p] b₂) (r' : b =[p'] b₂)
(q : change_path s r = r') : r =[s] r' :=
by induction s; induction q; constructor
definition pathover_pathover_path [constructor] (s : p = p') (r : b =[p] b₂) (r' : b =[p'] b₂) :
(r =[s] r') ≃ change_path s r = r' :=
begin
fapply equiv.MK,
{ apply change_path_of_pathover},
{ apply pathover_of_change_path},
{ intro q, induction s, induction q, reflexivity},
{ intro q, induction s, eapply idp_rec_on q, reflexivity},
end
definition inverseo2 [unfold 10] {r r' : b =[p] b₂} (s : r = r') : r⁻¹ᵒ = r'⁻¹ᵒ :=
by induction s; reflexivity
definition concato2 [unfold 15 16] {r r' : b =[p] b₂} {r₂ r₂' : b₂ =[p₂] b₃}
(s : r = r') (s₂ : r₂ = r₂') : r ⬝o r₂ = r' ⬝o r₂' :=
by induction s; induction s₂; reflexivity
infixl `◾o`:75 := concato2
postfix [parsing-only] `⁻²ᵒ`:(max+10) := inverseo2 --this notation is abusive, should we use it?
end eq

20
hott/types/arrow.hlean
View file

@ -21,30 +21,34 @@ namespace pi
/- Functorial action -/
variables (f0 : A' → A) (f1 : B → B')
definition arrow_functor : (A → B) → (A' → B') := pi_functor f0 (λa, f1)
definition arrow_functor [unfold-full] : (A → B) → (A' → B') := pi_functor f0 (λa, f1)
/- Equivalences -/
definition is_equiv_arrow_functor
definition is_equiv_arrow_functor [constructor]
[H0 : is_equiv f0] [H1 : is_equiv f1] : is_equiv (arrow_functor f0 f1) :=
is_equiv_pi_functor f0 (λa, f1)
definition arrow_equiv_arrow_rev (f0 : A' ≃ A) (f1 : B ≃ B') : (A → B) ≃ (A' → B') :=
definition arrow_equiv_arrow_rev [constructor] (f0 : A' ≃ A) (f1 : B ≃ B')
: (A → B) ≃ (A' → B') :=
equiv.mk _ (is_equiv_arrow_functor f0 f1)
definition arrow_equiv_arrow (f0 : A ≃ A') (f1 : B ≃ B') : (A → B) ≃ (A' → B') :=
definition arrow_equiv_arrow [constructor] (f0 : A ≃ A') (f1 : B ≃ B') : (A → B) ≃ (A' → B') :=
arrow_equiv_arrow_rev (equiv.symm f0) f1
definition arrow_equiv_arrow_right (f1 : B ≃ B') : (A → B) ≃ (A → B') :=
variable (A)
definition arrow_equiv_arrow_right [constructor] (f1 : B ≃ B') : (A → B) ≃ (A → B') :=
arrow_equiv_arrow_rev equiv.refl f1
definition arrow_equiv_arrow_left_rev (f0 : A' ≃ A) : (A → B) ≃ (A' → B) :=
variables {A} (B)
definition arrow_equiv_arrow_left_rev [constructor] (f0 : A' ≃ A) : (A → B) ≃ (A' → B) :=
arrow_equiv_arrow_rev f0 equiv.refl
definition arrow_equiv_arrow_left (f0 : A ≃ A') : (A → B) ≃ (A' → B) :=
definition arrow_equiv_arrow_left [constructor] (f0 : A ≃ A') : (A → B) ≃ (A' → B) :=
arrow_equiv_arrow f0 equiv.refl
definition arrow_equiv_arrow_right' (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B') :=
variables {B}
definition arrow_equiv_arrow_right' [constructor] (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B') :=
pi_equiv_pi_id f1
/- Transport -/

2
hott/types/eq.hlean
View file

@ -91,7 +91,7 @@ namespace eq
theorem idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q :=
by cases q;reflexivity
definition ap_weakly_constant [unfold 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b)
definition ap_is_constant [unfold 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b)
{x y : A} (q : x = y) : ap f q = p x ⬝ (p y)⁻¹ :=
by induction q;exact !con.right_inv⁻¹

2
hott/types/equiv.hlean
View file

@ -36,7 +36,7 @@ namespace is_equiv
fapply is_trunc_equiv_closed,
{apply fiber.sigma_char},
fapply is_contr_fiber_of_is_equiv,
apply (to_is_equiv (arrow_equiv_arrow_right (equiv.mk f H))),
apply (to_is_equiv (arrow_equiv_arrow_right B (equiv.mk f H))),
end
definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ~ id)

2
hott/types/lift.hlean
View file

@ -129,7 +129,7 @@ namespace lift
definition is_embedding_lift [instance] : is_embedding lift :=
begin
apply is_embedding.mk, intro A A', fapply is_equiv.homotopy_closed,
intro A A', fapply is_equiv.homotopy_closed,
exact to_inv !lift_eq_lift_equiv,
exact _,
{ intro p, induction p,

9
hott/types/pi.hlean
View file

@ -170,7 +170,7 @@ namespace pi
/- Equivalences -/
definition is_equiv_pi_functor [instance] [H0 : is_equiv f0]
definition is_equiv_pi_functor [instance] [constructor] [H0 : is_equiv f0]
[H1 : Πa', is_equiv (f1 a')] : is_equiv (pi_functor f0 f1) :=
begin
apply (adjointify (pi_functor f0 f1) (pi_functor f0⁻¹
@ -187,15 +187,16 @@ namespace pi
end
end
definition pi_equiv_pi_of_is_equiv [H : is_equiv f0]
definition pi_equiv_pi_of_is_equiv [constructor] [H : is_equiv f0]
[H1 : Πa', is_equiv (f1 a')] : (Πa, B a) ≃ (Πa', B' a') :=
equiv.mk (pi_functor f0 f1) _
definition pi_equiv_pi (f0 : A' ≃ A) (f1 : Πa', (B (to_fun f0 a') ≃ B' a'))
definition pi_equiv_pi [constructor] (f0 : A' ≃ A) (f1 : Πa', (B (to_fun f0 a') ≃ B' a'))
: (Πa, B a) ≃ (Πa', B' a') :=
pi_equiv_pi_of_is_equiv (to_fun f0) (λa', to_fun (f1 a'))
definition pi_equiv_pi_id {P Q : A → Type} (g : Πa, P a ≃ Q a) : (Πa, P a) ≃ (Πa, Q a) :=
definition pi_equiv_pi_id [constructor] {P Q : A → Type} (g : Πa, P a ≃ Q a)
: (Πa, P a) ≃ (Πa, Q a) :=
pi_equiv_pi equiv.refl g
/- Truncatedness: any dependent product of n-types is an n-type -/

4
hott/types/trunc.hlean
View file

@ -65,7 +65,7 @@ namespace is_trunc
end
definition is_embedding_to_fun (A B : Type) : is_embedding (@to_fun A B) :=
is_embedding.mk (λf f', !is_equiv_ap_to_fun)
λf f', !is_equiv_ap_to_fun
definition is_trunc_trunctype [instance] (n : trunc_index) : is_trunc n.+1 (n-Type) :=
begin
@ -241,7 +241,7 @@ end trunc open trunc
namespace function
variables {A B : Type}
definition is_surjective_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_surjective f :=
is_surjective.mk (λb, !center)
λb, !center
definition is_equiv_equiv_is_embedding_times_is_surjective (f : A → B)
: is_equiv f ≃ (is_embedding f × is_surjective f) :=

2
src/emacs/lean-input.el
View file

@ -341,12 +341,14 @@ order for the change to take effect."
("-1f" . ("⁻¹ᶠ"))
("-1g" . ("⁻¹ᵍ"))
("-1h" . ("⁻¹ʰ"))
("-1i" . ("⁻¹ⁱ"))
("-1m" . ("⁻¹ᵐ"))
("-1o" . ("⁻¹ᵒ"))
("-1r" . ("⁻¹ʳ"))
("-1p" . ("⁻¹ᵖ"))
("-1v" . ("⁻¹ᵛ"))
("-2" . ("⁻²"))
("-2o" . ("⁻²ᵒ"))
("-3" . ("⁻³"))
("qed" . ("∎"))
("x" . ("×"))