Proving extentionality for category structure with 7 entries

Stream: maths

[Dean Young]

Does anyone have any advice on how to prove extensionality for the category structure with seven entries? See CatExt here.

def zero : Nat := 0


def reflexivity {X : Type} {x : X} : x = x := Eq.refl x


def symmetry {X : Type} {x : X} {y : X}  (p : x = y) := Eq.symm p


def transitivity {X : Type} {x : X} {y : X} {z : X} (p : x = y) (q : y = z) := Eq.trans p q


def extensionality (f g : X → Y) (p : (x:X) → f x = g x) : f = g := funext p


def equal_arguments {X : Type} {Y : Type} {a : X} {b : X} (f : X → Y) (p : a = b) : f a = f b := congrArg f p

def equal_functions {X : Type} {Y : Type} {f₁ : X → Y} {f₂ : X → Y} (p : f₁ = f₂) (x : X) : f₁ x = f₂ x := congrFun p x

def pairwise {A : Type} {B : Type} (a₁ : A) (a₂ : A) (b₁ : B) (b₂ : B) (p : a₁ = a₂) (q : b₁ = b₂) : (a₁,b₁)=(a₂,b₂) := (congr ((congrArg Prod.mk) p) q)


-- 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:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C



-- Notation for composition which infers the 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


theorem Id₁ {C : category} {X : C.Obj} { Y : C.Obj} {f : C.Hom X Y} :
  (f ∘_(C) (𝟙_(C) X)) = f := C.Id₂ X Y f

theorem Id₂ {C : category} {X Y : C.Obj} {f : C.Hom X Y} :
  (𝟙_(C) Y ∘_(C) f) = f := C.Id₁ X Y f

theorem Ass {C : category} {W X Y Z : C.Obj} {f : C.Hom W X} {g : C.Hom X Y} {h : C.Hom Y Z} :
  ((h ∘_(C) g) ∘_(C) f) = (h ∘_(C) (g ∘_(C) f)) := (C.Ass W X Y Z f g h)


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

example {C : category}
          {W : C.Obj}
          {X : C.Obj}
          {Y : C.Obj}
          {Z : C.Obj}
          {f : C.Hom W X}
          {g : C.Hom X Y}
          {h : C.Hom Y Z}
          {i : C.Hom Z W}:
     (i ∘_(C) (h ∘_(C) (g ∘_(C) (f ∘_(C) (𝟙_(C) W))) ))
  = ((i ∘_(C)  h) ∘_(C) ((𝟙_(C) Y) ∘_(C) g)) ∘_(C) (f) := by cat


-- obtaining a morphism from an equality
def Map (C : category) {X : C.Obj} {Y : C.Obj} (p : X = Y) : C.Hom X Y := by
subst p
exact 𝟙_(C) X


notation "Map_(" C ")" p => Map C p



-- definition of an isomorphism from X to Y
structure isomorphism (C : category) (X : C.Obj) (Y : C.Obj) where
  Fst : C.Hom X Y
  Snd : C.Hom Y X
  Id₁ : (C.Cmp X Y X Fst Snd) = C.Idn X
  Id₂ : (C.Cmp Y X Y Snd Fst) = C.Idn Y


-- notation for isomorphisms from X to Y (≅)
notation X "≅_(" C ")" Y => isomorphism C X Y


-- defining the inverse of an isomorphism between objects X and Y
def inverse {C : category} {X : C.Obj} {Y : C.Obj} (f : X ≅_(C) Y) : Y ≅_(C) X := {Fst := f.Snd, Snd := f.Fst, Id₁ := f.Id₂, Id₂ := f.Id₁}


-- notation for inverse : isos from X to Y to isos from Y to X
notation f "⁻¹" => inverse f


def SetObj := Type

def SetHom (X : SetObj) (Y : SetObj) : Type := X → Y

def SetIdn (X : SetObj) : (SetHom X X) := λ (x : X) => x


def SetCmp (X : SetObj) (Y : SetObj) (Z : SetObj) (f : SetHom X Y) (g : SetHom Y Z) : SetHom X Z := λ (x : X) => (g (f x))


def SetId₁ (X : SetObj) (Y : SetObj) (f : SetHom X Y) : (SetCmp X Y Y f (SetIdn Y)) = f := funext (λ _ => rfl)

def SetId₂ (X : SetObj) (Y : SetObj) (f : SetHom X Y) : (SetCmp X X Y (SetIdn X) f) = f := rfl

