## Stream: maths

### Topic: strictification

#### Reid Barton (May 26 2018 at 19:15):

If α is a type, then as @Kevin Buzzard describes near https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/affine.20schemes.20are.20schemes/near/126963972, we can interpret α as a groupoid whose objects are the "inhabitants of α up to defeq" and whose morphisms are propositional equalities, that is, the morphisms from a to b are the inhabitants of a = b (and so a morphism from a to b is unique if it exists, by proof irrelevance).
Suppose now α is a monoid. Then associativity is a propositional equality (a * b) * c = a * (b * c) and not necessarily a defeq, so under this interpretation α corresponds to a monoidal groupoid which is not necessarily strict.

#### Reid Barton (May 26 2018 at 19:18):

But we can replace α with a strict monoidal groupoid using standard strictification results. Here, for example, α acts on itself by left multiplication, and then α is isomorphic to the image of this action in the endomorphism monoid α → α, which is strictly associative and unital.

#### Reid Barton (May 26 2018 at 19:18):

For the monoid list t, this is basically the "difference list" construction

#### Reid Barton (May 26 2018 at 19:19):

More generally, any category is isomorphic to a category whose composition is strictly associative and unital.

#### Reid Barton (May 26 2018 at 19:28):

I wonder how useful this observation is. I encountered it in a situation similar to the following. Consider a type indexed on a monoid, like def vector (α : Type u) (n : ℕ) := { l : list α // l.length = n }. Then append is an operation {n m : nat} : vector α n → vector α m → vector α (n + m). In order to state associativity of append, we need to use transport across the equality (n + m) + k = n + (m + k), or use heterogeneous equality.
If we replaced ℕ with a "strictly associative" version, we wouldn't need to do this.

#### Reid Barton (May 26 2018 at 19:28):

I haven't yet tried putting this plan into practice, though.

#### Reid Barton (May 26 2018 at 20:19):

Actually, this is kind of funny. This construction gives you a monoid which is strictly associative, but not strictly unital.

#### Reid Barton (May 26 2018 at 20:34):

https://gist.github.com/rwbarton/658ccdd57986b32fd8be0c155c63d47e#file-strictification-lean-L21

#### Reid Barton (May 26 2018 at 20:37):

Now as soon as I write this I realize I actually need the additive version, hah.

Last updated: May 11 2021 at 16:22 UTC