## Stream: maths

### Topic: weird Lean proofs

#### Reid Barton (Nov 29 2018 at 01:36):

Lemma. If $t : (X_j)_{j \in J} \to X$ is a colimit cocone in Set, then every element of $X$ is in the image of $X_j \to X$ for some $j \in J$.

Proof. Let $f : X \to \mathtt{Prop}$ be the function sending x to ∃ j y, t.ι.app j y = x and let $g$ be the constant function true. Then $f$ and $g$ agree after precomposition with each $X_j \to X$, so they are equal.

you what

#### Keeley Hoek (Nov 29 2018 at 01:43):

To a category theorist, on a scale of 1-10, how old is the "I think it's actually called a 'ne'" joke

#### Kenny Lau (Nov 29 2018 at 01:45):

@Kevin Buzzard "lean will revolutionize mathematics"

#### Johan Commelin (Nov 29 2018 at 05:24):

To a category theorist, on a scale of 1-10, how old is the "I think it's actually called a 'ne'" joke

I think that joke turned 10 several years ago...

#### Mario Carneiro (Nov 29 2018 at 05:29):

I don't see why this is a weird proof. Isn't this basically how you prove that epis are surjective in Set?

#### Johan Commelin (Nov 29 2018 at 05:31):

We don't have Curry-Howard in mathematics, remember (-;

#### Johan Commelin (Nov 29 2018 at 05:31):

So you can't even write this proof down in "mathematics"

#### Mario Carneiro (Nov 29 2018 at 05:32):

yes you can, just make f take values in {0, 1} or something, or do equality of sets instead (i.e. f denotes a subset of X)

#### Johan Commelin (Nov 29 2018 at 05:36):

Sure... But I agree with Reid that is just feels a lot different then when you build a map to Prop.

#### Johan Commelin (Nov 29 2018 at 05:36):

Anyway, it's probably just taste.

#### Mario Carneiro (Nov 29 2018 at 05:37):

I think that this is one of the really interesting places where you get a truly nonconstructive exists without choice

#### Chris Hughes (Dec 03 2018 at 19:03):

Can you prove the existence of a colimit cocone in Set without choice though?

#### Reid Barton (Dec 03 2018 at 19:06):

Yes (https://github.com/leanprover/mathlib/blob/master/category_theory/limits/types.lean#L49), and what I would consider the "normal" proof of the original fact consists of writing down this formula (which one has presumably done already), noting that the fact is obvious in this case, and using essential uniqueness of the colimit

#### Reid Barton (Dec 03 2018 at 19:12):

It might actually end up being easier in Lean than the one I outlined above, because I needed to do some juggling to get Prop into the correct universe to make that proof actually work

#### Reid Barton (Dec 03 2018 at 19:16):

You might be thinking of the situation where you have a type X and some subsets whose union is all of X, and you want to prove that X is some kind of colimit of the subsets

Last updated: May 06 2021 at 18:20 UTC