lawvere fixed point

lawvere.lean

import category_theory.closed.cartesian

noncomputable theory

open category_theory category_theory.limits tactic interactive interactive.types

def tidy_prod_helper {C} [category C] [has_binary_products C] {Γ X Y : C}
  (h : Π Δ, (Δ ⟶ Γ) → (Δ ⟶ X) → (Δ ⟶ Y)) : X ⨯ Γ ⟶ Y :=
h (X ⨯ Γ) limits.prod.snd limits.prod.fst

namespace tactic

-- from Flypitch
meta def get_name : expr → name
| (expr.const c [])          := c
| (expr.local_const _ c _ _) := c
| _                          := name.anonymous

-- given `f : Δ → Γ` and `h : Γ ⟶ X`, replace `h` with `f ≫ h : Δ ⟶ Γ`
meta def clear_hom (f Δ Γ h : expr) : tactic unit :=
try $ do
  `(%%Γ ⟶ %%X) ← infer_type h,
  replace (get_name h) ``(%%f ≫ %%h)

-- given `f : Δ → Γ`, replace all assumptions `Γ ⟶ X` with `Δ ⟶ Γ`,
-- clear `f` and `Γ`, and rename `Δ` to `Γ`.
meta def rebase_context (f : expr) : tactic unit :=
do
  `(%%Δ ⟶ %%Γ) ← infer_type f,
  ctx ← local_context,
  ctx.for_each (clear_hom f Δ Γ),
  clear f,
  clear Γ,
  rename (get_name Δ) (get_name Γ)

namespace interactive

-- changes a goal `Γ ⨯ X ⟶ Y` to `Γ ⟶ Y` and adds an assumption `n : Γ ⟶ X` to context.
meta def tidy_prod (n : parse $ optional ident_) : tactic unit :=
do
  `[refine tidy_prod_helper _, intro],
  f ← intro1,
  nm ← n.elim (get_unused_name "H") pure,
  intro nm,
  rebase_context f

-- changes a goal `Γ ⟶ X ⟹ Y` to `Γ ⟶ Y` and adds an assumption `n : Γ ⟶ X` to context.
-- this gives the illusion that `(Γ ⟶ X) → (Γ ⟶ Y)` is sufficient to deduce `Γ ⟶ (X ⟹ Y)`.
meta def c_intro (n : parse $ optional ident_) : tactic unit :=
`[refine category_theory.cartesian_closed.curry _] >> tidy_prod n

end interactive
end tactic

variables {C : Type*} (Γ X Y Z W : C) [category C] [has_finite_products C] [cartesian_closed C]

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

-- TODO more general version where we have Δ ⟶ Γ
@[simp]
lemma beta (h : Π Δ, (Δ ⟶ Γ) → (Δ ⟶ X) → (Δ ⟶ Y)) (x : Γ ⟶ X) :
(cartesian_closed.curry (tidy_prod_helper h) : Γ ⟶ X ⟹ Y) x = h Γ (𝟙 Γ) x :=
begin
  sorry, -- TODO prove this!
end

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] }⟩
-- we should be able to remove the `clear φ_surj` invocation above, 
-- by having `c_intro` automatically clear hypotheses when needed