/-
See main example and other example below for my thoughts on "smart composition" (perhaps in a strict 2-category). Email edeany@linearlibrary.net for more complex suggestions.
-/

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


/-
Defining the category of categories
-/

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

def Idn {C : category} (X : C.Obj) := C.Idn X
notation "𝟙" X => Idn X

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

def Cmp {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 "∘" f => Cmp f g


-- 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.Idn 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


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


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


/-
Defining the product of categories
-/

-- defining the objects of the PrdCatObj C D
def PrdCatObjObj (C : category) (D : category) := (D.Obj) × (C.Obj)

-- defining the morphisms of PrdCatObj C D
def PrdCatObjHom (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) := (D.Hom X.1 Y.1) × (C.Hom X.2 Y.2)

-- defining the identity functor on an object in C × D
def PrdCatObjIdn (C : category) (D : category) (X : PrdCatObjObj C D) := ((D.Idn X.1),(C.Idn X.2))

-- defining the composition on morphisms in C × D
def PrdCatObjCmp (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) (Z : PrdCatObjObj C D) (f : PrdCatObjHom C D X Y) (g : PrdCatObjHom C D Y Z) : PrdCatObjHom C D X Z := (D.Cmp X.1 Y.1 Z.1 f.1 g.1, C.Cmp X.2 Y.2 Z.2 f.2 g.2)


-- proving the first identity law for morphisms in C ×_Cat D 
theorem PrdCatObjId₁ (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) (f : PrdCatObjHom C D X Y) :
  PrdCatObjCmp C D X Y Y f (PrdCatObjIdn C D Y) = f := sorry

-- proving the second identity law for morphisms in C ×_Cat D 
theorem PrdCatObjId₂ (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) (f : PrdCatObjHom C D X Y) : PrdCatObjCmp C D X X Y (PrdCatObjIdn C D X) f = f := sorry

-- proving associativity for morphisms in C ×_Cat D
theorem PrdCatObjAss 
  (C : category) (D : category)
  (W : PrdCatObjObj C D) (X : PrdCatObjObj C D) 
  (Y : PrdCatObjObj C D) (Z : PrdCatObjObj C D)
  (f : PrdCatObjHom C D W X) (g : PrdCatObjHom C D X Y) (h : PrdCatObjHom C D Y Z) :
  PrdCatObjCmp C D W X Z f (PrdCatObjCmp C D X Y Z g h) = PrdCatObjCmp C D W Y Z (PrdCatObjCmp C D W X Y f g) h := sorry


-- defining the PrdCatObj of two categories
def PrdCatObj (C : category) (D : category) : category := {Obj := PrdCatObjObj C D, Hom := PrdCatObjHom C D, Idn := PrdCatObjIdn C D, Cmp := PrdCatObjCmp C D, Id₁ := PrdCatObjId₁ C D, Id₂:= PrdCatObjId₂ C D, Ass := PrdCatObjAss C D}


notation:1000  D "×_Cat" C => PrdCatObj C D

/-
Defining the functor category
-/

-- defining natural transformations for a category C and a category D
structure HomCatObjHom (C : category) (D : category) (F : functor C D) (G : functor C D) where
  Obj : (X : C.Obj) → (D.Hom (F.Obj X) (G.Obj X))
  Nat : (X : C.Obj) → (Y : C.Obj) → (f : C.Hom X Y) → (D.Cmp (F.Obj X) (F.Obj Y) (G.Obj Y) (F.Hom X Y f) (Obj Y)) = (D.Cmp (F.Obj X) (G.Obj X) (G.Obj Y) (Obj X) (G.Hom X Y f))


-- notation for natural transformations
def natural_transformation {C : category} {D : category} (F : functor C D) (G : functor C D) := HomCatObjHom C D F G


-- defining (C →_Cat D).Idn.Obj, the identity natural transformation of a functor on objects 
def HomCatObjIdnObj (C : category) (D : category) (F : functor C D) (X : C.Obj) : (D.Hom (F.Obj X) (F.Obj X)) := D.Idn (F.Obj X)


-- helping to prove the naturality of the identity functor
def HomCatObjIdnNat₁ (C : category) (D : category) (F : functor C D) (X : C.Obj) (Y : C.Obj) (f : C.Hom X Y) : (D.Cmp (F.Obj X) (F.Obj Y) (F.Obj Y) (F.Hom X Y f) (HomCatObjIdnObj C D F Y)) = F.Hom X Y f := D.Id₁ (functor.Obj F X) (functor.Obj F Y) (functor.Hom F X Y f)

-- starting to prove the naturality of the identity functor
def HomCatObjIdnNat₂ (C : category) (D : category) (F : functor C D) (X : C.Obj) (Y : C.Obj) (f : C.Hom X Y) : (D.Cmp (F.Obj X) (F.Obj X) (F.Obj Y) (HomCatObjIdnObj C D F X) (F.Hom X Y f)) = F.Hom X Y f := D.Id₂ (functor.Obj F X) (functor.Obj F Y) (functor.Hom F X Y f)

-- proving the naturality of the identity functor, (C →_Cat D).Idn.Nat
def HomCatObjIdnNat (C : category) (D : category) (F : functor C D) (X : C.Obj) (Y : C.Obj) (f : C.Hom X Y) : (D.Cmp (F.Obj X) (F.Obj Y) (F.Obj Y) (F.Hom X Y f) (HomCatObjIdnObj C D F Y)) = (D.Cmp (F.Obj X) (F.Obj X) (F.Obj Y) (HomCatObjIdnObj C D F X) (F.Hom X Y f)) := Eq.trans (HomCatObjIdnNat₁ C D F X Y f) (Eq.symm (HomCatObjIdnNat₂ C D F X Y f))


-- defining (C →_Cat D).Idn for a category C and a category D
def HomCatObjIdn (C : category) (D : category) (F : functor C D) : HomCatObjHom C D F F := {Obj := HomCatObjIdnObj C D F, Nat := HomCatObjIdnNat C D F}


-- defining composition of natural transformations
def HomCatObjCmpObj (C : category) (D : category) (F : functor C D) (G : functor C D) (H : functor C D) (f : HomCatObjHom C D F G) (g : HomCatObjHom C D G H) (X : C.Obj) :  D.Hom (F.Obj X) (H.Obj X) := (g.Obj X) ∘_(D) (f.Obj X)

-- defining composition of natural transformations
def HomCatObjCmpNat (C : category) (D : category) (F : functor C D) (G : functor C D) (H : functor C D) (f : HomCatObjHom C D F G) (g : HomCatObjHom C D G H) (X : C.Obj) (Y : C.Obj) (α : C.Hom X Y) : (((g.Obj Y) ∘_(D) (f.Obj Y)) ∘_(D) (F.Hom X Y α))  = ((H.Hom X Y α) ∘_(D) ((g.Obj X) ∘_(D) (f.Obj X)))  := sorry

-- defining composition of natural transformations
def HomCatObjCmp (C : category) (D : category) (F : functor C D) (G : functor C D) (H : functor C D) (f : HomCatObjHom C D F G) (g : HomCatObjHom C D G H) : HomCatObjHom C D F H := {Obj := HomCatObjCmpObj C D F G H f g, Nat := HomCatObjCmpNat C D F G H f g}


-- proving the identity laws and associativity for the category C →_Cat D

-- proving the first identity law of the functor category C →_Cat D
def HomCatObjId₁ (C : category) (D : category) (F : functor C D) (G : functor C D) (f : HomCatObjHom C D F G) : HomCatObjCmp C D F G G f (HomCatObjIdn C D G) = f := sorry

-- proving the second identity law of the functor category C →_Cat D
def HomCatObjId₂ (C : category) (D : category) (F : functor C D) (G : functor C D) (f : HomCatObjHom C D F G) : HomCatObjCmp C D F F G (HomCatObjIdn C D F) f = f := sorry

-- proving associativity of the functor category C →_Cat D
def HomCatObjAss (C : category) (D : category) (F : functor C D) (G : functor C D) (H : functor C D) (I : functor C D) (α : HomCatObjHom C D F G) (β : HomCatObjHom C D G H) (γ : HomCatObjHom C D H I) : (HomCatObjCmp C D F G I α (HomCatObjCmp C D G H I β γ)) = (HomCatObjCmp C D F H I (HomCatObjCmp C D F G H α β) γ) := sorry


-- defining the category C →_Cat D for a category C and a category D
def HomCatObj (C : category) (D : category) : category := {Obj := functor C D, Hom := HomCatObjHom C D, Idn := HomCatObjIdn C D, Cmp := HomCatObjCmp C D, Id₁ := HomCatObjId₁ C D, Id₂ := HomCatObjId₂ C D, Ass := HomCatObjAss C D}


-- notation for the functor HomCatObj C D
notation C "→_Cat" D => (HomCatObj C D)





-- defining 𝟭
def categoriesIdn (C : category) : (C →_Cat C).Obj := Cat.Idn C

notation "𝟭_Cat" C => categoriesIdn C


-- defining • on objects
def categoriesCmpObj (C : category) (D : category) (E : category) (P : ((C →_Cat D) ×_Cat (D →_Cat E)).Obj) : (C →_Cat E).Obj := P.2 ∘_(Cat) P.1

-- defining • on morphisms
def categoriesCmpHom (C : category) (D : category) (E : category) (P₁ : ((C →_Cat D) ×_Cat (D →_Cat E)).Obj) (P₂ : ((C →_Cat D) ×_Cat (D →_Cat E)).Obj) (f : ((C →_Cat D) ×_Cat (D →_Cat E)).Hom P₁ P₂) : (C →_Cat E).Hom (categoriesCmpObj C D E P₁) (categoriesCmpObj C D E P₂) := sorry

-- proving the identity law for •
def categoriesCmpIdn (C : category) (D : category) (E : category) (P : ((C →_Cat D) ×_Cat (D →_Cat E)).Obj) : (categoriesCmpHom C D E P P (𝟙_((C →_Cat D) ×_Cat (D →_Cat E)) P))= (𝟙_(C →_Cat E) (categoriesCmpObj C D E P))  := sorry

-- proving the compositionality law for •
def categoriesCmpCmp (C : category) (D : category) (E : category) (X : ((C →_Cat D) ×_Cat (D →_Cat E)).Obj) (Y : ((C →_Cat D) ×_Cat (D →_Cat E)).Obj) (Z : ((C →_Cat D) ×_Cat (D →_Cat E)).Obj) (f : ((C →_Cat D) ×_Cat (D →_Cat E)).Hom X Y) (g : ((C →_Cat D) ×_Cat (D →_Cat E)).Hom Y Z) : ((C →_Cat E)).Cmp (categoriesCmpObj C D E X) (categoriesCmpObj C D E Y) (categoriesCmpObj C D E Z) (categoriesCmpHom C D E X Y f) (categoriesCmpHom C D E Y Z g) = categoriesCmpHom C D E X Z (((C →_Cat D) ×_Cat (D →_Cat E)).Cmp X Y Z f g)
 := sorry

-- assembling the functor •
def categoriesCmp (C : category) (D : category) (E : category) : functor ((C →_Cat D) ×_Cat (D →_Cat E)) (C →_Cat E) := {Obj := categoriesCmpObj C D E, Hom := categoriesCmpHom C D E, Idn := categoriesCmpIdn C D E, Cmp := categoriesCmpCmp C D E}


def horizontal_composition {C : category.{u,v}} {D : category.{u,v}} {E : category.{u,v}} {F₁ : (C →_Cat D).Obj} {F₂ : (C →_Cat D).Obj} {G₁ : (D →_Cat E).Obj} {G₂ : (D →_Cat E).Obj} (η : (C →_Cat D).Hom F₁ F₂) (ε : (D →_Cat E).Hom G₁ G₂) : (C →_Cat E).Hom (G₁ ∘_(Cat) F₁) (G₂ ∘_(Cat) F₂) := sorry -- (categoriesCmp C D E).Hom (η, ε)
notation : 1000 η "•_Cat" ε => horizontal_composition η ε


/-
MAIN EXAMPLE
-/


variable {D₁ : category}
variable {D₂ : category}
variable {D₃ : category}
variable {D₄ : category}
variable {F : functor D₁ D₄}
variable {G₁ : functor D₁ D₂}
variable {G₂ : functor D₂ D₃}
variable {G₃ : functor D₃ D₄}
variable {H : functor D₁ D₄}
def Gfst : functor D₁ D₄ := (((G₃) ∘_(Cat) (G₂)) ∘_(Cat) (G₁)) ∘_(Cat) (𝟙_(Cat) D₁)
def Gsnd : functor D₁ D₄ := (G₃) ∘_(Cat) (((G₂) ∘_(Cat)  (𝟙_(Cat) D₂)) ∘_(Cat) (G₁))
variable {η : (D₁ →_Cat D₄).Hom F Gfst}
variable {ε : (D₁ →_Cat D₄).Hom Gsnd H}

def φ : (D₁ →_Cat D₄).Hom F H := ε ∘_Cat η

/-
Right now this gives an error, but it would be nice to design something which could infer the equality between Gfst and Gand on its own. The algorithm is pretty clear: eliminate all identity maps and right associate both sides, then attempt a reflexivity. 
-/

/-
OTHER EXAMPLE
-/

-- definition of the right triangle identity
def AdjId₁ (C : category) (D : category) (F : (C →_Cat D).Obj) (G : (D →_Cat C).Obj) (unit : (C →_Cat C).Hom (𝟙_Cat C) (G ∘_Cat F)) ( counit : (D →_Cat D).Hom (F ∘_Cat G) (𝟙_Cat D) ) : Prop := sorry


-- definition of the left triangle identity
def AdjId₂ (C : category) (D : category) (F : (C →_Cat D).Obj) (G : (D →_Cat C).Obj) (unit : (C →_Cat C).Hom (𝟙_Cat C) (G ∘_Cat F)) ( counit : (D →_Cat D).Hom (F ∘_Cat G) (𝟙_Cat D) ) : Prop := sorry


-- definition of an adjunction
structure adjunction where
  Dom : category
  Cod : category
  F  : (Dom →_Cat Cod).Obj
  G  : (Cod →_Cat Dom).Obj
  η : (Dom →_Cat Dom).Hom (𝟙_Cat Dom) (G ∘_Cat F)
  ε : (Cod →_Cat Cod).Hom (F ∘_Cat G) (𝟙_Cat Cod) 
  Id₁ : AdjId₁ Dom Cod F G η ε -- here is where the smart composition would go
  Id₂ : AdjId₂ Dom Cod F G η ε -- here too

/-
In this example, it would be good if ∘_Cat "just worked" without any need for the "Map" function, which inserts morphisms in-between two morphisms.
-/