weird Lean proofs

Stream: maths

[Reid Barton]

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.

[Kenny Lau]

you what

[Keeley Hoek]

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]

@Kevin Buzzard "lean will revolutionize mathematics"

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

Anyway, it's probably just taste.

[Mario Carneiro]

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

[Chris Hughes]

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

[Reid Barton]

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]

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]

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