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

fix(hott/init/path): reorder arguments of whisker_right

Browse source
This commit is contained in:
Floris van Doorn 2016-11-24 00:13:05 -05:00 committed by Leonardo de Moura
parent a9fc853985
commit e87a27cb4b
31 changed files with 196 additions and 195 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
hott/algebra/bundled.hlean
View file

@ -63,29 +63,29 @@ Group.struct G
attribute AddGroup.struct Group.struct [instance] [priority 2000] attribute AddGroup.struct Group.struct [instance] [priority 2000]
structure CommGroup := structure AbGroup :=
(carrier : Type) (struct : comm_group carrier) (carrier : Type) (struct : ab_group carrier)
attribute CommGroup.carrier [coercion] attribute AbGroup.carrier [coercion]
definition AddCommGroup : Type := CommGroup definition AddAbGroup : Type := AbGroup
definition AddCommGroup.mk [constructor] [reducible] (G : Type) (H : add_comm_group G) : definition AddAbGroup.mk [constructor] [reducible] (G : Type) (H : add_ab_group G) :
AddCommGroup := AddAbGroup :=
CommGroup.mk G H AbGroup.mk G H
definition AddCommGroup.struct [reducible] (G : AddCommGroup) : add_comm_group G := definition AddAbGroup.struct [reducible] (G : AddAbGroup) : add_ab_group G :=
CommGroup.struct G AbGroup.struct G
attribute AddCommGroup.struct CommGroup.struct [instance] [priority 2000] attribute AddAbGroup.struct AbGroup.struct [instance] [priority 2000]
definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group := definition Group_of_AbGroup [coercion] [constructor] (G : AbGroup) : Group :=
Group.mk G _ Group.mk G _
attribute algebra._trans_of_Group_of_CommGroup_1 attribute algebra._trans_of_Group_of_AbGroup_1
algebra._trans_of_Group_of_CommGroup algebra._trans_of_Group_of_AbGroup
algebra._trans_of_Group_of_CommGroup_3 [constructor] algebra._trans_of_Group_of_AbGroup_3 [constructor]
attribute algebra._trans_of_Group_of_CommGroup_2 [unfold 1] attribute algebra._trans_of_Group_of_AbGroup_2 [unfold 1]
-- structure AddSemigroup := -- structure AddSemigroup :=
@ -118,9 +118,9 @@ attribute algebra._trans_of_Group_of_CommGroup_2 [unfold 1]
-- attribute AddGroup.carrier [coercion] -- attribute AddGroup.carrier [coercion]
-- attribute AddGroup.struct [instance] -- attribute AddGroup.struct [instance]
-- structure AddCommGroup := -- structure AddAbGroup :=
-- (carrier : Type) (struct : add_comm_group carrier) -- (carrier : Type) (struct : add_ab_group carrier)
-- attribute AddCommGroup.carrier [coercion] -- attribute AddAbGroup.carrier [coercion]
-- attribute AddCommGroup.struct [instance] -- attribute AddAbGroup.struct [instance]
end algebra end algebra

2
hott/algebra/e_closure.hlean
View file

@ -158,7 +158,7 @@ section
ap_e_closure_elim_h e p t = ap_e_closure_elim_h e p t =
ap_e_closure_elim_h (λa a' s, ap g (e s)) (λa a' s, (ap_compose h g (e s))⁻¹ ⬝ p s) t := ap_e_closure_elim_h (λa a' s, ap g (e s)) (λa a' s, (ap_compose h g (e s))⁻¹ ⬝ p s) t :=
begin begin
refine whisker_right (eq_of_square (ap_ap_e_closure_elim g h e t)⁻¹ʰ)⁻¹ _ ⬝ _, refine whisker_right _ (eq_of_square (ap_ap_e_closure_elim g h e t)⁻¹ʰ)⁻¹ ⬝ _,
refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con, apply eq_of_square, refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con, apply eq_of_square,
apply transpose, apply transpose,
-- the rest of the proof is almost the same as the proof of ap_ap_e_closure_elim[_h]. -- the rest of the proof is almost the same as the proof of ap_ap_e_closure_elim[_h].

26
hott/algebra/group.hlean
View file

@ -346,7 +346,7 @@ section group
end group end group
structure comm_group [class] (A : Type) extends group A, comm_monoid A structure ab_group [class] (A : Type) extends group A, comm_monoid A
/- additive group -/ /- additive group -/
@ -551,21 +551,21 @@ section add_group
end add_group end add_group
definition add_comm_group [class] : Type → Type := comm_group definition add_ab_group [class] : Type → Type := ab_group
definition add_group_of_add_comm_group [reducible] [trans_instance] (A : Type) definition add_group_of_add_ab_group [reducible] [trans_instance] (A : Type)
[H : add_comm_group A] : add_group A := [H : add_ab_group A] : add_group A :=
@comm_group.to_group A H @ab_group.to_group A H
definition add_comm_monoid_of_add_comm_group [reducible] [trans_instance] (A : Type) definition add_comm_monoid_of_add_ab_group [reducible] [trans_instance] (A : Type)
[H : add_comm_group A] : add_comm_monoid A := [H : add_ab_group A] : add_comm_monoid A :=
@comm_group.to_comm_monoid A H @ab_group.to_comm_monoid A H
definition add_comm_group.to_comm_group {A : Type} [s : add_comm_group A] : comm_group A := s definition add_ab_group.to_ab_group {A : Type} [s : add_ab_group A] : ab_group A := s
definition comm_group.to_add_comm_group {A : Type} [s : comm_group A] : add_comm_group A := s definition ab_group.to_add_ab_group {A : Type} [s : ab_group A] : add_ab_group A := s
section add_comm_group section add_ab_group
variable [s : add_comm_group A] variable [s : add_ab_group A]
include s include s
theorem sub_add_eq_sub_sub (a b c : A) : a - (b + c) = a - b - c := theorem sub_add_eq_sub_sub (a b c : A) : a - (b + c) = a - b - c :=
@ -606,7 +606,7 @@ section add_comm_group
theorem neg_neg_sub_neg (a b : A) : - (-a - -b) = a - b := theorem neg_neg_sub_neg (a b : A) : - (-a - -b) = a - b :=
by rewrite [neg_sub, sub_neg_eq_add, neg_add_eq_sub] by rewrite [neg_sub, sub_neg_eq_add, neg_add_eq_sub]
end add_comm_group end add_ab_group
definition group_of_add_group (A : Type) [G : add_group A] : group A := definition group_of_add_group (A : Type) [G : add_group A] : group A :=
⦃group, ⦃group,

26
hott/algebra/group_theory.hlean
View file

@ -21,12 +21,12 @@ namespace group
definition Group.struct' [instance] [reducible] (G : Group) : group G := definition Group.struct' [instance] [reducible] (G : Group) : group G :=
Group.struct G Group.struct G
definition comm_group_Group_of_CommGroup [instance] [constructor] [priority 900] definition ab_group_Group_of_AbGroup [instance] [constructor] [priority 900]
(G : CommGroup) : comm_group (Group_of_CommGroup G) := (G : AbGroup) : ab_group (Group_of_AbGroup G) :=
begin esimp, exact _ end begin esimp, exact _ end
definition comm_group_pSet_of_Group [instance] (G : CommGroup) : comm_group (pSet_of_Group G) := definition ab_group_pSet_of_Group [instance] (G : AbGroup) : ab_group (pSet_of_Group G) :=
CommGroup.struct G AbGroup.struct G
definition group_pSet_of_Group [instance] [priority 900] (G : Group) : definition group_pSet_of_Group [instance] [priority 900] (G : Group) :
group (pSet_of_Group G) := group (pSet_of_Group G) :=
@ -463,14 +463,14 @@ namespace group
definition eq_of_isomorphism {G₁ G₂ : Group} (φ : G₁ ≃g G₂) : G₁ = G₂ := definition eq_of_isomorphism {G₁ G₂ : Group} (φ : G₁ ≃g G₂) : G₁ = G₂ :=
Group_eq (equiv_of_isomorphism φ) (respect_mul φ) Group_eq (equiv_of_isomorphism φ) (respect_mul φ)
definition comm_group.to_has_mul {A : Type} (H : comm_group A) : has_mul A := _ definition ab_group.to_has_mul {A : Type} (H : ab_group A) : has_mul A := _
local attribute comm_group.to_has_mul [coercion] local attribute ab_group.to_has_mul [coercion]
definition comm_group_eq {A : Type} {G H : comm_group A} definition ab_group_eq {A : Type} {G H : ab_group A}
(same_mul : Π(g h : A), @mul A G g h = @mul A H g h) (same_mul : Π(g h : A), @mul A G g h = @mul A H g h)
: G = H := : G = H :=
begin begin
have g_eq : @comm_group.to_group A G = @comm_group.to_group A H, from group_eq same_mul, have g_eq : @ab_group.to_group A G = @ab_group.to_group A H, from group_eq same_mul,
cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5, cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4 Gh5,
cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4 Hh5, cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4 Hh5,
have pm : Gm = Hm, from ap (@mul _ ∘ group.to_has_mul) g_eq, have pm : Gm = Hm, from ap (@mul _ ∘ group.to_has_mul) g_eq,
@ -487,18 +487,18 @@ namespace group
reflexivity reflexivity
end end
definition comm_group_pathover {A B : Type} {G : comm_group A} {H : comm_group B} {p : A = B} definition ab_group_pathover {A B : Type} {G : ab_group A} {H : ab_group B} {p : A = B}
(resp_mul : Π(g h : A), cast p (g * h) = cast p g * cast p h) : G =[p] H := (resp_mul : Π(g h : A), cast p (g * h) = cast p g * cast p h) : G =[p] H :=
begin begin
induction p, induction p,
apply pathover_idp_of_eq, exact comm_group_eq (resp_mul) apply pathover_idp_of_eq, exact ab_group_eq (resp_mul)
end end
definition CommGroup_eq_of_isomorphism {G₁ G₂ : CommGroup} (φ : G₁ ≃g G₂) : G₁ = G₂ := definition AbGroup_eq_of_isomorphism {G₁ G₂ : AbGroup} (φ : G₁ ≃g G₂) : G₁ = G₂ :=
begin begin
induction G₁, induction G₂, induction G₁, induction G₂,
apply apd011 CommGroup.mk (ua (equiv_of_isomorphism φ)), apply apd011 AbGroup.mk (ua (equiv_of_isomorphism φ)),
apply comm_group_pathover, apply ab_group_pathover,
intro g h, exact !cast_ua ⬝ respect_mul φ g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹ intro g h, exact !cast_ua ⬝ respect_mul φ g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹
end end

