2
$\begingroup$

I'm stuck on proving extensionality results for my dependent structures in Lean 4. It's turning out to be very difficult to show equalities for these dependent structures, since I require a kind of substitution for dependent types. I kind of want to avoid HEq so I can to avoid complaints about equality of types.

Here's an example for the "category" structure, but it's just an example I'm trying to make work (I really want extensionality results for many of my dependent structures)

Here's the structure:

import Init.Core

-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) → 
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) → 
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z: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


-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g

macro "CAT" : tactic => `(tactic| repeat (rw [category.Id₁]) ; repeat (rw [category.Id₂]) ; repeat (rw [category.Ass]))

I first defined two helping functions for the extensionality result to be expressed:

-- rewriting via obj
def 𝕆𝕓𝕛 (C : category) (D : category) (obj : C.Obj = D.Obj) (X : C.Obj) : D.Obj := by
rw [obj]
exact X

-- rewriting via hom
def ℍ𝕠𝕞 (C : category) (D : category) (obj : C.Obj = D.Obj) (X : C.Obj) (Y : C.Obj) (hom : D.Hom (𝕆𝕓𝕛 C D obj X) (𝕆𝕓𝕛 C D obj Y)) = C.Hom X Y ) (f : C.Hom X Y) : D.Hom (𝕆𝕓𝕛 C D obj X) (𝕆𝕓𝕛 C D obj Y) := by
rw [hom]
exact f

These help to avoid HEq which I don't want to use.

Now, category.mk is a bit complex and of course dependent:

#check category.mk

I'm trying to work with this structure "equal_categories", which pertains to sufficient conditions for categories to be equal:

structure equal_categories where
  Fst : category
  Snd : category
  Obj : Snd.Obj = Fst.Obj
  Hom : (X : Fst.Obj) →
      (Y : Fst.Obj) →
      Snd.Hom
      (𝕆𝕓𝕛 Fst Snd Obj X)
      (𝕆𝕓𝕛 Fst Snd Obj Y)
      =
      Fst.Hom X Y
--  Idn : (X : Fst.Obj) → 
  Cmp : (X Y Z : Fst.Obj) →
      (f : Fst.Hom X Y) →
      (g : Fst.Hom Y Z) →
      (ℍ𝕠𝕞 Fst Snd Obj X Z
      (Hom X Z)
      (Fst.Cmp X Y Z f g))
      =
      Snd.Cmp
      (𝕆𝕓𝕛 Fst Snd Obj X)
      (𝕆𝕓𝕛 Fst Snd Obj Y)
      (𝕆𝕓𝕛 Fst Snd Obj Z)
      (ℍ𝕠𝕞 Fst Snd Obj X Y (Hom X Y) f)
      (ℍ𝕠𝕞 Fst Snd Obj Y Z (Hom Y Z) g)

Now I want to show this

theorem CatExt (P : equal_categories) : P.Fst = P.Snd := by
sorry

I've found that I can witness a constituent of the equal_categories with what I know, but it's really very difficult to perform the necessary replacements to get CatExt. Does anyone have any advice?

Note this is Lean 4.

Edit: after further thought, I am comfortable using HEq because I figured out how to obtain an equality from two HEq-equal terms of the same type.

I kind of want to show this:

def this (X : Type) (Y : Type) (p : X = Y) : HEq (category.mk X) (category.mk Y) := by 
sorry

theorem CatExtObj  {a b:Type} (H : Eq a b) : HEq (category.mk a) (category.mk b) :=
Eq.recOn H (HEq.refl (category.mk a))


theorem hcongrsdfjkjkjkjk {X Y:Type} (H : Eq X Y) : HEq (category.mk X) (category.mk Y) :=
Eq.recOn H (HEq.refl (category.mk X))

Edit: here's a result I want on functors:

-- definition of a functor
structure functor (C : category) (D : category) where
   Obj : ∀(_ : C.Obj),D.Obj
   Hom : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Hom X X (C.Idn X) = D.Idn (Obj X)
   Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),
   D.Cmp (Obj X) (Obj Y) (Obj Z) (Hom X Y f) (Hom Y Z g) = Hom X Z (C.Cmp X Y Z f g)

structure equal_functors (C : category) (D : category) where
  Fst : functor C D
  Snd : functor C D
  Obj : Fst.Obj = Snd.Obj
  Hom : (X : C.Obj) → (Y : C.Obj) → (f : C.Hom X Y) → (HEq (Fst.Hom X Y f) (Snd.Hom X Y f))

theorem FunExtOne (C : category) (D : category) (P : equal_functors C D) (H : Eq P.Fst.Obj P.Snd.Obj) : HEq (functor.mk P.Fst.Obj) (functor.mk P.Snd.Obj) := 
Eq.recOn H (HEq.refl (functor.mk P.Fst.Obj))

theorem FunExt (C : category) (D : category) (P :equal_functors C D) : P.Fst = P.Snd := by 
sorry
```
$\endgroup$
5
  • $\begingroup$ Your MWE doesn't type check. I think you need to replace Cat.Obj with category? $\endgroup$
    – Jason Rute
    Aug 6, 2023 at 22:59
  • $\begingroup$ Sorry, I made some fixes $\endgroup$ Aug 7, 2023 at 0:35
  • $\begingroup$ I've got to fix it but don't have time right now $\endgroup$ Aug 7, 2023 at 0:35
  • $\begingroup$ Also your def of blackboard Hom should use exact f in place of sorry, no? $\endgroup$
    – Jason Rute
    Aug 7, 2023 at 3:07
  • $\begingroup$ Oh, you fixed it! Thanks. $\endgroup$ Aug 7, 2023 at 4:06

