## Stream: general

### Topic: to_additive and punit

#### Adrián Doña Mateo (Mar 23 2021 at 20:57):

Why does to_additive fail here? There definitely is a has_add instance for punit.

import algebra.punit_instances

example : add_group punit := infer_instance

lemma foo {G : Type*} [group G] : G ≃* punit := sorry


#### Johan Commelin (Mar 23 2021 at 20:59):

What is the error message that it gives?

#### Adrián Doña Mateo (Mar 23 2021 at 21:03):

type mismatch at application
G ≃+ punit
term
@distrib.to_has_mul punit (@ring.to_distrib punit (@comm_ring.to_ring punit punit.comm_ring))
has type
has_mul punit
but is expected to have type


#### Johan Commelin (Mar 23 2021 at 21:08):

ouch... it's getting the multiplication from the ring structure

#### Johan Commelin (Mar 23 2021 at 21:08):

What exactly are you trying to do? Can you abstract punit away? For example by using a subsingleton type?

#### Adrián Doña Mateo (Mar 23 2021 at 21:11):

I was hoping to define

def of_subsingleton (h : subsingleton G) : G ≃* punit :=
⟨λ _, punit.star, λ _, 1, λ x, subsingleton.elim _ _, λ x, subsingleton.elim _ _, λ _ _, rfl⟩


and transfer it to additive notation.

#### Yury G. Kudryashov (Mar 23 2021 at 21:12):

If you want to fix this, then you should define @[to_additive] instance punit.has_mul, @[to_additive] instance punit.has_one, in algebra/punit_instances, then make sure that all instances in that file use mul := (*) etc.

#### Adrián Doña Mateo (Mar 23 2021 at 21:15):

Okay, I'll give that a go.

#### Johan Commelin (Mar 23 2021 at 21:17):

@Adrián Doña Mateo So, what I would suggest is that you show that two groups G and H with [unique G] and [unique H] are isomorphic.

#### Johan Commelin (Mar 23 2021 at 21:18):

Then you can specialise this to H = punit whenever you want.

#### Adrián Doña Mateo (Mar 23 2021 at 21:19):

Oh yeah, that makes sense. What is the difference between unique and subsingleton?

#### Yury G. Kudryashov (Mar 23 2021 at 21:25):

[unique α] gives you [default α]

#### Yury G. Kudryashov (Mar 23 2021 at 21:26):

But for a [monoid], you already have 1.

#### Adrián Doña Mateo (Mar 23 2021 at 21:26):

Right, in this case it wouldn't matter. Thanks a lot!

#### Johan Commelin (Mar 23 2021 at 21:33):

subsingletons can be empty

Last updated: May 06 2021 at 22:13 UTC