12
hott/algebra/homotopy_group.hlean
View file

@ -26,18 +26,18 @@ namespace eq
group (carrier (ptrunctype.to_pType (π[k + 1] A))) := group (carrier (ptrunctype.to_pType (π[k + 1] A))) :=
group_homotopy_group k A group_homotopy_group k A
definition comm_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*) definition ab_group_homotopy_group [constructor] [reducible] (n : ℕ) (A : Type*)
: comm_group (π[succ (succ n)] A) := : ab_group (π[succ (succ n)] A) :=
trunc_comm_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton trunc_ab_group concat inverse idp con.assoc idp_con con_idp con.left_inv eckmann_hilton
local attribute comm_group_homotopy_group [instance] local attribute ab_group_homotopy_group [instance]
definition ghomotopy_group [constructor] : Π(n : ℕ) [is_succ n] (A : Type*), Group definition ghomotopy_group [constructor] : Π(n : ℕ) [is_succ n] (A : Type*), Group
| (succ n) x A := Group.mk (π[succ n] A) _ | (succ n) x A := Group.mk (π[succ n] A) _
definition cghomotopy_group [constructor] : definition cghomotopy_group [constructor] :
Π(n : ℕ) [is_at_least_two n] (A : Type*), CommGroup Π(n : ℕ) [is_at_least_two n] (A : Type*), AbGroup
| (succ (succ n)) x A := CommGroup.mk (π[succ (succ n)] A) _ | (succ (succ n)) x A := AbGroup.mk (π[succ (succ n)] A) _
definition fundamental_group [constructor] (A : Type*) : Group := definition fundamental_group [constructor] (A : Type*) : Group :=
ghomotopy_group 1 A ghomotopy_group 1 A

70
hott/algebra/ordered_group.hlean
View file

@ -213,40 +213,40 @@ end
/- partially ordered groups -/ /- partially ordered groups -/
structure ordered_mul_comm_group [class] (A : Type) extends comm_group A, order_pair A := structure ordered_mul_ab_group [class] (A : Type) extends ab_group A, order_pair A :=
(mul_le_mul_left : Πa b, le a b → Πc, le (mul c a) (mul c b)) (mul_le_mul_left : Πa b, le a b → Πc, le (mul c a) (mul c b))
(mul_lt_mul_left : Πa b, lt a b → Π c, lt (mul c a) (mul c b)) (mul_lt_mul_left : Πa b, lt a b → Π c, lt (mul c a) (mul c b))
definition ordered_comm_group [class] : Type → Type := ordered_mul_comm_group definition ordered_ab_group [class] : Type → Type := ordered_mul_ab_group
definition add_comm_group_of_ordered_comm_group [reducible] [trans_instance] (A : Type) definition add_ab_group_of_ordered_ab_group [reducible] [trans_instance] (A : Type)
[H : ordered_comm_group A] : add_comm_group A := [H : ordered_ab_group A] : add_ab_group A :=
@ordered_mul_comm_group.to_comm_group A H @ordered_mul_ab_group.to_ab_group A H
theorem ordered_mul_comm_group.le_of_mul_le_mul_left [s : ordered_mul_comm_group A] {a b c : A} theorem ordered_mul_ab_group.le_of_mul_le_mul_left [s : ordered_mul_ab_group A] {a b c : A}
(H : a * b ≤ a * c) : b ≤ c := (H : a * b ≤ a * c) : b ≤ c :=
have H' : a⁻¹ * (a * b) ≤ a⁻¹ * (a * c), from ordered_mul_comm_group.mul_le_mul_left _ _ H _, have H' : a⁻¹ * (a * b) ≤ a⁻¹ * (a * c), from ordered_mul_ab_group.mul_le_mul_left _ _ H _,
by rewrite *inv_mul_cancel_left at H'; exact H' by rewrite *inv_mul_cancel_left at H'; exact H'
theorem ordered_mul_comm_group.lt_of_mul_lt_mul_left [s : ordered_mul_comm_group A] {a b c : A} theorem ordered_mul_ab_group.lt_of_mul_lt_mul_left [s : ordered_mul_ab_group A] {a b c : A}
(H : a * b < a * c) : b < c := (H : a * b < a * c) : b < c :=
have H' : a⁻¹ * (a * b) < a⁻¹ * (a * c), from ordered_mul_comm_group.mul_lt_mul_left _ _ H _, have H' : a⁻¹ * (a * b) < a⁻¹ * (a * c), from ordered_mul_ab_group.mul_lt_mul_left _ _ H _,
by rewrite *inv_mul_cancel_left at H'; exact H' by rewrite *inv_mul_cancel_left at H'; exact H'
definition ordered_mul_comm_group.to_ordered_mul_cancel_comm_monoid [reducible] [trans_instance] definition ordered_mul_ab_group.to_ordered_mul_cancel_comm_monoid [reducible] [trans_instance]
[s : ordered_mul_comm_group A] : ordered_mul_cancel_comm_monoid A := [s : ordered_mul_ab_group A] : ordered_mul_cancel_comm_monoid A :=
⦃ ordered_mul_cancel_comm_monoid, s, ⦃ ordered_mul_cancel_comm_monoid, s,
mul_left_cancel := @mul.left_cancel A _, mul_left_cancel := @mul.left_cancel A _,
mul_right_cancel := @mul.right_cancel A _, mul_right_cancel := @mul.right_cancel A _,
le_of_mul_le_mul_left := @ordered_mul_comm_group.le_of_mul_le_mul_left A _, le_of_mul_le_mul_left := @ordered_mul_ab_group.le_of_mul_le_mul_left A _,
lt_of_mul_lt_mul_left := @ordered_mul_comm_group.lt_of_mul_lt_mul_left A _⦄ lt_of_mul_lt_mul_left := @ordered_mul_ab_group.lt_of_mul_lt_mul_left A _⦄
definition ordered_comm_group.to_ordered_cancel_comm_monoid [reducible] [trans_instance] definition ordered_ab_group.to_ordered_cancel_comm_monoid [reducible] [trans_instance]
[s : ordered_comm_group A] : ordered_cancel_comm_monoid A := [s : ordered_ab_group A] : ordered_cancel_comm_monoid A :=
@ordered_mul_comm_group.to_ordered_mul_cancel_comm_monoid A s @ordered_mul_ab_group.to_ordered_mul_cancel_comm_monoid A s
section section
variables [s : ordered_comm_group A] (a b c d e : A) variables [s : ordered_ab_group A] (a b c d e : A)
include s include s
theorem neg_le_neg {a b : A} (H : a ≤ b) : -b ≤ -a := theorem neg_le_neg {a b : A} (H : a ≤ b) : -b ≤ -a :=
@ -603,37 +603,37 @@ end
/- linear ordered group with decidable order -/ /- linear ordered group with decidable order -/
structure decidable_linear_ordered_mul_comm_group [class] (A : Type) structure decidable_linear_ordered_mul_ab_group [class] (A : Type)
extends comm_group A, decidable_linear_order A := extends ab_group A, decidable_linear_order A :=
(mul_le_mul_left : Π a b, le a b → Π c, le (mul c a) (mul c b)) (mul_le_mul_left : Π a b, le a b → Π c, le (mul c a) (mul c b))
(mul_lt_mul_left : Π a b, lt a b → Π c, lt (mul c a) (mul c b)) (mul_lt_mul_left : Π a b, lt a b → Π c, lt (mul c a) (mul c b))
definition decidable_linear_ordered_comm_group [class] : Type → Type := definition decidable_linear_ordered_ab_group [class] : Type → Type :=
decidable_linear_ordered_mul_comm_group decidable_linear_ordered_mul_ab_group
definition add_comm_group_of_decidable_linear_ordered_comm_group [reducible] [trans_instance] (A : Type) definition add_ab_group_of_decidable_linear_ordered_ab_group [reducible] [trans_instance] (A : Type)
[H : decidable_linear_ordered_comm_group A] : add_comm_group A := [H : decidable_linear_ordered_ab_group A] : add_ab_group A :=
@decidable_linear_ordered_mul_comm_group.to_comm_group A H @decidable_linear_ordered_mul_ab_group.to_ab_group A H
definition decidable_linear_order_of_decidable_linear_ordered_comm_group [reducible] definition decidable_linear_order_of_decidable_linear_ordered_ab_group [reducible]
[trans_instance] (A : Type) [H : decidable_linear_ordered_comm_group A] : [trans_instance] (A : Type) [H : decidable_linear_ordered_ab_group A] :
decidable_linear_order A := decidable_linear_order A :=
@decidable_linear_ordered_mul_comm_group.to_decidable_linear_order A H @decidable_linear_ordered_mul_ab_group.to_decidable_linear_order A H
definition decidable_linear_ordered_mul_comm_group.to_ordered_mul_comm_group [reducible] definition decidable_linear_ordered_mul_ab_group.to_ordered_mul_ab_group [reducible]
[trans_instance] (A : Type) [s : decidable_linear_ordered_mul_comm_group A] : [trans_instance] (A : Type) [s : decidable_linear_ordered_mul_ab_group A] :
ordered_mul_comm_group A := ordered_mul_ab_group A :=
⦃ ordered_mul_comm_group, s, ⦃ ordered_mul_ab_group, s,
le_of_lt := @le_of_lt A _, le_of_lt := @le_of_lt A _,
lt_of_le_of_lt := @lt_of_le_of_lt A _, lt_of_le_of_lt := @lt_of_le_of_lt A _,
lt_of_lt_of_le := @lt_of_lt_of_le A _ ⦄ lt_of_lt_of_le := @lt_of_lt_of_le A _ ⦄
definition decidable_linear_ordered_comm_group.to_ordered_comm_group [reducible] [trans_instance] definition decidable_linear_ordered_ab_group.to_ordered_ab_group [reducible] [trans_instance]
(A : Type) [s : decidable_linear_ordered_comm_group A] : ordered_comm_group A := (A : Type) [s : decidable_linear_ordered_ab_group A] : ordered_ab_group A :=
@decidable_linear_ordered_mul_comm_group.to_ordered_mul_comm_group A s @decidable_linear_ordered_mul_ab_group.to_ordered_mul_ab_group A s
section section
variables [s : decidable_linear_ordered_comm_group A] variables [s : decidable_linear_ordered_ab_group A]
variables {a b c d e : A} variables {a b c d e : A}
include s include s

