# Zulip Chat Archive

## Stream: new members

### Topic: golfing Lawvere's fixed-point theorem

#### Matt Diamond (Oct 15 2022 at 19:19):

I'm trying to gain a better understanding of category theory, so I wrote up a proof of Lawvere's fixed-point theorem as an exercise (specifically the category-theoretical version... the proof using functions and types is much simpler and I've done that already). My solution feels a bit inelegant though, and I'm wondering if it could be shorter. I suspect that someone who knows what they're doing could golf it down to a few lines. I'm curious to see what that ideal proof looks like.

```
import category_theory.closed.cartesian
open category_theory category_theory.limits.prod
variables {C : Type*} [category C]
[limits.has_finite_products C]
[cartesian_closed C]
{A B : C}
def point_surjective (Φ : A ⟶ B) : Prop :=
∀ (q : ⊤_ C ⟶ B), ∃ (p : ⊤_ C ⟶ A), p ≫ Φ = q
theorem lawvere (h : ∃ (Φ : A ⟶ (B ^^ A)), point_surjective Φ)
: ∀ (f : End B), ∃ (s : ⊤_ C ⟶ B), f • s = s :=
begin
intro f,
cases h with Φ psurj_Φ,
set g : A ⟶ B := lift (𝟙 A) Φ ≫ (exp.ev A).app B ≫ f with hg,
set q : ⊤_ C ⟶ B ^^ A := internalize_hom g with hq,
cases psurj_Φ q with x hx,
set s : ⊤_ C ⟶ B := lift x q ≫ (exp.ev A).app B with hs,
have h : lift x (𝟙 ⊤_ C) ≫ cartesian_closed.uncurry q = s, {
rw [hs, cartesian_closed.uncurry_eq],
simp,
},
rw [
hq, internalize_hom, cartesian_closed.uncurry_curry,
lift_fst_assoc, hg, comp_lift_assoc, category.comp_id,
hx, ← category.assoc, ← hs
] at h,
exact ⟨s, h⟩,
end
```

#### Adam Topaz (Oct 15 2022 at 19:43):

Aside from some very minor golfing, this looks like a good proof to me!

#### Martin Harrison (Oct 15 2022 at 19:49):

What is golfing? I am picturing a scene on the putting green where you take many extra steps, tapping the ball here and there before sinking it. Is that the meaning?

#### Matt Diamond (Oct 15 2022 at 19:50):

@Adam Topaz Thanks!

#### Matt Diamond (Oct 15 2022 at 19:52):

@Martin Harrison It's from "code golfing", which is when people try to write a piece of code in the shortest possible way

#### Matt Diamond (Oct 15 2022 at 19:53):

#### Adam Topaz (Oct 15 2022 at 19:55):

There may be a few smaller lemmas that would be useful and could shorten it.... I don't know if I'll have time to play around with this right now, but I'll try later.

#### Matt Diamond (Oct 15 2022 at 19:56):

Sounds good! No pressure, of course... I just wanted to make sure I wasn't missing something wildly obvious. Glad to hear it's on the right track.

#### Kyle Miller (Oct 15 2022 at 20:20):

@Martin Harrison In golf you're trying to take the fewest strokes to get the ball in the hole. In code golf you're trying to take the fewest keystrokes.

#### David Wärn (Oct 16 2022 at 09:02):

Personally I like the idea of working with Cartesian closed categories as if they were `Type`

. In this spirit, here's what a statement and proof can look like:

```
lemma lawvere
(φ : Γ ⟶ X ⟹ X ⟹ Y)
(φ_surj : ∀ y : Γ ⟶ X ⟹ Y, ∃ x : Γ ⟶ X, φ x = y)
(f : Γ ⟶ Y ⟹ Y) :
∃ s : Γ ⟶ Y, f s = s :=
let q : Γ ⟶ X ⟹ Y := by clear φ_surj; c_intro x; exact f (φ x x) in
let ⟨p, hp⟩ := φ_surj q in
⟨φ p p, by conv_rhs { rw [hp, beta, category.id_comp, category.id_comp] }⟩
```

It is based on a general `c_intro`

tactic and associated (sorried!) lemma `beta`

which can be found here

#### David Michael Roberts (Oct 16 2022 at 10:15):

With blatant self-promotion, you can prove Lawvere's theorem with much less https://arxiv.org/abs/2110.00239 so you can rely on less background material

#### Matt Diamond (Oct 16 2022 at 19:21):

@David Michael Roberts Nice! Do pointed magmoidal categories exist in mathlib?

#### David Michael Roberts (Oct 16 2022 at 22:00):

Not that I know! The axioms are so minimal it seems not terrible to formalise directly

#### Matt Diamond (Oct 16 2022 at 22:23):

@David Wärn It looks like you're applying morphisms as if they were functions... I didn't think that was possible in mathlib. Do you have some kind of `has_coe_to_fn`

set up with `quiver.hom`

?

#### David Wärn (Oct 17 2022 at 07:55):

Ah yes, it's this coercion in the gist

```
instance : has_coe_to_fun (Γ ⟶ X ⟹ Y) (λ _, (Γ ⟶ X) → (Γ ⟶ Y)) :=
⟨λ f g, prod.lift g f ≫ (exp.ev X).app Y⟩
```

Last updated: Dec 20 2023 at 11:08 UTC