Proving extensionality for category structure with 7 entries

Stream: maths

[Dean Young]

@Kim Morrison @Adam Topaz do you think there would be dependent type hell with regards to EnrichedCatExt?

@Shanghe Chen and I think we can show a version of the below for enriched categories.

/--
 The version of ext for two input arguments
 ref: https://proofassistants.stackexchange.com/questions/2352/dependent-replacement-in-lean
 The comment by Dan Doel linking to https://hub.darcs.net/dolio/agda-share/browse/HEqExt.agda
 hints this proof
-/
theorem HEqFunExt₁.{u, v} (α β : Type u) (γ : Type v) (p : α = β)
    (f : α -> α -> γ) (g : β -> β -> γ)
    (h : (a : α) -> (b : α) -> f a b = g (cast p a) (cast p b))
  : HEq f g := by
  cases p
  simp
  ext x y
  revert x y
  assumption

/--
 A version of ext for the input arguments like the data of two categories... Quite complicated
 simplified version: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Improve.20a.20proof.20related.20to.20funext
-/
theorem HEqFunExt₂.{u, v} (α β : Sort u) (p : α = β)
    (f : α -> α -> Sort v) (g : β -> β -> Sort v)
    (q : (a : α) -> (b : α) -> f a b = g (cast p a) (cast p b))
    (h : (a a' a'' : α) -> (f a a') -> (f a' a'') -> (f a a''))
    (i : (b b' b'' : β) -> (g b b') -> (g b' b'') -> (g b b''))
    (j : (a a' a'' : α ) -> (x: f a a') -> (y : f a' a'') ->
            cast (q a a'') (h a a' a'' x y) = i (cast p a) (cast p a') (cast p a'') (cast (q a a') x) (cast (q a' a'') y))
      : HEq h i
    := by
  cases p
  simp at *
  let k : f = g := by
    ext x y
    exact q x y
  cases k
  simp at *
  ext a a' a'' x y
  apply j

/--
a version for ext for the identity part of equality
-/
theorem HEqFunExt₃.{u, v} (α β : Sort u) (p : α = β)
    (f : α -> α -> Sort v) (g : β -> β -> Sort v)
    (q : (a : α) -> (b : α) -> f a b = g (cast p a) (cast p b))
    (i : (a : α) -> f a a)
    (j : (b : β) -> g b b)
    (k : (a : α) -> cast (q a a) (i a) = j (cast p a)) : HEq i j
    := by
  cases p
  simp at *
  let l : f = g := by
    apply funext
    intro x
    apply funext
    intro y
    apply q
  cases l
  simp at *
  apply funext
  intro a
  apply k

/--
Category as a structure, with the ext attribute
-/

@[ext]
structure Category₇.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj -> Obj -> Type v₀
  Idn : (X:Obj) -> Hom X X
  Cmp : (X Y Z : Obj) -> (_:Hom X Y) -> (_:Hom Y Z) -> Hom X Z
  Id₁ : (X Y : Obj) -> (f:Hom X Y) ->
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X Y : Obj) -> (f:Hom X Y) ->
    Cmp X X Y (Idn X) f = f
  Ass : (X Y Z W : Obj) -> (f:Hom W X) -> (g:Hom X Y) -> (h:Hom Y Z) ->
    Cmp W X Z f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h

-- print to see how ext is generated
-- #print Category₇.ext

structure Category₆.{u₀,v₀} (Obj : Type u₀) where
  Hom : Obj -> Obj -> Type v₀
  Idn : (X:Obj) -> Hom X X
  Cmp : (X Y Z : Obj) -> (_:Hom X Y) -> (_:Hom Y Z) -> Hom X Z
  Id₁ : (X Y : Obj) -> (f:Hom X Y) ->
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X Y : Obj) -> (f:Hom X Y) ->
    Cmp X X Y (Idn X) f = f
  Ass : (X Y Z W : Obj) -> (f:Hom W X) -> (g:Hom X Y) -> (h:Hom Y Z) ->
    Cmp W X Z f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h

structure EqualCategories₇ where
  Fst : Category₇
  Snd : Category₇
  Obj : Fst.Obj = Snd.Obj
  Hom : (X Y : Fst.Obj) → Fst.Hom X Y = Snd.Hom (cast Obj X) (cast Obj Y)
  Idn : (X : Fst.Obj) → cast (Hom X X) (Fst.Idn X) = Snd.Idn (cast Obj X)
  Cmp : (X Y Z : Fst.Obj) → (f : Fst.Hom X Y) → (g : Fst.Hom Y Z) →
      (cast (Hom X Z) (Fst.Cmp X Y Z f g)) = Snd.Cmp (cast Obj X) (cast Obj Y) (cast Obj Z) (cast (Hom X Y) f) (cast (Hom Y Z) g)


theorem CatExt₇ (P : EqualCategories₇) : P.Fst = P.Snd := by
  cases P
  case mk Fst Snd Obj Hom Idn Cmp =>
  simp
  simp [cast] at Hom
  ext
  case Obj => rw [Obj]
  case Cmp =>
    apply HEqFunExt₂ Fst.Obj Snd.Obj Obj Fst.Hom Snd.Hom Hom Fst.Cmp Snd.Cmp Cmp
  case Hom =>
    apply HEqFunExt₁ _ _ _ Obj
    intro a b
    apply Hom
  case Idn =>
    apply HEqFunExt₃ Fst.Obj Snd.Obj Obj Fst.Hom Snd.Hom Hom Fst.Idn Snd.Idn Idn


theorem CatExt₆ (P : EqualCategories₇) : P.Fst = P.Snd := by
  cases P
  case mk Fst Snd Obj Hom Idn Cmp =>
  simp
  simp [cast] at Hom
  ext
  case Obj => rw [Obj]
  case Cmp =>
    apply HEqFunExt₂ Fst.Obj Snd.Obj Obj Fst.Hom Snd.Hom Hom Fst.Cmp Snd.Cmp Cmp
  case Hom =>
    apply HEqFunExt₁ _ _ _ Obj
    intro a b
    apply Hom
  case Idn =>
    apply HEqFunExt₃ Fst.Obj Snd.Obj Obj Fst.Hom Snd.Hom Hom Fst.Idn Snd.Idn Idn

[Kim Morrison]

I don't understand the purpose of this code.

[Kim Morrison]

I'm sorry, I didn't mean to upset you. It was a request for explanation what problem you are trying to solve, and what this code is doing to solve the problem.

[Kim Morrison]

I understand the general problem of DTT hell in category theory, and that it is a bad idea to use extensionality in categorical settings. Can you explain starting from there?

[Kim Morrison]

(More text, less code, to begin with!)

[Dean Young]

Thanks for your patience.

Here I am interested in rw [] in tactic mode and countable models of the category of categories. It's known that ZFC has countable models.

I think it's interesting to construct a countable model of the strict twocategory of categories. The result above combines fruitfully with functor extensionality and the extensionality for natural transformations. The interesting question is whether one can form the category of categories in a way such that it has countably many 0-cells, 1-cells, 2-cells, and equations.

Here are some constructions that could be featured in a countable strict twocategory:

• It is possible to form Set using one atomic cell and a fiat about its relationship with adjunctions.
• A Kan extension along the Yoneda embedding with the necessary addition of a universe is related to ends and coends.
• The category of elements gets an atomic cell
• [-,X] : Set ⭢ Set after defining Set (by fiat) as a 1-cell adjoint to product, where product of 1-cells X, Y : * ⭢ Set is defined with the universal property.

[Kim Morrison]

What is "the result above", informally?

[Andrew Yang]

Even if you are working with strict 2-cat, I don't think you would ever need equality of categories?

[Dean Young]

@Kim Morrison For a structure with potentially dependent entries, we might wonder whether there is an associated algorithm for it which produces grounds by which two instances are equal and which replaces one entry at a time, but which features only homogeneous equalities and cast (cast can be recovered from rw [], exact, and tactic mode).

After reflecting on this, I decided that a tough goal could be to show that the 7-entry category is one of these structures, even though we would never need equality of categories. That goal also suits the thought about countable models.

A bit more specific: for a structure S with n dependent entries, and s, t particular terms of type S, we might wonder whether there is a algorithm for S which produces grounds G by which s = t, which G features only homogeneous equalities and not HEq. This could be called a homogeneous replacement result.

We can begin by taking a variable v of type S whose first entry is v₀, along with a potentially empty G. Then we consider an alternative to v₀, a variable w₀, and let g₀ be the grounds under which they are equal. Then add g₀ to G, take v₀ out of S, and replace the occurrences of v₀ in the remaining entries of S using g₀.

We iterate this process until taking out v₀ would produce an empty structure, in which case we add g₀ to G and terminate.

In the above, G is EqualCategories₇ and the proof that G produces grounds for replacement is CatExt₇. G features only homogeneous equalities, so the result is that Category₇ has homogeneous replacement (however the intermediate steps you see do make use of HEq). This implies the same result for Category X.

[Kim Morrison]

I don't understand the desire to avoid HEq, while not minding cast. They're not so different.

[Andrew Yang]

See docs#cast_eq_iff_heq and docs#type_eq_of_heq

[Dean Young]

@Andrew Yang @Kim Morrison thanks for this. I didn't know about the batteries section.

Plus @[ext] is shorter and you can get an equality from two HEq-equal terms of the same type.