20
hott/algebra/ordered_ring.hlean
View file

@ -34,7 +34,7 @@ structure ordered_semiring (A : Type)
-- ordered_semiring.to_ordered_mul_cancel_comm_monoid to be an instance -/ -- ordered_semiring.to_ordered_mul_cancel_comm_monoid to be an instance -/
attribute ordered_semiring [class] attribute ordered_semiring [class]
definition add_comm_group_of_ordered_semiring [trans_instance] [reducible] (A : Type) definition add_ab_group_of_ordered_semiring [trans_instance] [reducible] (A : Type)
[H : ordered_semiring A] : semiring A := [H : ordered_semiring A] : semiring A :=
@ordered_semiring.to_semiring A H @ordered_semiring.to_semiring A H
@ -209,7 +209,7 @@ structure decidable_linear_ordered_semiring [class] (A : Type)
/- ring structures -/ /- ring structures -/
structure ordered_ring (A : Type) extends ring A, ordered_mul_comm_group A renaming structure ordered_ring (A : Type) extends ring A, ordered_mul_ab_group A renaming
mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
mul_left_inv→add_left_inv mul_comm→add_comm mul_le_mul_left→add_le_add_left mul_left_inv→add_left_inv mul_comm→add_comm mul_le_mul_left→add_le_add_left
mul_lt_mul_left→add_lt_add_left, mul_lt_mul_left→add_lt_add_left,
@ -218,16 +218,16 @@ structure ordered_ring (A : Type) extends ring A, ordered_mul_comm_group A renam
(mul_pos : Πa b, lt zero a → lt zero b → lt zero (mul a b)) (mul_pos : Πa b, lt zero a → lt zero b → lt zero (mul a b))
-- /- we make it a class now (and not as part of the structure) to avoid -- /- we make it a class now (and not as part of the structure) to avoid
-- ordered_ring.to_ordered_mul_comm_group to be an instance -/ -- ordered_ring.to_ordered_mul_ab_group to be an instance -/
attribute ordered_ring [class] attribute ordered_ring [class]
definition add_comm_group_of_ordered_ring [reducible] [trans_instance] (A : Type) definition add_ab_group_of_ordered_ring [reducible] [trans_instance] (A : Type)
[H : ordered_ring A] : ring A := [H : ordered_ring A] : ring A :=
@ordered_ring.to_ring A H @ordered_ring.to_ring A H
definition monoid_of_ordered_ring [reducible] [trans_instance] (A : Type) definition monoid_of_ordered_ring [reducible] [trans_instance] (A : Type)
[H : ordered_ring A] : ordered_comm_group A := [H : ordered_ring A] : ordered_ab_group A :=
@ordered_ring.to_ordered_mul_comm_group A H @ordered_ring.to_ordered_mul_ab_group A H
definition zero_ne_one_class_of_ordered_ring [reducible] [trans_instance] (A : Type) definition zero_ne_one_class_of_ordered_ring [reducible] [trans_instance] (A : Type)
[H : ordered_ring A] : zero_ne_one_class A := [H : ordered_ring A] : zero_ne_one_class A :=
@ -486,7 +486,7 @@ end
Search on mult_le_cancel_right1 in Rings.thy. -/ Search on mult_le_cancel_right1 in Rings.thy. -/
structure decidable_linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_comm_ring A, structure decidable_linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_comm_ring A,
decidable_linear_ordered_mul_comm_group A renaming decidable_linear_ordered_mul_ab_group A renaming
mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
mul_left_inv→add_left_inv mul_comm→add_comm mul_le_mul_left→add_le_add_left mul_left_inv→add_left_inv mul_comm→add_comm mul_le_mul_left→add_le_add_left
mul_lt_mul_left→add_lt_add_left mul_lt_mul_left→add_lt_add_left
@ -500,10 +500,10 @@ definition linear_ordered_comm_ring_of_decidable_linear_ordered_comm_ring [reduc
linear_ordered_comm_ring A := linear_ordered_comm_ring A :=
@decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring A H @decidable_linear_ordered_comm_ring.to_linear_ordered_comm_ring A H
definition decidable_linear_ordered_comm_group_of_decidable_linear_ordered_comm_ring [reducible] definition decidable_linear_ordered_ab_group_of_decidable_linear_ordered_comm_ring [reducible]
[trans_instance] (A : Type) [H : decidable_linear_ordered_comm_ring A] : [trans_instance] (A : Type) [H : decidable_linear_ordered_comm_ring A] :
decidable_linear_ordered_comm_group A := decidable_linear_ordered_ab_group A :=
@decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_mul_comm_group A H @decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_mul_ab_group A H
section section
variable [s : decidable_linear_ordered_comm_ring A] variable [s : decidable_linear_ordered_comm_ring A]

26
hott/algebra/ring.hlean
View file

@ -186,17 +186,17 @@ end comm_semiring
/- ring -/ /- ring -/
structure ring (A : Type) extends comm_group A renaming mul→add mul_assoc→add_assoc structure ring (A : Type) extends ab_group A renaming mul→add mul_assoc→add_assoc
one→zero one_mul→zero_add mul_one→add_zero inv→neg mul_left_inv→add_left_inv mul_comm→add_comm, one→zero one_mul→zero_add mul_one→add_zero inv→neg mul_left_inv→add_left_inv mul_comm→add_comm,
monoid A, distrib A monoid A, distrib A
/- we make it a class now (and not as part of the structure) to avoid /- we make it a class now (and not as part of the structure) to avoid
ring.to_comm_group to be an instance -/ ring.to_ab_group to be an instance -/
attribute ring [class] attribute ring [class]
definition add_comm_group_of_ring [reducible] [trans_instance] (A : Type) definition add_ab_group_of_ring [reducible] [trans_instance] (A : Type)
[H : ring A] : add_comm_group A := [H : ring A] : add_ab_group A :=
@ring.to_comm_group A H @ring.to_ab_group A H
definition monoid_of_ring [reducible] [trans_instance] (A : Type) definition monoid_of_ring [reducible] [trans_instance] (A : Type)
[H : ring A] : monoid A := [H : ring A] : monoid A :=
@ -485,7 +485,7 @@ theorem mk_cong (op : A → A) (a b : A) (H : a = b) : op a = op b :=
theorem mk_eq (a : A) : a = a := rfl theorem mk_eq (a : A) : a = a := rfl
theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H : c + a + b = 0) : theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_ab_group A] (a b c : A) (H : c + a + b = 0) :
-a + -b = c := -a + -b = c :=
begin begin
apply add_neg_eq_of_eq_add, apply add_neg_eq_of_eq_add,
@ -493,26 +493,26 @@ theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H
rewrite [add.comm, add.assoc, add.comm b, -add.assoc, H] rewrite [add.comm, add.assoc, add.comm b, -add.assoc, H]
end end
theorem neg_add_neg_helper [s : add_comm_group A] (a b c : A) (H : a + b = c) : -a + -b = -c := theorem neg_add_neg_helper [s : add_ab_group A] (a b c : A) (H : a + b = c) : -a + -b = -c :=
begin apply iff.mp !neg_eq_neg_iff_eq, rewrite [neg_add, *neg_neg, H] end begin apply iff.mp !neg_eq_neg_iff_eq, rewrite [neg_add, *neg_neg, H] end
theorem neg_add_pos_eq_of_eq_add [s : add_comm_group A] (a b c : A) (H : b = c + a) : -a + b = c := theorem neg_add_pos_eq_of_eq_add [s : add_ab_group A] (a b c : A) (H : b = c + a) : -a + b = c :=
begin apply neg_add_eq_of_eq_add, rewrite add.comm, exact H end begin apply neg_add_eq_of_eq_add, rewrite add.comm, exact H end
theorem neg_add_pos_helper1 [s : add_comm_group A] (a b c : A) (H : b + c = a) : -a + b = -c := theorem neg_add_pos_helper1 [s : add_ab_group A] (a b c : A) (H : b + c = a) : -a + b = -c :=
begin apply neg_add_eq_of_eq_add, apply eq_add_neg_of_add_eq H end begin apply neg_add_eq_of_eq_add, apply eq_add_neg_of_add_eq H end
theorem neg_add_pos_helper2 [s : add_comm_group A] (a b c : A) (H : a + c = b) : -a + b = c := theorem neg_add_pos_helper2 [s : add_ab_group A] (a b c : A) (H : a + c = b) : -a + b = c :=
begin apply neg_add_eq_of_eq_add, rewrite H end begin apply neg_add_eq_of_eq_add, rewrite H end
theorem pos_add_neg_helper [s : add_comm_group A] (a b c : A) (H : b + a = c) : a + b = c := theorem pos_add_neg_helper [s : add_ab_group A] (a b c : A) (H : b + a = c) : a + b = c :=
by rewrite [add.comm, H] by rewrite [add.comm, H]
theorem sub_eq_add_neg_helper [s : add_comm_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁) theorem sub_eq_add_neg_helper [s : add_ab_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁)
(H₂ : t₂ = w₂) (H : w₁ + -w₂ = e) : t₁ - t₂ = e := (H₂ : t₂ = w₂) (H : w₁ + -w₂ = e) : t₁ - t₂ = e :=
by rewrite [sub_eq_add_neg, H₁, H₂, H] by rewrite [sub_eq_add_neg, H₁, H₂, H]
theorem pos_add_pos_helper [s : add_comm_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂) theorem pos_add_pos_helper [s : add_ab_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂)
(H : h₁ + h₂ = c) : a + b = c := (H : h₁ + h₂ = c) : a + b = c :=
by rewrite [H₁, H₂, H] by rewrite [H₁, H₂, H]

6
hott/algebra/trunc_group.hlean
View file

@ -96,9 +96,9 @@ namespace algebra
mul_left_inv := algebra.trunc_mul_left_inv 0 mul_left_inv, mul_left_inv := algebra.trunc_mul_left_inv 0 mul_left_inv,
is_set_carrier := _⦄ is_set_carrier := _⦄
definition trunc_comm_group [constructor] (mul_comm : ∀a b, mul a b = mul b a) definition trunc_ab_group [constructor] (mul_comm : ∀a b, mul a b = mul b a)
: comm_group (trunc 0 A) := : ab_group (trunc 0 A) :=
⦃comm_group, trunc_group, mul_comm := algebra.trunc_mul_comm 0 mul_comm⦄ ⦃ab_group, trunc_group, mul_comm := algebra.trunc_mul_comm 0 mul_comm⦄
end end
end algebra end algebra

4
hott/cubical/square.hlean
View file

@ -378,11 +378,11 @@ namespace eq
by induction r;induction p;reflexivity by induction r;induction p;reflexivity
definition eq_of_square_eq_vconcat {p : a₀₀ = a₂₀} (r : p = p₁₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) definition eq_of_square_eq_vconcat {p : a₀₀ = a₂₀} (r : p = p₁₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
: eq_of_square (r ⬝pv s₁₁) = whisker_right r p₂₁ ⬝ eq_of_square s₁₁ := : eq_of_square (r ⬝pv s₁₁) = whisker_right p₂₁ r ⬝ eq_of_square s₁₁ :=
by induction s₁₁;cases r;reflexivity by induction s₁₁;cases r;reflexivity
definition eq_of_square_eq_hconcat {p : a₀₀ = a₀₂} (r : p = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) definition eq_of_square_eq_hconcat {p : a₀₀ = a₀₂} (r : p = p₀₁) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
: eq_of_square (r ⬝ph s₁₁) = eq_of_square s₁₁ ⬝ (whisker_right r p₁₂)⁻¹ := : eq_of_square (r ⬝ph s₁₁) = eq_of_square s₁₁ ⬝ (whisker_right p₁₂ r)⁻¹ :=
by induction r;reflexivity by induction r;reflexivity
definition eq_of_square_vconcat_eq {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) definition eq_of_square_vconcat_eq {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p)

4
hott/eq2.hlean
View file

@ -44,7 +44,7 @@ namespace eq
theorem ap_con_left_inv_sq {A B : Type} {a1 a2 : A} (f : A → B) (p : a1 = a2) : theorem ap_con_left_inv_sq {A B : Type} {a1 a2 : A} (f : A → B) (p : a1 = a2) :
square (ap (ap f) (con.left_inv p)) square (ap (ap f) (con.left_inv p))
(con.left_inv (ap f p)) (con.left_inv (ap f p))
(ap_con f p⁻¹ p ⬝ whisker_right (ap_inv f p) _) (ap_con f p⁻¹ p ⬝ whisker_right _ (ap_inv f p))
idp := idp :=
by cases p;apply vrefl by cases p;apply vrefl
@ -91,7 +91,7 @@ namespace eq
natural_square_tr (ap_compose g f) r natural_square_tr (ap_compose g f) r
theorem whisker_right_eq_of_con_inv_eq_idp {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp) : theorem whisker_right_eq_of_con_inv_eq_idp {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp) :
whisker_right (eq_of_con_inv_eq_idp r) q⁻¹ ⬝ con.right_inv q = r := whisker_right q⁻¹ (eq_of_con_inv_eq_idp r) ⬝ con.right_inv q = r :=
by induction q; esimp at r; cases r; reflexivity by induction q; esimp at r; cases r; reflexivity
theorem ap_eq_of_con_inv_eq_idp (f : A → B) {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp) theorem ap_eq_of_con_inv_eq_idp (f : A → B) {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp)

1
hott/hit/two_quotient.hlean
View file

@ -279,6 +279,7 @@ namespace simple_two_quotient
⦃a : A⦄ ⦃r : T a a⦄ (q : Q r) : ap (elim P0 P1 P2) (incl2' q base) = idpath (P0 a) := ⦃a : A⦄ ⦃r : T a a⦄ (q : Q r) : ap (elim P0 P1 P2) (incl2' q base) = idpath (P0 a) :=
!elim_eq_of_rel !elim_eq_of_rel
local attribute whisker_right [reducible]
protected theorem elim_incl2w {P : Type} (P0 : A → P) protected theorem elim_incl2w {P : Type} (P0 : A → P)
(P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a') (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
(P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp) (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)

46
hott/homotopy/EM.hlean
View file

@ -192,7 +192,7 @@ end EM
open hopf susp open hopf susp
namespace EM namespace EM
/- EM1 G is an h-space if G is an abelian group. This allows us to construct K(G,n) for n ≥ 2 -/ /- EM1 G is an h-space if G is an abelian group. This allows us to construct K(G,n) for n ≥ 2 -/
variables {G : CommGroup} (n : ℕ) variables {G : AbGroup} (n : ℕ)
definition EM1_mul [unfold 2 3] (x x' : EM1' G) : EM1' G := definition EM1_mul [unfold 2 3] (x x' : EM1' G) : EM1' G :=
begin begin
@ -260,7 +260,7 @@ namespace EM
refine freudenthal_pequiv _ this } refine freudenthal_pequiv _ this }
end end
definition loopn_EMadd1_pequiv_EM1 (G : CommGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) := definition loopn_EMadd1_pequiv_EM1 (G : AbGroup) (n : ℕ) : EM1 G ≃* Ω[n] (EMadd1 G n) :=
begin begin
induction n with n e, induction n with n e,
{ reflexivity }, { reflexivity },
@ -270,7 +270,7 @@ namespace EM
end end
-- use loopn_EMadd1_pequiv_EM1 in this definition? -- use loopn_EMadd1_pequiv_EM1 in this definition?
definition loopn_EMadd1 (G : CommGroup) (n : ℕ) : G ≃* Ω[succ n] (EMadd1 G n) := definition loopn_EMadd1 (G : AbGroup) (n : ℕ) : G ≃* Ω[succ n] (EMadd1 G n) :=
begin begin
induction n with n e, induction n with n e,
{ apply loop_EM1 }, { apply loop_EM1 },
@ -279,15 +279,15 @@ namespace EM
exact e } exact e }
end end
definition loopn_EMadd1_succ [unfold_full] (G : CommGroup) (n : ℕ) : loopn_EMadd1 G (succ n) ~* definition loopn_EMadd1_succ [unfold_full] (G : AbGroup) (n : ℕ) : loopn_EMadd1 G (succ n) ~*
!loopn_succ_in⁻¹ᵉ* ∘* apn (succ n) !loop_EMadd1 ∘* loopn_EMadd1 G n := !loopn_succ_in⁻¹ᵉ* ∘* apn (succ n) !loop_EMadd1 ∘* loopn_EMadd1 G n :=
by reflexivity by reflexivity
definition EM_up {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) definition EM_up {G : AbGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G)
: Ω[succ n] (Ω X) ≃* G := : Ω[succ n] (Ω X) ≃* G :=
!loopn_succ_in⁻¹ᵉ* ⬝e* e !loopn_succ_in⁻¹ᵉ* ⬝e* e
definition is_homomorphism_EM_up {G : CommGroup} {X : Type*} {n : ℕ} definition is_homomorphism_EM_up {G : AbGroup} {X : Type*} {n : ℕ}
(e : Ω[succ (succ n)] X ≃* G) (e : Ω[succ (succ n)] X ≃* G)
(r : Π(p q : Ω[succ (succ n)] X), e (p ⬝ q) = e p * e q) (r : Π(p q : Ω[succ (succ n)] X), e (p ⬝ q) = e p * e q)
(p q : Ω[succ n] (Ω X)) : EM_up e (p ⬝ q) = EM_up e p * EM_up e q := (p q : Ω[succ n] (Ω X)) : EM_up e (p ⬝ q) = EM_up e p * EM_up e q :=
@ -295,7 +295,7 @@ namespace EM
refine _ ⬝ !r, apply ap e, esimp, apply apn_con refine _ ⬝ !r, apply ap e, esimp, apply apn_con
end end
definition EMadd1_pmap [unfold 8] {G : CommGroup} {X : Type*} (n : ℕ) definition EMadd1_pmap [unfold 8] {G : AbGroup} {X : Type*} (n : ℕ)
(e : Ω[succ n] X ≃* G) (e : Ω[succ n] X ≃* G)
(r : Πp q, e (p ⬝ q) = e p * e q) (r : Πp q, e (p ⬝ q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X := [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n →* X :=
@ -307,12 +307,12 @@ namespace EM
(psusp.elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)), (psusp.elim (f _ (EM_up e) (is_homomorphism_EM_up e r) _ _)),
end end
definition EMadd1_pmap_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ (succ n)] X ≃* G) definition EMadd1_pmap_succ {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[succ (succ n)] X ≃* G)
r [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : EMadd1_pmap (succ n) e r = r [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : EMadd1_pmap (succ n) e r =
ptrunc.elim ((succ n).+1) (psusp.elim (EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r))) := ptrunc.elim ((succ n).+1) (psusp.elim (EMadd1_pmap n (EM_up e) (is_homomorphism_EM_up e r))) :=
by reflexivity by reflexivity
definition loop_EMadd1_pmap {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G) definition loop_EMadd1_pmap {G : AbGroup} {X : Type*} {n : ℕ} (e : Ω[succ (succ n)] X ≃* G)
(r : Πp q, e (p ⬝ q) = e p * e q) (r : Πp q, e (p ⬝ q) = e p * e q)
[H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] : [H1 : is_conn (succ n) X] [H2 : is_trunc ((succ n).+1) X] :
Ω→(EMadd1_pmap (succ n) e r) ∘* loop_EMadd1 G n ~* Ω→(EMadd1_pmap (succ n) e r) ∘* loop_EMadd1 G n ~*
@ -329,7 +329,7 @@ namespace EM
reflexivity } reflexivity }
end end
definition loopn_EMadd1_pmap' {G : CommGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃* G) definition loopn_EMadd1_pmap' {G : AbGroup} {X : Type*} {n : ℕ} (e : Ω[succ n] X ≃* G)
(r : Πp q, e (p ⬝ q) = e p * e q) (r : Πp q, e (p ⬝ q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] :
Ω→[succ n](EMadd1_pmap n e r) ∘* loopn_EMadd1 G n ~* e⁻¹ᵉ* := Ω→[succ n](EMadd1_pmap n e r) ∘* loopn_EMadd1 G n ~* e⁻¹ᵉ* :=
@ -346,7 +346,7 @@ namespace EM
apply pinv_pcompose_cancel_left apply pinv_pcompose_cancel_left
end end
definition EMadd1_pequiv' {G : CommGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G) definition EMadd1_pequiv' {G : AbGroup} {X : Type*} (n : ℕ) (e : Ω[succ n] X ≃* G)
(r : Π(p q : Ω[succ n] X), e (p ⬝ q) = e p * e q) (r : Π(p q : Ω[succ n] X), e (p ⬝ q) = e p * e q)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
begin begin
@ -365,7 +365,7 @@ namespace EM
do 2 exact trivial_homotopy_group_of_is_trunc _ H} do 2 exact trivial_homotopy_group_of_is_trunc _ H}
end end
definition EMadd1_pequiv {G : CommGroup} {X : Type*} (n : ℕ) (e : πg[n+1] X ≃g G) definition EMadd1_pequiv {G : AbGroup} {X : Type*} (n : ℕ) (e : πg[n+1] X ≃g G)
[H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X := [H1 : is_conn n X] [H2 : is_trunc (n.+1) X] : EMadd1 G n ≃* X :=
begin begin
have is_set (Ω[succ n] X), from !is_set_loopn, have is_set (Ω[succ n] X), from !is_set_loopn,
@ -373,7 +373,7 @@ namespace EM
intro p q, esimp, exact to_respect_mul e (tr p) (tr q) intro p q, esimp, exact to_respect_mul e (tr p) (tr q)
end end
definition EMadd1_pequiv_succ {G : CommGroup} {X : Type*} (n : ℕ) (e : πag[n+2] X ≃g G) definition EMadd1_pequiv_succ {G : AbGroup} {X : Type*} (n : ℕ) (e : πag[n+2] X ≃g G)
[H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd1 G (succ n) ≃* X := [H1 : is_conn (n.+1) X] [H2 : is_trunc (n.+2) X] : EMadd1 G (succ n) ≃* X :=
EMadd1_pequiv (succ n) e EMadd1_pequiv (succ n) e
@ -389,7 +389,7 @@ namespace EM
EMadd1_pequiv_succ n !isomorphism.refl EMadd1_pequiv_succ n !isomorphism.refl
/- K(G, n) -/ /- K(G, n) -/
definition EM (G : CommGroup) : ℕ → Type* definition EM (G : AbGroup) : ℕ → Type*
| 0 := G | 0 := G
| (k+1) := EMadd1 G k | (k+1) := EMadd1 G k
@ -449,7 +449,7 @@ namespace EM
{ reflexivity } { reflexivity }
end end
definition EMadd1_functor [constructor] {G H : CommGroup} (φ : G →g H) (n : ℕ) : definition EMadd1_functor [constructor] {G H : AbGroup} (φ : G →g H) (n : ℕ) :
EMadd1 G n →* EMadd1 H n := EMadd1 G n →* EMadd1 H n :=
begin begin
induction n with n ψ, induction n with n ψ,
@ -457,7 +457,7 @@ namespace EM
{ apply ptrunc_functor, apply psusp_functor, exact ψ } { apply ptrunc_functor, apply psusp_functor, exact ψ }
end end
definition EM_functor [unfold 4] {G H : CommGroup} (φ : G →g H) (n : ℕ) : definition EM_functor [unfold 4] {G H : AbGroup} (φ : G →g H) (n : ℕ) :
K G n →* K H n := K G n →* K H n :=
begin begin
cases n with n, cases n with n,
@ -481,7 +481,7 @@ namespace EM
begin intro X, apply ptruncconntype_eq, esimp, exact EM1_pequiv_type X end begin intro X, apply ptruncconntype_eq, esimp, exact EM1_pequiv_type X end
begin intro G, apply eq_of_isomorphism, apply fundamental_group_EM1 end begin intro G, apply eq_of_isomorphism, apply fundamental_group_EM1 end
/- Equivalence of CommGroups and pointed n-connected (n+1)-truncated types (n ≥ 1) -/ /- Equivalence of AbGroups and pointed n-connected (n+1)-truncated types (n ≥ 1) -/
open trunc_index open trunc_index
definition ptruncconntype_pequiv : Π(n : ℕ) (X Y : (n.+1)-Type*[n]) definition ptruncconntype_pequiv : Π(n : ℕ) (X Y : (n.+1)-Type*[n])
@ -497,16 +497,16 @@ namespace EM
EMadd1 (πag[n+2] X) (succ n) ≃* X := EMadd1 (πag[n+2] X) (succ n) ≃* X :=
EMadd1_pequiv_type X n EMadd1_pequiv_type X n
definition CommGroup_equiv_ptruncconntype' [constructor] (n : ℕ) : definition AbGroup_equiv_ptruncconntype' [constructor] (n : ℕ) :
CommGroup ≃ (n + 1 + 1)-Type*[n+1] := AbGroup ≃ (n + 1 + 1)-Type*[n+1] :=
equiv.MK equiv.MK
(λG, ptruncconntype.mk (EMadd1 G (n+1)) _ pt _) (λG, ptruncconntype.mk (EMadd1 G (n+1)) _ pt _)
(λX, πag[n+2] X) (λX, πag[n+2] X)
begin intro X, apply ptruncconntype_eq, apply EMadd1_pequiv_type end begin intro X, apply ptruncconntype_eq, apply EMadd1_pequiv_type end
begin intro G, apply CommGroup_eq_of_isomorphism, exact ghomotopy_group_EMadd1 G (n+1) end begin intro G, apply AbGroup_eq_of_isomorphism, exact ghomotopy_group_EMadd1 G (n+1) end
definition CommGroup_equiv_ptruncconntype [constructor] (n : ℕ) : definition AbGroup_equiv_ptruncconntype [constructor] (n : ℕ) :
CommGroup ≃ (n.+2)-Type*[n.+1] := AbGroup ≃ (n.+2)-Type*[n.+1] :=
CommGroup_equiv_ptruncconntype' n AbGroup_equiv_ptruncconntype' n
end EM end EM

16
hott/homotopy/LES_of_homotopy_groups.hlean
View file

@ -716,20 +716,20 @@ namespace chain_complex
| (fin.mk 2 H) := begin rexact group_homotopy_group n (pfiber f) end | (fin.mk 2 H) := begin rexact group_homotopy_group n (pfiber f) end
| (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition comm_group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)), definition ab_group_LES_of_homotopy_groups (n : ℕ) : Π(x : fin (succ 2)),
comm_group (LES_of_homotopy_groups (n + 2, x)) ab_group (LES_of_homotopy_groups (n + 2, x))
| (fin.mk 0 H) := proof comm_group_homotopy_group n Y qed | (fin.mk 0 H) := proof ab_group_homotopy_group n Y qed
| (fin.mk 1 H) := proof comm_group_homotopy_group n X qed | (fin.mk 1 H) := proof ab_group_homotopy_group n X qed
| (fin.mk 2 H) := proof comm_group_homotopy_group n (pfiber f) qed | (fin.mk 2 H) := proof ab_group_homotopy_group n (pfiber f) qed
| (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} := definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} :=
Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x)) Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x))
(group_LES_of_homotopy_groups (pr1 x) (pr2 x)) (group_LES_of_homotopy_groups (pr1 x) (pr2 x))
definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : CommGroup.{u} := definition AbGroup_LES_of_homotopy_groups (n : +3ℕ) : AbGroup.{u} :=
CommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n)) AbGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n))
(comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n)) (ab_group_LES_of_homotopy_groups (pr1 n) (pr2 n))
definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ), definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ),
Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k Group_LES_of_homotopy_groups (S k) →g Group_LES_of_homotopy_groups k