def SetAss (W : SetObj) (X : SetObj) (Y : SetObj) (Z : SetObj) (f : SetHom W X) (g : SetHom X Y) (h : SetHom Y Z) : (SetCmp W X Z f (SetCmp X Y Z g h)) = (SetCmp W Y Z (SetCmp W X Y f g) h) := funext (λ _ => rfl)


def Set : category := {Obj := SetObj, Hom := SetHom, Idn := SetIdn, Cmp := SetCmp, Id₁ := SetId₁, Id₂ := SetId₂, Ass := SetAss}


-- 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)


def FunRfl (C : category) (D : category) (F : functor C D) : F = {Obj := F.Obj, Hom := F.Hom, Idn := F.Idn, Cmp := F.Cmp} := by
rfl

-- def FunOut (C : category) (D : category )

-- definition of the identity functor on objects
def CatIdnObj (C : category) :=
fun(X : C.Obj)=>
X

-- definition of the identity functor on morphisms
def CatIdnMor (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
f

-- proving the identity law for the identity functor
def CatIdnIdn (C : category) :=
fun(X : C.Obj)=>
Eq.refl (C.Idn X)

-- proving the compositionality law for the identity functor
def CatIdnCmp (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
Eq.refl (C.Cmp X Y Z f g)


-- defining the identity functor
def CatIdn (C : category) : functor C C :=
{Obj := CatIdnObj C, Hom := CatIdnMor C, Idn := CatIdnIdn C, Cmp := CatIdnCmp C}


-- defining the composition G ∘_(Cat) F on objects
def CatCmpObj (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
(G.Obj (F.Obj X))

-- defining the composition G ∘_(Cat) F on morphisms
def CatCmpHom (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
(G.Hom) (F.Obj X) (F.Obj Y) (F.Hom X Y f)


-- proving the identity law for the composition G ∘_(Cat) F
def CatCmpIdn (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
Eq.trans (congrArg (G.Hom (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))


-- proving the compositionality law for the composition G ∘_(Cat) F
def CatCmpCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
((Eq.trans)
(G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Hom X Y f) (F.Hom Y Z g))
(congrArg (G.Hom  (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))


-- defining the composition in the category Cat
def CatCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) : functor C E :=
{Obj := CatCmpObj C D E F G, Hom := CatCmpHom C D E F G,Idn := CatCmpIdn C D E F G, Cmp := CatCmpCmp C D E F G}


-- proving Cat.Id₁
def CatId₁ (C : category) (D : category) (F : functor C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F

-- Proof of Cat.Id₂
def CatId₂ (C : category) (D : category) (F : functor C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F

-- Proof of Cat.Ass
def CatAss (B : category) (C : category) (D : category) (E : category) (F : functor B C) (G : functor C D) (H : functor D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) :=
Eq.refl (CatCmp B C E F (CatCmp C D E G H))


-- The category of categories

universe u
universe v

def Cat : category := {Obj := category.{u, v}, Hom := functor, Idn := CatIdn, Cmp := CatCmp, Id₁:= CatId₁, Id₂:= CatId₂, Ass := CatAss}

-- def equal {A : Type u} {B }
def MorCatObj (C : Cat.Obj) (D : Cat.Obj) (p : D.Obj = C.Obj) (X : C.Obj) : D.Obj := by
rw [p]
exact X
sorry

def MorCatHom (C : Cat.Obj) (D : Cat.Obj) (p : D.Obj = C.Obj) (X : C.Obj) (Y : C.Obj) (f : C.Hom X Y) : D.Hom (MorCatObj C D p X) (MorCatObj C D p Y) := by
sorry

-- def MorCatIdn (C : Cat.Obj) (D : Cat.Obj) (X : C)

-- def MorCatCmp

def CatRfl (C : Cat.Obj) : C = {Obj := C.Obj, Hom := C.Hom, Idn := C.Idn, Cmp := C.Cmp, Id₁ := C.Id₁, Id₂ := C.Id₂, Ass := C.Ass} := by
rfl


def CatExt (C : Cat.Obj)
          (D : Cat.Obj)
          (p₁ : D.Obj = C.Obj)
          (X : C.Obj)
          (Y : C.Obj)
          (p₂ : C.Hom X Y = D.Hom (MorCatObj C D p₁ X) (MorCatObj C D p₁ Y))
          (X₁ : C.Obj)
          (X₂ : C.Obj)
          (X₃ : C.Obj)
          (f₁ : C.Hom X₁ X₂)
          (f₂ : C.Hom X₂ X₃)
          (p₃ : (MorCatHom C D p₁ X₁ X₃ (C.Cmp X₁ X₂ X₃ f₁ f₂)) = D.Cmp (MorCatObj C D p₁ X₁) (MorCatObj C D p₁ X₂) (MorCatObj C D p₁ X₃) (MorCatHom C D p₁ X₁ X₂ f₁) (MorCatHom C D p₁ X₂ X₃ f₂)) : C = D := by
rw [CatRfl C]
rw [CatRfl D]
simp
sorry

[Notification Bot]

A message was moved here from #mathlib4 > shortcut for Seminorm.instMulAction? by Kyle Miller.

[Dean Young]

Sorry for not tagging the question correctly

[Scott Morrison]

That statement is clearly false. Your p₂ and p₃ arguments need to be foralls.

[Dean Young]

I changed it to a structure, "equal categories":

-- def equal {A : Type u} {B }
def 𝕆𝕓𝕛 (C : Cat.Obj) (D : Cat.Obj) (obj : D.Obj = C.Obj) (X : C.Obj) : D.Obj := by
rw [obj]
exact X

-- def equal {A : Type u} {B }
def ℍ𝕠𝕞 (C : Cat.Obj) (D : Cat.Obj) (obj : D.Obj = C.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]
sorry

#check category.mk

structure equal_categories where
  Fst : Cat.Obj
  Snd : Cat.Obj
  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
  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)

[Scott Morrison]

Could you #xy a bit? This is not really a sensible thing to be trying to do.

[Dean Young]

I need this extensionality result for the categories to be able to show that two categories are equal. So it's my main goal right now (as well as an extensionality result for functors), but... it's come up whenever I have a structure with dependent types in it.

In general I want something like a = b → f a = f b for dependent f,i.e. f x might not be the same type as f y for x, y : X, and yet f a does have the same type as f b when a = b, and f a = f b should somehow be able to be expressed and proven. That may be a critical feature of equality for me.

[Dean Young]

So, if I had such a feature I think I could prove category.mk C.Obj = category.mk D.Obj, then categorylmk C.Obj C.Hom = category.mk D.Obj D.Hom

[Scott Morrison]

Categories aren't equal. They are rarely even isomorphic. Usually they are only equivalent. Ignoring this is in invitation to suffering in dependent type theory hell. :-)

[Scott Morrison]

Similarly, functors are rarely equal. Have a look in Mathlib how we handle this --- we have an extensionality theorem for functors, but use it exceptionally rarely.

[Scott Morrison]

Even if you do the dependent type theory suffering, you only prove a result that encourages you to do more things "the wrong way".

[Dean Young]

Ok, I'll take your advice.

Categories | Equivalence
Functors | Isomorphism
Natural transformations | Equality

[Dean Young]

How does Lean handle extensionality of natural transformations?

[Scott Morrison]

Do you mean Mathilb? See docs#CategoryTheory.NatTrans.ext

[Dean Young]

Take a look at this structure:

structure foo where
   X : foo
  Y : foo
  k : X = Y

I want to fill in the sorry here:

def A (a : foo) (b : foo) (p : a.X =  b.X) (q : a.Y = b.Y) : a = b := by
sorry

When I try a rewrite tactic it says "motive is not type correct".

In general I still need a way of proving R : x = y → A x = A y for dependent A. Right now I have several such situations where the extensionality feature is hard to get because of dependent A. Is there a name for R?

[Adam Topaz]

your foo doesn't compile

[Dean Young]

Oops let's do this then:

structure foo where
  X : Type
  Y : Type
  k : X = Y

def A (a : foo) (b : foo) (p : a.X =  b.X) (q : a.Y = b.Y) : a = b := by
sorry

[Adam Topaz]

Just so you know, equality of types is evil. But in any case, here's a proof:

structure foo where
  X : Type
  Y : Type
  k : X = Y

def A (a : foo) (b : foo) (p : a.X = b.X) (q : a.Y = b.Y) : a = b := by
  cases a
  cases b
  congr

[Matthew Ballard]

Tag it with @[ext]

[Adam Topaz]

yep, that would work as well.

[Dean Young]

Thanks those worked well for my natural transformation extensionality.

[Adam Topaz]

If you're going through all this as an exercise, then that's great. But it's worthwhile to mention that mathlib4 has a very extensive category theory library. If you want to use category theory for something, it's probably better to learn how to use that part of the library instead of reinventing the wheel.