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

chore(hott/algebra) complete the sigma characterization

Browse source
This commit is contained in:
Jakob von Raumer 2014-12-31 23:07:29 -05:00 committed by Leonardo de Moura
parent 4af0a911b3
commit 428a2b6f58
1 changed files with 23 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
hott/algebra/precategory/natural_transformation.hlean
View file

@ -47,6 +47,7 @@ namespace natural_transformation
apply (dcongr_arg2 (@natural_transformation.mk C D F G) p₁ p₂), apply (dcongr_arg2 (@natural_transformation.mk C D F G) p₁ p₂),
end end
protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) : protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) :
η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ := η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
begin begin
@ -92,28 +93,34 @@ namespace natural_transformation
apply (@is_hset.elim), apply !homH, apply (@is_hset.elim), apply !homH,
end end
protected definition sigma_char : --set_option pp.implicit true
(Σ (η : Π (a : C), hom (F a) (G a)), Π (a b : C) (f : hom a b), G f ∘ η a = η b ∘ F f) ≃ (F ⟹ G) := protected definition sigma_char (F G : C ⇒ D) :
/-begin (Σ (η : Π (a : C), hom (F a) (G a)), Π (a b : C) (f : hom a b), G f ∘ η a = η b ∘ F f) ≃ (F ⟹ G) :=
intro what, begin
fapply equiv.mk, fapply equiv.mk,
intro S, apply natural_transformation.mk, exact (S.2), intro S, apply natural_transformation.mk, exact (S.2),
fapply adjointify, fapply adjointify,
intro H, apply (natural_transformation.rec_on H), intros (η, natu), intro H,
exact (sigma.mk η @natu), fapply sigma.mk,
intro H, apply (natural_transformation.rec_on _ _ _), intro a, exact (H a),
intro S2, intros (a, b, f), exact (naturality H f),
end-/ intro H, apply (natural_transformation.rec_on H),
/-(λ x, equiv.mk (λ S, natural_transformation.mk S.1 S.2) intros (eta, nat), unfold function.id,
(adjointify (λ S, natural_transformation.mk S.1 S.2) fapply natural_transformation.congr,
(λ H, natural_transformation.rec_on H (λ η nat, sigma.mk η nat)) apply idp,
(λ H, natural_transformation.rec_on H (λ η nat, refl (natural_transformation.mk η nat))) repeat ( apply funext.path_pi ; intro a ),
(λ S, sigma.rec_on S (λ η nat, refl (sigma.mk η nat)))))-/ apply (@is_hset.elim), apply !homH,
sorry intro S,
fapply sigma.path,
apply funext.path_pi, intro a,
apply idp,
repeat ( apply funext.path_pi ; intro a ),
apply (@is_hset.elim), apply !homH,
end
protected definition to_hset : is_hset (F ⟹ G) := protected definition to_hset : is_hset (F ⟹ G) :=
begin begin
apply trunc_equiv, apply (equiv.to_is_equiv sigma_char), apply trunc_equiv, apply (equiv.to_is_equiv !sigma_char),
apply trunc_sigma, apply trunc_sigma,
apply trunc_pi, intro a, exact (@homH (objects D) _ (F a) (G a)), apply trunc_pi, intro a, exact (@homH (objects D) _ (F a) (G a)),
intro η, apply trunc_pi, intro a, intro η, apply trunc_pi, intro a,