4
hott/homotopy/freudenthal.hlean
View file

@ -110,7 +110,7 @@ namespace freudenthal section
apply trunc_pathover, apply trunc_pathover,
apply eq_pathover_constant_left_id_right, apply eq_pathover_constant_left_id_right,
apply square_of_eq, apply square_of_eq,
exact whisker_right !con.right_inv (merid a) exact whisker_right (merid a) !con.right_inv
end end
definition decode_coh_g (a' : A) : tr (up a') =[merid pt] decode_south (code_merid pt (tr a')) := definition decode_coh_g (a' : A) : tr (up a') =[merid pt] decode_south (code_merid pt (tr a')) :=
@ -122,7 +122,7 @@ namespace freudenthal section
end end
definition decode_coh_lem {A : Type} {a a' : A} (p : a = a') definition decode_coh_lem {A : Type} {a a' : A} (p : a = a')
: whisker_right (con.right_inv p) p = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ := : whisker_right p (con.right_inv p) = inv_con_cancel_right p p ⬝ (idp_con p)⁻¹ :=
by induction p; reflexivity by induction p; reflexivity
theorem decode_coh (a : A) : decode_north =[merid a] decode_south := theorem decode_coh (a : A) : decode_north =[merid a] decode_south :=

2
hott/homotopy/homotopy_group.hlean
View file

