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

fix(library/algebra/category/constructions): make proof more robust

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-20 18:20:28 -07:00
parent e9b92adf29
commit c2ed5d3f1f
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/algebra/category/constructions.lean
View file

@ -39,8 +39,8 @@ namespace category
theorem op_op' {ob : Type} (C : category ob) : opposite (opposite C) = C :=
category.rec (λ hom comp id assoc idl idr, refl (mk _ _ _ _ _ _)) C
theorem op_op : Opposite (Opposite C) = C :=
(@congr_arg _ _ _ _ (Category.mk C) (op_op' C)) ⬝ !Category.equal
definition op_op : Opposite (Opposite C) = C :=
(@congr_arg _ _ (@opposite C (@opposite C C)) _ (Category.mk C) (op_op' C)) ⬝ !Category.equal
end
end opposite