1 Answer 1

2
+50
$\begingroup$

Having thought about this for a bit, I'm not 100% certain what you are trying to prove is provable in Lean. (But I'm not positive it isn't provable either.)

Here is what I do know:

Your 𝕆𝕓𝕛 and ℍ𝕠𝕞 definitions could be replaced with the built in cast. Indeed HEq is really just reasoning about cast:

Heterogeneous equality. HEq a b asserts that a and b have the same type, and casting a across the equality yields b, and vice versa.

And one natural way to prove facts about heterogeneous equality is just to convert it to cast equalities (with cast_heq) and reason about the equalities.

Now what you are trying to prove seems to boil down to proving a version of function extentionality for heterogeneous equality, namely

theorem heq_funext (α β : Type u) (γ : Type v) (p : α = β)
    (f : α -> γ) (g : β -> γ)
    (h : (a : α) -> f a = g (cast p a))
  : HEq f g

Edit: The reason it comes down to this is that for two dependent structures (say Sigma) to be equal it is necessary and sufficient for the non-dependent fields to be equal and the dependent fields to be HEq. See for example, Sigma.ext_iff.

But I don't know if this is provable. Indeed HEq comes with a big warning:

You should avoid using this type if you can. Heterogeneous equality does not have all the same properties as Eq, because the assumption that the types of a and b are equal is often too weak to prove theorems of interest. One important non-theorem is the analogue of congr: If HEq f g and HEq x y and f x and g y are well typed it does not follow that HEq (f x) (g y).

Indeed that was the very thing I was stuck on when trying to prove heq_funext.


Here is my partial proof of heq_funext:

theorem heq_fun_ext (α β : Type u) (γ : Type v) (p : α = β)
    (f : α -> γ) (g : β -> γ)
    (h : (a : α) -> f a = g (cast p a))
  : HEq f g := by
  have pp : (α -> γ) = (β -> γ) := by
    simp [p]
  have hh : f = (cast pp.symm g) := by
    apply funext
    intro a
    rw [h, <-heq_eq_eq]
    sorry
  simp [hh, cast_heq]

The goal for sorry is:

    α β : Type u
    γ : Type v
    p : α = β
    f : α → γ
    g : β → γ
    h : ∀ (a : α), f a = g (cast p a)
    pp : (α → γ) = (β → γ)
    a : α
    ⊢ HEq (g (cast p a)) (cast (_ : (β → γ) = (α → γ)) g a)

This is basically a form of the congruence lemma the warning said was not provable.


I'm not certain my skepticism is correct, but I would also think this lemma would be in Mathlib if provable. I think there is a better chance this sort of thing works in homotopy or cubical type theory, but I'm not certain of that either.

$\endgroup$
9
  • $\begingroup$ I don't think your proposition is an example of a problem. I suspect the issue is that if you start with just HEq f g, then you know (α → γ) = (β → δ), but that does not tell you α = β and γ = δ. That would be assuming that is injective. But you have explicitly assumed α = β instead, so that issue doesn't arise. $\endgroup$
    – Dan Doel
    Aug 7, 2023 at 15:07
  • $\begingroup$ @DanDoel do you think my heq_funext lemma is provable, or do you have another way to prove the OPs theorem? (Although I’m pretty sure if you can prove the OP’s theorem you can prove my lemma with the same method.) $\endgroup$
    – Jason Rute
    Aug 7, 2023 at 16:13
  • $\begingroup$ To be clear, by “the OP’s theorem” I mean CatExt. $\endgroup$
    – Jason Rute
    Aug 7, 2023 at 16:23
  • $\begingroup$ The most important extensionality result for me is one on functors, which may be easier. $\endgroup$ Aug 7, 2023 at 17:07
  • $\begingroup$ @Cayley-Hamilton Can you be more specific? What is this functor result you want proved? Also, the main takeaway I think is that equality of dependent structures (especially ones which contain types) is hard in Lean. Many reasonable sounding results are just not provable. That I think is why the existing category theory library works with isomorphisms more than equalities. $\endgroup$
    – Jason Rute
    Aug 7, 2023 at 18:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.