@ -63,7 +63,7 @@ namespace is_trunc
end end
/- Corollaries of the LES of homotopy groups -/ /- Corollaries of the LES of homotopy groups -/
local attribute comm_group.to_group [coercion] local attribute ab_group.to_group [coercion]
local attribute is_equiv_tinverse [instance] local attribute is_equiv_tinverse [instance]
open prod chain_complex group fin equiv function is_equiv lift open prod chain_complex group fin equiv function is_equiv lift

8
hott/homotopy/smash.hlean
View file

@ -50,7 +50,7 @@ namespace smash
gluel' a pt ⬝ gluer' pt b gluel' a pt ⬝ gluer' pt b
definition glue_pt_left (b : B) : glue (Point A) b = gluer' pt b := definition glue_pt_left (b : B) : glue (Point A) b = gluer' pt b :=
whisker_right !con.right_inv _ ⬝ !idp_con whisker_right _ !con.right_inv ⬝ !idp_con
definition glue_pt_right (a : A) : glue a (Point B) = gluel' a pt := definition glue_pt_right (a : A) : glue a (Point B) = gluel' a pt :=
proof whisker_left _ !con.right_inv qed proof whisker_left _ !con.right_inv qed
@ -82,11 +82,11 @@ namespace smash
{ exact gluel pt ▸ Pmk pt pt }, { exact gluel pt ▸ Pmk pt pt },
{ exact gluer pt ▸ Pmk pt pt }, { exact gluer pt ▸ Pmk pt pt },
{ refine change_path _ (Pg a pt ⬝o !pathover_tr), { refine change_path _ (Pg a pt ⬝o !pathover_tr),
refine whisker_right !glue_pt_right _ ⬝ _, esimp, refine !con.assoc ⬝ _, refine whisker_right _ !glue_pt_right ⬝ _, esimp, refine !con.assoc ⬝ _,
apply whisker_left, apply con.left_inv }, apply whisker_left, apply con.left_inv },
{ refine change_path _ ((Pg pt b)⁻¹ᵒ ⬝o !pathover_tr), { refine change_path _ ((Pg pt b)⁻¹ᵒ ⬝o !pathover_tr),
refine whisker_right !glue_pt_left⁻² _ ⬝ _, refine whisker_right _ !glue_pt_left⁻² ⬝ _,
refine whisker_right !inv_con_inv_right _ ⬝ _, refine !con.assoc ⬝ _, refine whisker_right _ !inv_con_inv_right ⬝ _, refine !con.assoc ⬝ _,
apply whisker_left, apply con.left_inv } apply whisker_left, apply con.left_inv }
end end

4
hott/init/equiv.hlean
View file

@ -174,12 +174,12 @@ namespace is_equiv
(left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y
definition ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q := definition ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q :=
!ap_con ⬝ whisker_right !ap_con _ !ap_con ⬝ whisker_right _ !ap_con
⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹) ⬝ ((!ap_inv ⬝ inverse2 (adj f _)⁻¹)
◾ (inverse (ap_compose f f⁻¹ _)) ◾ (inverse (ap_compose f f⁻¹ _))
◾ (adj f _)⁻¹) ◾ (adj f _)⁻¹)
⬝ con_ap_con_eq_con_con (right_inv f) _ _ ⬝ con_ap_con_eq_con_con (right_inv f) _ _
⬝ whisker_right !con.left_inv _ ⬝ whisker_right _ !con.left_inv
⬝ !idp_con ⬝ !idp_con
definition eq_of_fn_eq_fn'_ap {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q := definition eq_of_fn_eq_fn'_ap {x y : A} (q : x = y) : eq_of_fn_eq_fn' f (ap f q) = q :=

20
hott/init/path.hlean
View file

