refactor(library/algebra/category/constructions): more rewrite tactic tests
This commit is contained in:
Leonardo de Moura
parent
adae95cf68
commit
14aeac180a
4 changed files with 29 additions and 27 deletions
|
|
@ -25,11 +25,11 @@ namespace nat_trans
|
||||||
(λ a, η a ∘ θ a)
|
(λ a, η a ∘ θ a)
|
||||||
(λ a b f,
|
(λ a b f,
|
||||||
calc
|
calc
|
||||||
H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc
|
H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : by rewrite assoc
|
||||||
... = (η b ∘ G f) ∘ θ a : naturality η f
|
... = (η b ∘ G f) ∘ θ a : by rewrite naturality
|
||||||
... = η b ∘ (G f ∘ θ a) : assoc
|
... = η b ∘ (G f ∘ θ a) : by rewrite assoc
|
||||||
... = η b ∘ (θ b ∘ F f) : naturality θ f
|
... = η b ∘ (θ b ∘ F f) : by rewrite naturality
|
||||||
... = (η b ∘ θ b) ∘ F f : assoc)
|
... = (η b ∘ θ b) ∘ F f : by rewrite assoc)
|
||||||
|
|
||||||
infixr `∘n`:60 := compose
|
infixr `∘n`:60 := compose
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -23,13 +23,13 @@ namespace is_equiv
|
||||||
is_contr.mk
|
is_contr.mk
|
||||||
(fiber.mk (f⁻¹ b) (retr f b))
|
(fiber.mk (f⁻¹ b) (retr f b))
|
||||||
(λz, fiber.rec_on z (λa p, fiber.eq_mk ((ap f⁻¹ p)⁻¹ ⬝ sect f a) (calc
|
(λz, fiber.rec_on z (λa p, fiber.eq_mk ((ap f⁻¹ p)⁻¹ ⬝ sect f a) (calc
|
||||||
retr f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ retr f b) : inv_con_cancel_left
|
retr f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ retr f b) : by rewrite inv_con_cancel_left
|
||||||
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (retr f (f a) ⬝ p) : by rewrite ap_con_eq_con
|
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (retr f (f a) ⬝ p) : by rewrite ap_con_eq_con
|
||||||
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (sect f a) ⬝ p) : by rewrite adj
|
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (sect f a) ⬝ p) : by rewrite adj
|
||||||
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (sect f a) ⬝ p : con.assoc
|
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite con.assoc
|
||||||
... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite ap_compose
|
... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite ap_compose
|
||||||
... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite ap_inv
|
... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (sect f a) ⬝ p : by rewrite ap_inv
|
||||||
... = ap f ((ap f⁻¹ p)⁻¹ ⬝ sect f a) ⬝ p : by rewrite ap_con)))
|
... = ap f ((ap f⁻¹ p)⁻¹ ⬝ sect f a) ⬝ p : by rewrite ap_con)))
|
||||||
|
|
||||||
definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ∼ id) :=
|
definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ∼ id) :=
|
||||||
begin
|
begin
|
||||||
|
|
|
||||||
|
|
@ -312,8 +312,8 @@ namespace sigma
|
||||||
|
|
||||||
definition comm_equiv_nondep (A B : Type) : (Σ(a : A), B) ≃ Σ(b : B), A :=
|
definition comm_equiv_nondep (A B : Type) : (Σ(a : A), B) ≃ Σ(b : B), A :=
|
||||||
calc
|
calc
|
||||||
(Σ(a : A), B) ≃ A × B : equiv_prod
|
(Σ(a : A), B) ≃ A × B : equiv_prod
|
||||||
... ≃ B × A : prod_comm_equiv
|
... ≃ B × A : prod_comm_equiv
|
||||||
... ≃ Σ(b : B), A : equiv_prod
|
... ≃ Σ(b : B), A : equiv_prod
|
||||||
|
|
||||||
/- ** Universal mapping properties -/
|
/- ** Universal mapping properties -/
|
||||||
|
|
|
||||||
|
|
@ -238,13 +238,15 @@ namespace category
|
||||||
|
|
||||||
definition postcomposition_functor {x y : D} (h : x ⟶ y)
|
definition postcomposition_functor {x y : D} (h : x ⟶ y)
|
||||||
: Slice_category D x ⇒ Slice_category D y :=
|
: Slice_category D x ⇒ Slice_category D y :=
|
||||||
functor.mk (λ a, sigma.mk (to_ob a) (h ∘ ob_hom a))
|
functor.mk
|
||||||
(λ a b f, sigma.mk (hom_hom f)
|
(λ a, sigma.mk (to_ob a) (h ∘ ob_hom a))
|
||||||
(calc
|
(λ a b f,
|
||||||
(h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : (assoc h (ob_hom b) (hom_hom f))⁻¹
|
⟨hom_hom f,
|
||||||
... = h ∘ ob_hom a : congr_arg (λx, h ∘ x) (commute f)))
|
calc
|
||||||
(λ a, rfl)
|
(h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : by rewrite assoc
|
||||||
(λ a b c g f, dpair_eq rfl !proof_irrel)
|
... = h ∘ ob_hom a : by rewrite commute⟩)
|
||||||
|
(λ a, rfl)
|
||||||
|
(λ a b c g f, dpair_eq rfl !proof_irrel)
|
||||||
|
|
||||||
-- -- in the following comment I tried to have (A = B) in the type of a == b, but that doesn't solve the problems
|
-- -- in the following comment I tried to have (A = B) in the type of a == b, but that doesn't solve the problems
|
||||||
-- definition heq2 {A B : Type} (H : A = B) (a : A) (b : B) := a == b
|
-- definition heq2 {A B : Type} (H : A = B) (a : A) (b : B) := a == b
|
||||||
|
|
@ -347,15 +349,15 @@ namespace category
|
||||||
(show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a,
|
(show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a,
|
||||||
proof
|
proof
|
||||||
calc
|
calc
|
||||||
to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : !assoc
|
to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : by rewrite assoc
|
||||||
... = (hom_dst g ∘ to_hom b) ∘ hom_src f : {commute g}
|
... = (hom_dst g ∘ to_hom b) ∘ hom_src f : by rewrite commute
|
||||||
... = hom_dst g ∘ (to_hom b ∘ hom_src f) : symm !assoc
|
... = hom_dst g ∘ (to_hom b ∘ hom_src f) : by rewrite assoc
|
||||||
... = hom_dst g ∘ (hom_dst f ∘ to_hom a) : {commute f}
|
... = hom_dst g ∘ (hom_dst f ∘ to_hom a) : by rewrite commute
|
||||||
... = (hom_dst g ∘ hom_dst f) ∘ to_hom a : !assoc
|
... = (hom_dst g ∘ hom_dst f) ∘ to_hom a : by rewrite assoc
|
||||||
qed)
|
qed)
|
||||||
))
|
))
|
||||||
(λ a, sigma.mk id (sigma.mk id (!id_right ⬝ (symm !id_left))))
|
(λ a, sigma.mk id (sigma.mk id (!id_right ⬝ (symm !id_left))))
|
||||||
(λ a b c d h g f, ndtrip_eq !assoc !assoc !proof_irrel)
|
(λ a b c d h g f, ndtrip_eq !assoc !assoc !proof_irrel)
|
||||||
(λ a b f, ndtrip_equal !id_left !id_left !proof_irrel)
|
(λ a b f, ndtrip_equal !id_left !id_left !proof_irrel)
|
||||||
(λ a b f, ndtrip_equal !id_right !id_right !proof_irrel)
|
(λ a b f, ndtrip_equal !id_right !id_right !proof_irrel)
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue