Dependent type hell golfing challenge

Stream: maths

[Mario Carneiro]

This problem is extracted from some code by @Emily Riehl while trying to prove some properties of the slice category, defined directly rather than via the comma category. The trouble is that a natural proof leads to some inconvenient HEq goals, because an associativity application in a morphism means that we end up with an "evil" equality of objects in the slice category, and the morphisms over that equality end up in DTT hell.

import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Category

namespace CategoryTheory

open Category

variable {C : Type u} [Category.{v} C]

structure Slice (X : C) : Type max u v where
  dom : C
  hom : dom ⟶ X

@[ext] structure SliceMorphism {X : C} (f g : Slice X) where
  dom : f.dom ⟶ g.dom
  w : dom ≫ g.hom = f.hom := by aesop_cat

instance sliceCategory (X : C) : Category (Slice X) where
  Hom f g := SliceMorphism f g
  id f := { dom := 𝟙 f.dom }
  comp u v := { dom := u.dom ≫ v.dom, w := by rw [assoc, v.w, u.w] }

def compFunctor {X Y : C} (f : X ⟶ Y) : (Slice X) ⥤ (Slice Y) where
  obj x := {
    dom := x.dom
    hom := x.hom ≫ f
  }
  map {x x' : Slice X} u := {
    dom := u.dom
    w := by rw [← assoc, u.w]
  }

theorem compFunctorial.comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    compFunctor f ⋙ compFunctor g = compFunctor (f ≫ g) := by
  dsimp [sliceCategory, Functor.comp, compFunctor]
  congr
  · ext x
    congr 1
    rw [assoc]
  · sorry -- what the heq

[Mario Carneiro]

my solution

structure UnpackedSliceFunctor (D) [Category D] (X) where
  dom : D → C
  hom (a) : dom a ⟶ X
  map {a b : D} : (a ⟶ b) → (dom a ⟶ dom b)

def unpackSliceFunctor {D} [Category D] {X : C} (F : D ⥤ Slice X) : UnpackedSliceFunctor D X where
  dom := fun x => (F.obj x).dom
  hom := fun x => (F.obj x).hom
  map := fun f => (F.map f).1

theorem unpackSliceFunctor.inj {D} [Category D] {X : C} {F G : D ⥤ Slice X}
    (eq : unpackSliceFunctor F = unpackSliceFunctor G) : F = G :=
  let f (F : D ⥤ Slice X) : { F : UnpackedSliceFunctor D X //
    (∀ {x x' : D} (u : x ⟶ x'), F.map u ≫ F.hom x' = F.hom x) ∧
    (∀ X, F.map (𝟙 X) = 𝟙 (F.dom X)) ∧
    (∀ {a b c} (f : a ⟶ b) (g : b ⟶ c), F.map (f ≫ g) = F.map f ≫ F.map g) } :=
  ⟨unpackSliceFunctor F,
    fun u => (F.map u).2,
    fun X => (SliceMorphism.ext_iff ..).1 (F.map_id X),
    fun f g => (SliceMorphism.ext_iff ..).1 (F.map_comp f g)⟩
  let g F : D ⥤ Slice X := {
    obj := fun x => ⟨F.1.dom x, F.1.hom x⟩
    map := fun x => ⟨F.1.map x, F.2.1 x⟩
    map_id := fun x => (SliceMorphism.ext_iff ..).2 (F.2.2.1 x)
    map_comp := fun f g => (SliceMorphism.ext_iff ..).2 (F.2.2.2 f g)
  }
  (show Function.LeftInverse g f from fun _ => rfl).injective (Subtype.ext eq)

theorem compFunctorial.comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    compFunctor f ⋙ compFunctor g = compFunctor (f ≫ g) := by
  apply unpackSliceFunctor.inj
  dsimp [unpackSliceFunctor]
  congr 1; ext x
  dsimp [compFunctor]
  rw [assoc]

[Adam Topaz]

equality of functors!

[Adam Topaz]

in general you would want a natural iso instead.

[Mario Carneiro]

oh yeah, forgot to mention: this is dealing with Cat as a category so yeah, we have that :(

[Mario Carneiro]

we need some functors to/from Cat

[Adam Topaz]

We have Cat as a bicategory, which is a better setting.

[Mario Carneiro]

I'm pretty sure there are worse demons to be had there ;)

[Adam Topaz]

In any case, I think docs#CategoryTheory.Functor.hext is almost always better than using ext.

[Mario Carneiro]

that is slightly better, but unfortunately it doesn't solve the main problem, the HEq is still hard to prove (I think?)

[Adam Topaz]

There's also docs#CategoryTheory.Functor.ext

[Adam Topaz]

which involves eqToHoms

[Andrew Yang]

lemma eqToHom_dom {X : C} {x y : Slice X} (e : x = y) : (eqToHom e).dom = eqToHom (e ▸ rfl) := by
  subst e; rfl

theorem compFunctorial.comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    compFunctor f ⋙ compFunctor g = compFunctor (f ≫ g) := by
  fapply Functor.ext
  · intro x
    dsimp [sliceCategory, Functor.comp, compFunctor]
    rw [assoc]
  · intro x y f
    dsimp [sliceCategory, Functor.comp, compFunctor]
    ext
    simp only [eqToHom_dom, eqToHom_refl, comp_id, id_comp]

[Kyle Miller]

The congr! tactic gives you some additional equalities in the local context to deal with the HEq

theorem compFunctorial.comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    compFunctor f ⋙ compFunctor g = compFunctor (f ≫ g) := by
  dsimp [sliceCategory, Functor.comp, compFunctor]
  congr! 4
  · rw [assoc]
  · subst_vars
    congr! 3 <;> rw [assoc]

[Andrew Yang]

Turns out aesop_cat can handle everything (as expected) if you mark eqToHom_dom as simp

theorem compFunctorial.comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    compFunctor f ⋙ compFunctor g = compFunctor (f ≫ g) := by
  fapply Functor.ext <;> dsimp [sliceCategory, compFunctor] <;> aesop_cat

[Emily Riehl]

@Adam Topaz there's a reason you might want an identity here which if for applications to Beck Chevalley isos involving the adjoint functors to composition you get from having pullbacks or an LCC structure. @Sina H 𓃵 and I have a paper where you prove that various diagrams of natural transformations commute bc these natural transformations are iteratively defined by mates of identity natural transformations between composition functors. And if the map from a category C to Cat by taking slices is strictly functional than it's automatically coherent.

You'd get the same result I suppose by showing that this is pseudofunctorial (as opposed to just functional up to iso) but this seems like a nice place to use strict equality in set theory. Which is why I'm curious if the same holds here.

[Adam Topaz]

I see. Interesting! I think it may be worthwhile for someone (maybe me...) to try to define this pseudofunctor to check whether our automation is good enough to make things easy.

[Joël Riou]

Note: the slice category is already defined in mathlib as Over.

eqToHom are already used a little bit in this context in mathlib (@Markus Himmel may comment more about this). To a certain extent, it makes reasonable sense, because on objects dom, we tend to have definitional equalities, but on the hom part, we often need to use associativity or composition with identities (and such equalities are certainly not "evil").

I would suggest that the basic API in such situations should provide isomorphisms of functors, even though we may also have a lemma stating the equality (and that the iso coincide with the eqToIso). Then, the "cocycle" conditions should not difficult to obtain.

(Similar problems would arise for the functoriality of the Dold-Kan equivalence. The equivalence is in mathlib, but I have not PRed the functoriality compatibilities with respect to an additive functor. For one of the two functors of the equivalence, the functoriality can be stated as an equality of functors, which would also give automatically the required compatibilities in obtain to promote this to a pseudo-functor.)

[Dean Young]

https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Control/Functor.lean#L50-L60

[Eric Wieser]

@Dean Young, that doesn't look particularly relevant to me.

[Emily Riehl]

@Eric Wieser @Andrew Yang @Mario Carneiro This worked for me:

namespace Over
variable {C : Type u} [Category.{v} C]

@[simp]
theorem eqToHom_left {X : C} {x y : Over X} (e : x = y) : (eqToHom e).left = eqToHom (e ▸ rfl) := by
  subst e; rfl

theorem map.comp_eq {X Y Z : C}(f : X ⟶ Y)(g : Y ⟶ Z) :
    map f ⋙ map g = map (f ≫ g) := by
  fapply Functor.ext
  · dsimp [Over, Over.map]
    intro x
    unfold Comma.mapRight
    simp
  · intros x y u
    ext
    simp

end Over

[Emily Riehl]

But @Andrew Yang I don't understand the statement (nor the intuition) for your lemma.

If x : x.left -> X and y : y.left -> X then (eqToHom e).left : x.left -> y.left so eqToHom (e ▸ rfl) must be too. I guess from context the rfl must be of type x.left = x.left and e ▸ rflis the transport of this term along the path e : x = y using the type family (=motive)

(z : Over X) -> x.left = z.left

But how did you know this would be a useful reduction to make?

[Andrew Yang]

I believe that your understanding of the statement is correct. As for the intuition, the easy answer is "I invoked simp and see that (eqToHom e).left appears in the goal". But in general it is useful to have such lemmas showing that eqToHom is mapped to eqToHom under functorial constructions (e.g. docs#CategoryTheory.eqToHom_map)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Why is eqToHom_map not marked as simp? The docstring answers this.