Category-of-everything axiom?

Stream: general

[Tanner Swett]

I'm curious if anyone's ever heard of or investigated the following axiom: "Given any category C, there is a full and faithful functor from C to the category of types." Such an axiom might make it easier to prove things about some categories... although I admit I haven't thought it through at all.

[Matthew Ballard]

docs#CategoryTheory.ConcreteCategory might interest you

[Matthew Ballard]

Fullness is a pretty big ask though

[Chris Hughes]

It might even be provable in Lean if you are willing to go up a universe. Does (C ⥤ Type) embed into Type 1 by sending F to Hom (Terminal Object) F work? And then you compose this with Yoneda. I haven't thought hard about this, and I'm probably missing something, but it's a suggestion.

[Tanner Swett]

I would be pretty surprised if it were provable in Lean. There is a category (in fact, exactly two categories) that has exactly one object, which has exactly two endomorphisms, so this axiom would assert that there is some type a such that there are exactly two functions a -> a. On the other hand, I think Lean is consistent with ordinary set theory, which asserts that there is no type a with exactly two functions a -> a.

[Floris van Doorn]

Yes, that is also provable in Lean (using choice):

import Mathlib.SetTheory.Cardinal.Basic

open Cardinal Order

example : ¬ ∃ (α : Type u), #(α → α) = 2 := by
  push_neg
  intros α hα
  simp at hα
  rcases eq_zero_or_pos (a := #α) with h|h
  · simp [h] at hα
  simp [← succ_le_iff] at h
  rcases h.eq_or_lt with h2|h2
  · simp [← h2] at hα
  have : 2 ≤ #α
  · rw [← succ_le_iff] at h2
    norm_cast at h2
  rcases this.eq_or_lt with h2|h2
  · simp [← h2] at hα
    norm_cast at hα
  have := self_le_power #α h
  simp_rw [hα, h2.not_le] at this

[Chris Hughes]

You don't need choice to prove it, for this statement at least. Only Quot.sound is used here, so you need a pretty weak type theory for a Category of everything axiom to be consistent.

import Mathlib

universe u

lemma card_not_two {α : Type u} {f g : α → α}
    (hfg : f ≠ g) (h : ∀ h, f = h ∨ g = h) : False := by
  have h1 : ¬ ∀ a b : α, a = b := by
    intro hab
    apply hfg
    ext x
    exact hab _ _
  have h2 : ∀ a b : α, a = b := by
    intro a b
    rcases h (fun _ => a) with rfl | rfl
    · rcases h (fun _ => b) with h | rfl
      · exact congr_fun h a
      · rcases h id with h | h
        · exact congr_fun h b
        · exact (congr_fun h a).symm
    · rcases h (fun _ => b) with rfl | h
      · rcases h id with h | h
        · exact (congr_fun h a).symm
        · exact (congr_fun h b)
      · exact congr_fun h a
  exact h1 h2

#print axioms card_not_two

lemma card_is_two {α : Type u} {f g : α → α}
    (hfg : f ≠ g) (h : ∀ h, f = h ∨ g = h) : Cardinal.mk (α → α) = 2 := by
  letI : Fintype (α → α) :=
    ⟨⟨[f, g], by simp [hfg]⟩, fun i => by cases h i <;> simp_all⟩
  simp; rfl

[Trebor Huang]

No, this is because Lean implicitly assumes axiom K. In HoTT (consistent with LEM and AC) the delooping of Z/2Z has exactly two endomorphisms. (Caveat: the type of endomorphisms is not isomorphic to Bool, it just has cardinality 2.) However it's still impossible to get the other two-morphism-single-object category though, because there's always the constant map on inhabited objects, which is invertible iff the type is a singleton.