# Zulip Chat Archive

## 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