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

chore(hott/algebra) cmall changes in category files

Browse source
This commit is contained in:
Jakob von Raumer 2015-03-11 16:03:10 -04:00 committed by Leonardo de Moura
parent 362a0ec04c
commit 25abecaa26
2 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/groupoid.hlean
View file

@ -18,7 +18,7 @@ namespace category
(all_iso : Π ⦃a b : ob⦄ (f : hom a b), @is_iso ob parent a b f)
abbreviation all_iso := @groupoid.all_iso
attribute groupoid.all_iso [instance]
attribute groupoid.all_iso [instance] [priority 100000]
definition groupoid.mk' [reducible] (ob : Type) (C : precategory ob)
(H : Π (a b : ob) (f : a ⟶ b), is_iso f) : groupoid ob :=

5
hott/algebra/precategory/iso.hlean
View file

@ -35,7 +35,7 @@ namespace iso
definition right_inverse [reducible] := @is_iso.right_inverse
postfix `⁻¹` := inverse
--a second notation for the inverse, which is not overloaded
postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse
postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h
variables {ob : Type} [C : precategory ob]
variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
@ -82,7 +82,8 @@ namespace iso
definition inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
inverse_eq_left !left_inverse
definition inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ = f :=
definition inverse_involutive (f : a ⟶ b) [H : is_iso f] [H : is_iso (f⁻¹)]
: (f⁻¹)⁻¹ = f :=
inverse_eq_right !left_inverse
definition retraction_id (a : ob) : retraction_of (ID a) = id :=