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

chore(hott/algebra) make carrier hset witness an instance

Browse source
This commit is contained in:
Jakob von Raumer 2015-03-19 10:21:54 -04:00 committed by Leonardo de Moura
parent 8948926a07
commit f480d67881
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/group.hlean
View file

@ -52,6 +52,8 @@ structure semigroup [class] (A : Type) extends has_mul A :=
(carrier_hset : is_hset A) (carrier_hset : is_hset A)
(mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c)) (mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c))
attribute semigroup.carrier_hset [instance]
theorem mul_assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) := theorem mul_assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
!semigroup.mul_assoc !semigroup.mul_assoc