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

chore(hott/algebra) modify the proof that taking the dual category is involutive

Browse source
This commit is contained in:
Jakob von Raumer 2014-12-31 23:21:33 -05:00 committed by Leonardo de Moura
parent 428a2b6f58
commit 0915da6625
1 changed files with 5 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
hott/algebra/precategory/constructions.hlean
View file

@ -34,27 +34,14 @@ namespace precategory
-- take the trick they use in Coq-HoTT, and introduce a further -- take the trick they use in Coq-HoTT, and introduce a further
-- axiom in the definition of precategories that provides thee -- axiom in the definition of precategories that provides thee
-- symmetric associativity proof. -- symmetric associativity proof.
universe variables l k definition op_op' {ob : Type} (C : precategory ob) : opposite (opposite C) = C :=
definition op_op' {ob : Type} (C : precategory.{l k} ob) : opposite (opposite C) = C := begin
sorry
/-begin
apply (rec_on C), intros (hom', homH', comp', ID', assoc', id_left', id_right'), apply (rec_on C), intros (hom', homH', comp', ID', assoc', id_left', id_right'),
apply (ap (λassoc'', precategory.mk hom' @homH' comp' ID' assoc'' id_left' id_right')), apply (ap (λassoc'', precategory.mk hom' @homH' comp' ID' assoc'' id_left' id_right')),
apply (@funext.path_pi _ _ _ _ assoc'), intro a, repeat ( apply funext.path_pi ; intros ),
apply (@funext.path_pi _ _ _ _ (@assoc' a)), intro b,
apply (@funext.path_pi _ _ _ _ (@assoc' a b)), intro c,
apply (@funext.path_pi _ _ _ _ (@assoc' a b c)), intro d,
apply (@funext.path_pi _ _ _ _ (@assoc' a b c d)), intro f,
apply (@funext.path_pi _ _ _ _ (@assoc' a b c d f)), intro g,
apply (@funext.path_pi _ _ _ _ (@assoc' a b c d f g)), intro h,
apply ap, apply ap,
show @assoc ob (@opposite ob (@precategory.mk ob hom' @homH' comp' ID' assoc' id_left' id_right')) d c b a h apply (@is_hset.elim), apply !homH',
g end
f ⁻¹ = @assoc' a b c d f g h,
begin
apply is_hset.elim,
end
end-/
theorem op_op : Opposite (Opposite C) = C := theorem op_op : Opposite (Opposite C) = C :=
(ap (Precategory.mk C) (op_op' C)) ⬝ !Precategory.equal (ap (Precategory.mk C) (op_op' C)) ⬝ !Precategory.equal