@ -631,7 +631,7 @@ namespace eq
definition whisker_left [unfold 8] (p : x = y) {q r : y = z} (h : q = r) : p ⬝ q = p ⬝ r := definition whisker_left [unfold 8] (p : x = y) {q r : y = z} (h : q = r) : p ⬝ q = p ⬝ r :=
idp ◾ h idp ◾ h
definition whisker_right [unfold 7] {p q : x = y} (h : p = q) (r : y = z) : p ⬝ r = q ⬝ r := definition whisker_right [unfold 7] {p q : x = y} (r : y = z) (h : p = q) : p ⬝ r = q ⬝ r :=
h ◾ idp h ◾ idp
-- Unwhiskering, a.k.a. cancelling -- Unwhiskering, a.k.a. cancelling
@ -640,16 +640,16 @@ namespace eq
λs, !inv_con_cancel_left⁻¹ ⬝ whisker_left p⁻¹ s ⬝ !inv_con_cancel_left λs, !inv_con_cancel_left⁻¹ ⬝ whisker_left p⁻¹ s ⬝ !inv_con_cancel_left
definition cancel_right {x y z : A} {p q : x = y} (r : y = z) : (p ⬝ r = q ⬝ r) → (p = q) := definition cancel_right {x y z : A} {p q : x = y} (r : y = z) : (p ⬝ r = q ⬝ r) → (p = q) :=
λs, !con_inv_cancel_right⁻¹ ⬝ whisker_right s r⁻¹ ⬝ !con_inv_cancel_right λs, !con_inv_cancel_right⁻¹ ⬝ whisker_right r⁻¹ s ⬝ !con_inv_cancel_right
-- Whiskering and identity paths. -- Whiskering and identity paths.
definition whisker_right_idp {p q : x = y} (h : p = q) : definition whisker_right_idp {p q : x = y} (h : p = q) :
whisker_right h idp = h := whisker_right idp h = h :=
by induction h; induction p; reflexivity by induction h; induction p; reflexivity
definition whisker_right_idp_left [unfold_full] (p : x = y) (q : y = z) : definition whisker_right_idp_left [unfold_full] (p : x = y) (q : y = z) :
whisker_right idp q = idp :> (p ⬝ q = p ⬝ q) := whisker_right q idp = idp :> (p ⬝ q = p ⬝ q) :=
idp idp
definition whisker_left_idp_right [unfold_full] (p : x = y) (q : y = z) : definition whisker_left_idp_right [unfold_full] (p : x = y) (q : y = z) :
@ -668,7 +668,7 @@ namespace eq
end end
definition con2_idp [unfold_full] {p q : x = y} (h : p = q) : definition con2_idp [unfold_full] {p q : x = y} (h : p = q) :
h ◾ idp = whisker_right h idp :> (p ⬝ idp = q ⬝ idp) := h ◾ idp = whisker_right idp h :> (p ⬝ idp = q ⬝ idp) :=
idp idp
definition idp_con2 [unfold_full] {p q : x = y} (h : p = q) : definition idp_con2 [unfold_full] {p q : x = y} (h : p = q) :
@ -686,16 +686,16 @@ namespace eq
by induction d; induction c; induction b;induction a; reflexivity by induction d; induction c; induction b;induction a; reflexivity
definition con2_eq_rl {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z} definition con2_eq_rl {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z}
(a : p = p') (b : q = q') : a ◾ b = whisker_right a q ⬝ whisker_left p' b := (a : p = p') (b : q = q') : a ◾ b = whisker_right q a ⬝ whisker_left p' b :=
by induction b; induction a; reflexivity by induction b; induction a; reflexivity
definition con2_eq_lf {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z} definition con2_eq_lf {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z}
(a : p = p') (b : q = q') : a ◾ b = whisker_left p b ⬝ whisker_right a q' := (a : p = p') (b : q = q') : a ◾ b = whisker_left p b ⬝ whisker_right q' a :=
by induction b; induction a; reflexivity by induction b; induction a; reflexivity
definition whisker_right_con_whisker_left {x y z : A} {p p' : x = y} {q q' : y = z} definition whisker_right_con_whisker_left {x y z : A} {p p' : x = y} {q q' : y = z}
(a : p = p') (b : q = q') : (a : p = p') (b : q = q') :
(whisker_right a q) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right a q') := (whisker_right q a) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right q' a) :=
by induction b; induction a; reflexivity by induction b; induction a; reflexivity
-- Structure corresponding to the coherence equations of a bicategory. -- Structure corresponding to the coherence equations of a bicategory.
@ -704,13 +704,13 @@ namespace eq
definition pentagon {v w x y z : A} (p : v = w) (q : w = x) (r : x = y) (s : y = z) : definition pentagon {v w x y z : A} (p : v = w) (q : w = x) (r : x = y) (s : y = z) :
whisker_left p (con.assoc' q r s) whisker_left p (con.assoc' q r s)
⬝ con.assoc' p (q ⬝ r) s ⬝ con.assoc' p (q ⬝ r) s
⬝ whisker_right (con.assoc' p q r) s ⬝ whisker_right s (con.assoc' p q r)
= con.assoc' p q (r ⬝ s) ⬝ con.assoc' (p ⬝ q) r s := = con.assoc' p q (r ⬝ s) ⬝ con.assoc' (p ⬝ q) r s :=
by induction s;induction r;induction q;induction p;reflexivity by induction s;induction r;induction q;induction p;reflexivity
-- The 3-cell witnessing the left unit triangle. -- The 3-cell witnessing the left unit triangle.
definition triangulator (p : x = y) (q : y = z) : definition triangulator (p : x = y) (q : y = z) :
con.assoc' p idp q ⬝ whisker_right (con_idp p) q = whisker_left p (idp_con q) := con.assoc' p idp q ⬝ whisker_right q (con_idp p) = whisker_left p (idp_con q) :=
by induction q; induction p; reflexivity by induction q; induction p; reflexivity
definition eckmann_hilton (p q : idp = idp :> a = a) : p ⬝ q = q ⬝ p := definition eckmann_hilton (p q : idp = idp :> a = a) : p ⬝ q = q ⬝ p :=

2
hott/types/arrow_2.hlean
View file

@ -158,7 +158,7 @@ namespace arrow
(p (f⁻¹ b))⁻¹], (p (f⁻¹ b))⁻¹],
apply eq_of_square, apply eq_of_square,
refine vconcat_eq _ refine vconcat_eq _
(whisker_right (ap_inv β (right_inv f b)) (p (f⁻¹ b))⁻¹)⁻¹, (whisker_right (p (f⁻¹ b))⁻¹ (ap_inv β (right_inv f b)))⁻¹,
refine vconcat_eq _ refine vconcat_eq _
(con_inv (p (f⁻¹ b)) (ap β (right_inv f b))), (con_inv (p (f⁻¹ b)) (ap β (right_inv f b))),
refine vconcat_eq _ refine vconcat_eq _

10
hott/types/eq.hlean
View file

@ -28,7 +28,7 @@ namespace eq
end end
theorem whisker_right_con_right (q : a₂ = a₃) (r : p = p') (s : p' = p'') theorem whisker_right_con_right (q : a₂ = a₃) (r : p = p') (s : p' = p'')
: whisker_right (r ⬝ s) q = whisker_right r q ⬝ whisker_right s q := : whisker_right q (r ⬝ s) = whisker_right q r ⬝ whisker_right q s :=
begin begin
induction q, induction r, induction s, reflexivity induction q, induction r, induction s, reflexivity
end end
@ -40,7 +40,7 @@ namespace eq
end end
theorem whisker_right_con_left {p p' : a₁ = a₂} (q : a₂ = a₃) (q' : a₃ = a₄) (r : p = p') theorem whisker_right_con_left {p p' : a₁ = a₂} (q : a₂ = a₃) (q' : a₃ = a₄) (r : p = p')
: whisker_right r (q ⬝ q') = !con.assoc' ⬝ whisker_right (whisker_right r q) q' ⬝ !con.assoc := : whisker_right (q ⬝ q') r = !con.assoc' ⬝ whisker_right q' (whisker_right q r) ⬝ !con.assoc :=
begin begin
induction q', induction q, induction r, induction p, reflexivity induction q', induction q, induction r, induction p, reflexivity
end end
@ -56,7 +56,7 @@ namespace eq
by induction r; reflexivity by induction r; reflexivity
theorem whisker_right_inv {p p' : a₁ = a₂} (q : a₂ = a₃) (r : p = p') theorem whisker_right_inv {p p' : a₁ = a₂} (q : a₂ = a₃) (r : p = p')
: whisker_right r⁻¹ q = (whisker_right r q)⁻¹ := : whisker_right q r⁻¹ = (whisker_right q r)⁻¹ :=
by induction r; reflexivity by induction r; reflexivity
theorem ap_eq_apd10 {B : A → Type} {f g : Πa, B a} (p : f = g) (a : A) : theorem ap_eq_apd10 {B : A → Type} {f g : Πa, B a} (p : f = g) (a : A) :
@ -75,7 +75,7 @@ namespace eq
by induction p;reflexivity by induction p;reflexivity
theorem ap_con_left_inv (f : A → B) (p : a₁ = a₂) theorem ap_con_left_inv (f : A → B) (p : a₁ = a₂)
: ap_con f p⁻¹ p ⬝ whisker_right (ap_inv f p) _ ⬝ con.left_inv (ap f p) : ap_con f p⁻¹ p ⬝ whisker_right _ (ap_inv f p) ⬝ con.left_inv (ap f p)
= ap (ap f) (con.left_inv p) := = ap (ap f) (con.left_inv p) :=
by induction p;reflexivity by induction p;reflexivity
@ -282,7 +282,7 @@ namespace eq
equiv.mk _ !is_equiv_whisker_left equiv.mk _ !is_equiv_whisker_left
definition is_equiv_whisker_right [constructor] {p q : a₁ = a₂} (r : a₂ = a₃) definition is_equiv_whisker_right [constructor] {p q : a₁ = a₂} (r : a₂ = a₃)
: is_equiv (λs, whisker_right s r : p = q → p ⬝ r = q ⬝ r) := : is_equiv (λs, whisker_right r s : p = q → p ⬝ r = q ⬝ r) :=
begin begin
fapply adjointify, fapply adjointify,
{intro s, apply (!cancel_right s)}, {intro s, apply (!cancel_right s)},

6
hott/types/equiv.hlean
View file

@ -164,10 +164,10 @@ namespace is_equiv
intro q, apply eq_of_homotopy, intro c, intro q, apply eq_of_homotopy, intro c,
unfold inv_homotopy_of_homotopy_post, unfold inv_homotopy_of_homotopy_post,
unfold homotopy_of_inv_homotopy_post, unfold homotopy_of_inv_homotopy_post,
apply trans (whisker_right apply trans (whisker_right (left_inv f (α c))
(ap_con f⁻¹ (right_inv f (β c))⁻¹ (ap f (q c)) (ap_con f⁻¹ (right_inv f (β c))⁻¹ (ap f (q c))
⬝ whisker_right (ap_inv f⁻¹ (right_inv f (β c))) ⬝ whisker_right (ap f⁻¹ (ap f (q c)))
(ap f⁻¹ (ap f (q c)))) (left_inv f (α c))), (ap_inv f⁻¹ (right_inv f (β c))))),
apply inverse, apply eq_bot_of_square, apply inverse, apply eq_bot_of_square,
apply eq_hconcat (adj_inv f (β c))⁻¹, apply eq_hconcat (adj_inv f (β c))⁻¹,
apply eq_vconcat (ap_compose f⁻¹ f (q c))⁻¹, apply eq_vconcat (ap_compose f⁻¹ f (q c))⁻¹,

8
hott/types/fin.hlean
View file

@ -299,11 +299,11 @@ lemma madd_left_inv : Π i : fin (succ n), madd (minv i) i = fin.zero n
| (mk iv ilt) := eq_of_veq (by | (mk iv ilt) := eq_of_veq (by
rewrite [val_madd, ↑minv, mod_add_mod, nat.sub_add_cancel (le_of_lt ilt), mod_self]) rewrite [val_madd, ↑minv, mod_add_mod, nat.sub_add_cancel (le_of_lt ilt), mod_self])
definition madd_is_comm_group [instance] : add_comm_group (fin (succ n)) := definition madd_is_ab_group [instance] : add_ab_group (fin (succ n)) :=
comm_group.mk madd _ madd_assoc (fin.zero n) zero_madd madd_zero minv madd_left_inv madd_comm ab_group.mk madd _ madd_assoc (fin.zero n) zero_madd madd_zero minv madd_left_inv madd_comm
definition gfin (n : ℕ) [H : is_succ n] : AddCommGroup.{0} := definition gfin (n : ℕ) [H : is_succ n] : AddAbGroup.{0} :=
by induction H with n; exact AddCommGroup.mk (fin (succ n)) _ by induction H with n; exact AddAbGroup.mk (fin (succ n)) _
end madd end madd

6
hott/types/int/hott.hlean
View file

@ -24,10 +24,10 @@ namespace int
notation `gℤ` := group_integers notation `gℤ` := group_integers
definition CommGroup_int [reducible] [constructor] : AddCommGroup := definition AbGroup_int [reducible] [constructor] : AddAbGroup :=
AddCommGroup.mk ℤ _ AddAbGroup.mk ℤ _
notation `agℤ` := CommGroup_int notation `agℤ` := AbGroup_int
end end
definition is_equiv_succ [constructor] [instance] : is_equiv succ := definition is_equiv_succ [constructor] [instance] : is_equiv succ :=

4
hott/types/pointed.hlean
View file

@ -383,7 +383,7 @@ namespace pointed
(respect_pt g)) (respect_pt g))
... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), respect_pt f = ap10 p pt ⬝ respect_pt g ... ≃ Σ(p : pmap.to_fun f = pmap.to_fun g), respect_pt f = ap10 p pt ⬝ respect_pt g
: sigma_equiv_sigma_right : sigma_equiv_sigma_right
(λp, equiv_eq_closed_right _ (whisker_right (ap_eq_apd10 p _) _)) (λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _)))
... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), respect_pt f = p pt ⬝ respect_pt g ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), respect_pt f = p pt ⬝ respect_pt g
: sigma_equiv_sigma_left' eq_equiv_homotopy : sigma_equiv_sigma_left' eq_equiv_homotopy
... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), p pt ⬝ respect_pt g = respect_pt f ... ≃ Σ(p : pmap.to_fun f ~ pmap.to_fun g), p pt ⬝ respect_pt g = respect_pt f
@ -448,7 +448,7 @@ namespace pointed
begin begin
fconstructor, fconstructor,
{ intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left, { intro p, esimp, refine !con.assoc ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
refine whisker_right !ap_inv _ ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left, refine whisker_right _ !ap_inv ⬝ _ ⬝ !con_inv⁻¹, apply whisker_left,
exact !inv_inv⁻¹}, exact !inv_inv⁻¹},
{ induction B with B b, induction f with f pf, esimp at *, induction pf, reflexivity}, { induction B with B b, induction f with f pf, esimp at *, induction pf, reflexivity},
end end

6
hott/types/trunc.hlean
View file

@ -764,8 +764,8 @@ namespace trunc
begin begin
fapply phomotopy.mk, fapply phomotopy.mk,
{ apply trunc_functor_compose}, { apply trunc_functor_compose},
{ esimp, refine !idp_con ⬝ _, refine whisker_right !ap_compose'⁻¹ᵖ _ ⬝ _, { esimp, refine !idp_con ⬝ _, refine whisker_right _ !ap_compose'⁻¹ᵖ ⬝ _,
esimp, refine whisker_right (ap_compose' tr g _) _ ⬝ _, exact !ap_con⁻¹}, esimp, refine whisker_right _ (ap_compose' tr g _) ⬝ _, exact !ap_con⁻¹},
end end
definition ptrunc_functor_pid [constructor] (X : Type*) (n : ℕ₋₂) : definition ptrunc_functor_pid [constructor] (X : Type*) (n : ℕ₋₂) :
@ -851,7 +851,7 @@ namespace trunc
begin begin
fapply phomotopy.mk, fapply phomotopy.mk,
{ intro x, induction x with a, reflexivity }, { intro x, induction x with a, reflexivity },
{ esimp, exact !idp_con ⬝ whisker_right !ap_compose _ }, { esimp, exact !idp_con ⬝ whisker_right _ !ap_compose },
end end
end trunc open trunc end trunc open trunc

4
tests/lean/hott/614.hlean
View file

@ -8,7 +8,7 @@ protected definition my_decode {x : circle} (c : circle.code x) : base = x :=
begin begin
induction x, induction x,
{ revert c, exact power loop }, { revert c, exact power loop },
{ apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r, { apply arrow_pathover_left, intro b, apply concato_eq, apply eq_pathover_r,
rewrite [power_con,transport_code_loop]}, rewrite [power_con,transport_code_loop]},
end end
@ -16,6 +16,6 @@ protected definition my_decode' {x : circle} : circle.code x → base = x :=
begin begin
induction x, induction x,
{ exact power loop}, { exact power loop},
{ apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r, { apply arrow_pathover_left, intro b, apply concato_eq, apply eq_pathover_r,
rewrite [power_con,transport_code_loop]}, rewrite [power_con,transport_code_loop]},
end end

2
tests/lean/hott/615.hlean
View file

@ -15,6 +15,6 @@ protected definition my_decode {x : circle} : my_code x → base = x :=
begin begin
induction x, induction x,
{ exact power loop}, { exact power loop},
{ apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r, { apply arrow_pathover_left, intro b, apply concato_eq, apply eq_pathover_r,
xrewrite [power_con, transport_code_loop]}, xrewrite [power_con, transport_code_loop]},
end end

2
tests/lean/hott/beginend2.hlean
View file

@ -2,7 +2,7 @@ open eq tactic
open eq (rec_on) open eq (rec_on)
definition concat_whisker2 {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') : definition concat_whisker2 {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') :
(whisker_right a q) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right a q') := (whisker_right q a) ⬝ (whisker_left p' b) = (whisker_left p b) ⬝ (whisker_right q' a) :=
begin begin
apply (rec_on b), apply (rec_on b),
apply (rec_on a), apply (rec_on a),

4
tests/lean/hott/rewriter1.hlean
View file

@ -3,7 +3,7 @@ open algebra
constant f {A : Type} : A → A → A constant f {A : Type} : A → A → A
theorem test1 {A : Type} [s : add_comm_group A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) := theorem test1 {A : Type} [s : add_ab_group A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) :=
begin begin
rewrite [ rewrite [
add_zero at {1, 3}, -- rewrite 1st and 3rd occurrences add_zero at {1, 3}, -- rewrite 1st and 3rd occurrences
@ -12,7 +12,7 @@ end
axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_one A] (a : A) : f (a * 1) (a * 1) = 1 axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_one A] (a : A) : f (a * 1) (a * 1) = 1
theorem test2 {A : Type} [s : comm_group A] (a b c : A) : f a a = 1 := theorem test2 {A : Type} [s : ab_group A] (a b c : A) : f a a = 1 :=
begin begin
rewrite [-(mul_one a), -- - means apply symmetry, rewrite 0 ==> a * 0 at 1st and 2nd occurrences rewrite [-(mul_one a), -- - means apply symmetry, rewrite 0 ==> a * 0 at 1st and 2nd occurrences
Ax] -- use Ax as rewrite rule Ax] -- use Ax as rewrite rule

2
tests/lean/hott/rw_binders.hlean
View file

@ -5,5 +5,5 @@ variables {A : Type} {a1 a2 a3 : A}
definition my_transport_eq_l (p : a1 = a2) (q : a1 = a3) definition my_transport_eq_l (p : a1 = a2) (q : a1 = a3)
: transport (λx, x = a3) p q = p⁻¹ ⬝ q := : transport (λx, x = a3) p q = p⁻¹ ⬝ q :=
begin begin
rewrite transport_eq_l, rewrite eq_transport_l,
end end