Adjunction.lean

import Mathlib.tactic
import Mathlib.CategoryTheory.Functor.Currying
import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
import Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

open CategoryTheory
open Limits

/----------- /
/ 普遍射の定義 /
/ -----------/

def isUnivArrTo [Category C] [Category D] {S : D ⥤ C} {c : C} {r : D} (u : c ⟶ S.obj r) :=
  IsInitial (StructuredArrow.mk u)

def isUnivArrTo.to' [Category C] [Category D] {S : D ⥤ C} {c : C} {r : D} {u : c ⟶ S.obj r}
  (H : isUnivArrTo u) {r' : D} (u' : c ⟶ S.obj r') : r ⟶ r'
:= (H.to (StructuredArrow.mk u')).right

@[simp]
def isUnivArrTo.w' [Category C] [Category D] {S : D ⥤ C} {c : C} {r : D} {u : c ⟶ S.obj r}
   (H : isUnivArrTo u) {r' : D} (u' : c ⟶ S.obj r') : u' = u ≫ S.map (H.to' u')
:= by
  let E := (H.to (StructuredArrow.mk u')).w
  simp at E
  simp [isUnivArrTo.to']; rw [<- E]

def isUnivArrFrom [Category C] [Category D] {S : D ⥤ C} {c : C} {r : D} (u : S.obj r ⟶ c)  :=
  IsTerminal (CostructuredArrow.mk u)

def isUnivArrFrom.from' [Category C] [Category D] {S : D ⥤ C} {c : C} {r : D} {u : S.obj r ⟶ c}
  (H : isUnivArrFrom u) {r' : D} (u' : S.obj r' ⟶ c) : r' ⟶ r
:= (H.from (CostructuredArrow.mk u')).left

@[simp]
def isUnivArrFrom.w' [Category C] [Category D] {S : D ⥤ C} {c : C} {r : D} {u : S.obj r ⟶ c}
   (H : isUnivArrFrom u) {r' : D} (u' : S.obj r' ⟶ c) : S.map (H.from' u') ≫ u = u'
:= by
  let E := (H.from (CostructuredArrow.mk u')).w
  simp at E
  simp [isUnivArrFrom.from']; rw [E]


/-------------------------------- /
/ 随伴の定義1 : a x の両者について自然 /
/ --------------------------------/
structure AdjNat [Category X] [Category A] (F : X ⥤ A) (G : A ⥤ X) where
  -- A(F(x), -) ≅ X(x, G(-))
  naturality1 (x : X) :
    (curry.obj (F.op.prod (Functor.id A) ⋙ Functor.hom A)).obj (Opposite.op x) ≅
    (curry.obj ((Functor.id Xᵒᵖ).prod G ⋙ Functor.hom X)).obj (Opposite.op x)
  -- A(F(-), a) ≅ X(-, G(a))
  naturality2 (a : A) :
    (curry.obj ((F.op.prod (Functor.id A)) ⋙ Functor.hom A)).flip.obj a ≅
    (curry.obj (((Functor.id Xᵒᵖ).prod G) ⋙ Functor.hom X)).flip.obj a
  eq x a f :
    (naturality1 x).hom.app a f = (naturality2 a).hom.app (Opposite.op x) f

def AdjNat.iso1 [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (σ : AdjNat F G) (x : X) (a : A) :
  (F.obj x ⟶ a) ≅ (x ⟶ G.obj a)
:= {
  hom := λ f => (σ.naturality1 x).hom.app a f
  inv := λ g => (σ.naturality1 x).inv.app a g
  hom_inv_id := by ext f; simp
  inv_hom_id := by ext g; simp
}

def AdjNat.iso2 [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (σ : AdjNat F G) (x : X) (a : A) :
  (F.obj x ⟶ a) ≅ (x ⟶ G.obj a)
:= {
  hom := λ f => (σ.naturality2 a).hom.app (Opposite.op x) f
  inv := λ g => (σ.naturality2 a).inv.app (Opposite.op x) g
  hom_inv_id := by ext f; simp
  inv_hom_id := by ext g; simp
}

lemma AdjNat.iso_eq [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (σ : AdjNat F G) (x : X) (a : A) :
  AdjNat.iso1 σ x a = AdjNat.iso2 σ x a
:= by
  ext f; simp [AdjNat.iso1, AdjNat.iso2]
  exact σ.eq x a f

/------------------------------ /
/ 随伴の定義2 : 射による自然性の記述 /
/ ------------------------------/
structure AdjHom [Category X] [Category A] (F : X ⥤ A) (G : A ⥤ X) where
  iso x a : (F.obj x ⟶ a) ≅ (x ⟶ G.obj a)
  -- φ_{x a'}(f ≫ k) = φ_{x,a}(f) ≫ G(k)
  naturality1 (x : X) (a a' : A) (f : F.obj x ⟶ a) (k : a ⟶ a') :
    (iso x a').hom (f ≫ k) = (iso x a).hom f ≫ G.map k
  -- φ_{x' a}(F(h) ≫ f) = h ≫ φ_{x,a}(f)
  naturality2 (x x' : X) (a : A) (f : F.obj x ⟶ a) (h : x' ⟶ x) :
    (iso x' a).hom (F.map h ≫ f) = h ≫ (iso x a).hom f


structure AdjInv [Category X] [Category A] (F : X ⥤ A) (G : A ⥤ X) where
  iso x a : (F.obj x ⟶ a) ≅ (x ⟶ G.obj a)
  -- φ⁻¹_{x', a}(g ≫ G(k)) = φ⁻¹_{x,a}(g) ≫ k
  naturality1 (x : X) (a a' : A)  (g : x ⟶ G.obj a) (k : a ⟶ a') :
    (iso x a').inv (g ≫ G.map k) = (iso x a).inv g ≫ k
  -- φ⁻¹_{x, a}(h ≫ g) = F(h) ≫ φ⁻¹_{x',a}(g)
  naturality2 (x x' : X) (a : A) (h : x' ⟶ x) (g : x ⟶ G.obj a) :
    (iso x' a).inv (h ≫ g) = F.map h ≫ (iso x a).inv g



/------------- /
/ 各定義の同値性 /
/ -------------/

def AdjHom.AdjInv [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (φ : AdjHom F G) :
  AdjInv F G
:= {
  iso := φ.iso
  naturality1 := by
    intro x a a' g k
    have E := φ.naturality1 x a a' ((φ.iso x a).inv g) k
    simp at E
    rw [<- E]; simp
  naturality2 := by
    intro x x' a h g
    have E := φ.naturality2 x x' a ((φ.iso x a).inv g) h
    simp at E
    rw [<- E]; simp
}

def AdjInv.AdjHom [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (φ : AdjInv F G) :
  AdjHom F G
:= {
  iso := φ.iso
  naturality1 := by
    intro x a a' f k
    have E := φ.naturality1 x a a' ((φ.iso x a).hom f) k
    simp at E
    rw [<- E]; simp
  naturality2 := by
    intro x x' a f h
    have E := φ.naturality2 x x' a h ((φ.iso x a).hom f)
    simp at E
    rw [<- E]; simp
}

def AdjNat.AdjHom [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (σ : AdjNat F G) :
  AdjHom F G
:= {
  iso := σ.iso1
  naturality1 := by
    intro x a a' f k
    have E := (σ.naturality1 x).hom.naturality k
    simp [Functor.hom] at E
    have := congr_fun E f; simp at this
    simp [AdjNat.iso1]
    rw [this]
  naturality2 := by
    intro x x' a f h
    have E := (σ.naturality2 a).hom.naturality h.op
    simp [Functor.hom] at E
    have := congr_fun E f; simp at this
    rw [iso_eq, iso_eq]; simp [AdjNat.iso2]
    rw [this]
}

def AdjHom.AdjNat [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (φ : AdjHom F G) :
  AdjNat F G
:= {
  naturality1 x := {
    hom := {
      app a := (φ.iso x a).hom
      naturality := by
        intro a a' k; simp [Functor.hom]
        ext f; simp
        exact φ.naturality1 x a a' f k
    }
    inv := {
      app a := (φ.iso x a).inv
      naturality := by
        intro a a' k; simp [Functor.hom]
        ext g; simp
        have E := φ.naturality1 x a a' ((φ.iso x a).inv g) k
        simp at E
        rw [<- E]; simp
    }
  }
  naturality2 a := {
    hom := {
      app x := (φ.iso x.unop a).hom
      naturality := by
        intro x x' k; simp [Functor.hom]
        ext f; simp
        exact φ.naturality2 x.unop x'.unop a f k.unop

    }
    inv := {
      app x := (φ.iso x.unop a).inv
      naturality := by
        intro x x' k; simp [Functor.hom]
        ext g; simp
        have E := φ.naturality2 x.unop x'.unop a ((φ.iso _ _).inv g) k.unop
        simp at E
        rw [<- E]; simp
    }
  }
  eq x a f := by simp
}

abbrev Adj [Category X] [Category A] (F : X ⥤ A) (G : A ⥤ X) := AdjHom F G

/---------------- /
/ 単位・余単位の定義 /
/ ----------------/

def Adj.unit [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (σ : Adj F G) :
  (Functor.id X) ⟶ (F ⋙ G)
:= {
  app x := (σ.iso x (F.obj x)).hom (𝟙 (F.obj x))
  naturality x x' f := by
    simp
    have E := σ.naturality2 x' x (F.obj x') (𝟙 _) f
    rw [<- E]; clear E; simp
    have E := σ.naturality1 x (F.obj x) (F.obj x') (𝟙 _) (F.map f)
    simp at E
    rw [E]
}

def Adj.counit [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (σ : Adj F G) :
  (G ⋙ F) ⟶ (Functor.id A)
:= {
  app a := (σ.iso (G.obj a) a).inv (𝟙 (G.obj a))
  naturality a a' f := by
    simp
    have E := σ.AdjInv.naturality1 (G.obj a) a a' (𝟙 _) f
    simp [AdjHom.AdjInv] at E
    have E' := σ.AdjInv.naturality2 (G.obj a') (G.obj a) a' (G.map f) (𝟙 _)
    simp [AdjHom.AdjInv] at E'
    rw [<- E', <- E]
}

lemma Adj.hom_eq_unit_map [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (σ : Adj F G) (x : X) (a : A) (f : F.obj x ⟶ a) :
  -- σ(f) = μₓ ≫ G(f)
  (σ.iso x a).hom f = σ.unit.app x ≫ G.map f
:= by
  simp [Adj.unit]
  have E := σ.naturality1 x (F.obj x) a (𝟙 _) f; simp at E
  rw [E]


lemma Adj.inv_eq_map_counit [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (σ : Adj F G) (x : X) (a : A) (g : x ⟶ G.obj a) :
  -- σ⁻¹(g) = F(g) ≫ εₐ
  (σ.iso x a).inv g = F.map g ≫ σ.counit.app a
:= by
  have E := σ.AdjInv.naturality2 (G.obj a) x a g (𝟙 _)
  simp [AdjHom.AdjInv] at E
  simp [Adj.counit]; rw [<- E]

lemma Adj.triangle1 [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X}  (σ : Adj F G) :
  -- G ⟶ G ⋙ F ≫ G ⟶ G
  -- Gμ ≫ εG = 𝟙 G
  whiskerLeft G σ.unit ≫ whiskerRight σ.counit G = 𝟙 G
:= by
  ext a; simp
  have E := (σ.hom_eq_unit_map (f := σ.counit.app a)); simp at E
  rw [<- E]
  simp [Adj.counit]


lemma Adj.triangle2 [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X}  (σ : Adj F G) :
  -- F ⟶ F ⋙ G ⋙ F ⟶ F
  -- μF ≫ Fε = 𝟙 F
  whiskerRight σ.unit F ≫  whiskerLeft F σ.counit = 𝟙 F
:= by
  ext x; simp
  have E := σ.inv_eq_map_counit (g := σ.unit.app x)
  rw [<- E]
  simp [Adj.unit]


/------------------ /
/ 単位・余単位の普遍性 /
/ -----------------/

def Adj.unit_isUnivArr [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X}  (σ : Adj F G) (x : X) :
  isUnivArrTo (S := G) (σ.unit.app x)
:= by
  unfold isUnivArrTo
  apply IsInitial.ofUniqueHom ?_ ?_
  · intro Y; simp at Y
    refine ⟨𝟙 _, (σ.iso x Y.right).inv Y.hom, ?_⟩
    simp
    rw [<- hom_eq_unit_map]; simp
  · intro Y m
    ext; simp
    have E := m.w
    simp at E
    rw [E]; clear E
    rw [<- hom_eq_unit_map]; simp


def Adj.counit_isUnivArr [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X} (σ : Adj F G) (a : A) :
  isUnivArrFrom (S := F) (σ.counit.app a)
:= by
  unfold isUnivArrFrom
  apply IsTerminal.ofUniqueHom ?_ ?_
  · intro Y
    refine ⟨(σ.iso Y.left a).hom Y.hom, 𝟙 _, ?_⟩
    simp
    rw [<- inv_eq_map_counit]; simp
  · intro Y m
    ext; simp
    have E := m.w
    simp at E
    conv at E => arg 1; arg 2; change σ.counit.app a
    rw [<- E]; clear E
    rw [<- inv_eq_map_counit]; simp


/------------------------ /
/ 単位/余単位による随伴の構成 /
/ ------------------------/

-- 普遍をなすunitによる構成
def Adj.mkby_NatUnivArrTo
  [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X}
  (μ : Functor.id X ⟶ F ⋙ G) (H : ∀ x, isUnivArrTo (S := G) (μ.app x)) :
  Adj F G
:= {
  iso x a := by
    have Hx := H x
    refine {
      hom f := μ.app x ≫ G.map f
      inv g := (Hx.to (StructuredArrow.mk g)).right
      hom_inv_id := by
        ext f; simp
        set g := Hx.to (StructuredArrow.mk (μ.app x ≫ G.map f))
        have E := Hx.hom_ext g ⟨𝟙 _, f, by simp⟩
        rw [E]
      inv_hom_id := by
        ext g; simp
        set f := (IsInitial.to Hx (StructuredArrow.mk g))
        have Hf := f.w; simp at Hf
        rw [<- Hf]
    }
  naturality1 x a a' f k := by simp
  naturality2 x x' a f h := by
    simp
    have E := μ.naturality h; simp at E
    rw [<- Category.assoc, <- E, Category.assoc]
}


-- 普遍射をなすcounitによる構成
def Adj.mkby_NatUnivArrFrom
  [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X}
  (ε : G ⋙ F ⟶ Functor.id A) (H : ∀ a, isUnivArrFrom (S := F) (ε.app a)) :
  Adj F G
:= by
  apply AdjInv.AdjHom
  refine {
    iso x a := {
      hom f := ((H a).from (CostructuredArrow.mk f)).left
      inv g := F.map g ≫ ε.app a
      inv_hom_id := by
        ext g; simp
        set f := (H a).from (CostructuredArrow.mk (F.map g ≫ ε.app a))
        have E := (H a).hom_ext f ⟨g, 𝟙 _, by simp⟩
        rw [E]
      hom_inv_id := by
        ext f; simp
        set g := (H a).from (CostructuredArrow.mk f)
        have Hf := g.w; simp at Hf
        rw [Hf]
    }
    naturality1 x a a' f k := by
      simp
      have E := ε.naturality k; simp at E
      rw [E]
    naturality2 x x' a f h := by
      simp
}

-- triangleをなすunit/counitによる構成
-- Mathlibの随伴はこれ
def Adj.mkby_triangle
  [Category X] [Category A] {F : X ⥤ A} {G : A ⥤ X}
  (μ : Functor.id X ⟶ F ⋙ G) (ε : G ⋙ F ⟶ Functor.id A)
  (H1 : whiskerLeft G μ ≫ whiskerRight ε G = 𝟙 G)
  (H2 : whiskerRight μ F ≫  whiskerLeft F ε = 𝟙 F) :
  Adj F G
:= {
  iso x a := {
    hom f := μ.app x ≫ G.map f
    inv g := F.map g ≫ ε.app a
    hom_inv_id := by
      ext f; simp
      have E := ε.naturality f; simp at E
      rw [E, <- Category.assoc]; clear E
      injection H2 with H2
      have E := congr_fun H2 x; simp  at E
      rw [E]; simp
    inv_hom_id := by
      ext g; simp
      have E := μ.naturality g; simp at E
      rw [<- Category.assoc, <- E, Category.assoc]; clear E
      injection H1 with H1
      have E := congr_fun H1 a; simp at E
      rw [E]; simp
  }
  naturality1 x a a' f k := by simp
  naturality2 x x' a f h := by
    simp
    have E := μ.naturality h; simp at E
    rw [<- Category.assoc, <- E, Category.assoc]
}

def Adj.mk_rightFunc
  [Category X] [Category A] (G : A ⥤ X) {F₀ : X → A}
  {μ : ∀ x : X, x ⟶ G.obj (F₀ x)} (Hμ : ∀ x, isUnivArrTo (S := G) (μ x)) :
  X ⥤ A
:= {
  obj x := F₀ x
  map {x x'} f := ((Hμ x).to (StructuredArrow.mk (f ≫ μ x'))).right
  map_id x := by rw [Category.id_comp]; simp
  map_comp {x₁ x₂ x₃} f g := by
    set fgμ := (StructuredArrow.mk ((f ≫ g) ≫ μ x₃))
    set fμ := (StructuredArrow.mk (f ≫ μ x₂))
    set gμ := (StructuredArrow.mk (g ≫ μ x₃))
    set h₁  := ((Hμ x₁).to fμ)
    set h₂  := ((Hμ x₂).to gμ)
    set h  := ((Hμ x₁).to fgμ)
    have E₁ := h₁.w; simp [fμ] at E₁
    have E₂ := h₂.w; simp [gμ] at E₂
    rw [(Hμ x₁).hom_ext h]; swap
    · refine ⟨𝟙 _, h₁.right ≫ h₂.right, ?_⟩
      simp [fgμ]
      rw [E₂, <- Category.assoc, E₁, Category.assoc]
    · simp
}

def Adj.mk_leftFunc
  [Category X] [Category A] (F : X ⥤ A) {G₀ : A → X}
  {ε : ∀ a : A, F.obj (G₀ a) ⟶ a} (Hε : ∀ a, isUnivArrFrom (S := F) (ε a)) :
  A ⥤ X
:= {
  obj a := G₀ a
  map {a a'} f := ((Hε a').from (CostructuredArrow.mk (ε a ≫ f))).left
  map_id a := by rw [Category.comp_id]; simp
  map_comp {a₁ a₂ a₃} f g := by
    set fgε := (CostructuredArrow.mk (ε a₁ ≫ f ≫ g))
    set fε := (CostructuredArrow.mk (ε a₁ ≫ f))
    set gε := (CostructuredArrow.mk (ε a₂ ≫ g))
    set h₁  := ((Hε a₂).from fε)
    set h₂  := ((Hε a₃).from gε)
    set h  := ((Hε a₃).from fgε)
    have E₁ := h₁.w; simp [fε] at E₁
    have E₂ := h₂.w; simp [gε] at E₂
    rw [(Hε a₃).hom_ext h]; swap
    · refine ⟨h₁.left ≫ h₂.left, 𝟙 _, ?_⟩
      simp [fgε]
      rw [E₂, <- Category.assoc, E₁, Category.assoc]
    · simp
}
-- TODO
-- def Adj.mkby_univArrTo
--   [Category X] [Category A] (G : A ⥤ X) {F₀ : X → A}
--   {μ : ∀ x : X, x ⟶ G.obj (F₀ x)} (Hμ : ∀ x, isUnivArrTo (S := G) (μ x)) :
--   Adj G (Adj.mk_rightFunc G Hμ)
-- := {
--   iso a x := {
--     hom f := by
--       simp [Adj.mk_rightFunc]
--       let Ff := (Adj.mk_rightFunc G Hμ).map f; simp [mk_rightFunc] at Ff
--   }
-- }

-- TODO
-- def Adj.mkby_UnivArrFrom
--   [Category X] [Category A] (F : X ⥤ A) {G₀ : A → X}
--   {ε : ∀ a : A, F.obj (G₀ a) ⟶ a} (Hε : ∀ a, isUnivArrFrom (S := F) (ε a)) :
--   Adj (Adj.mk_leftFunc F Hε) F
-- := sorry

-- TODO
-- lemma Adj.exists_leftFunc_iff_isUnivArrTo
--   [Category X] [Category A] (G : A ⥤ X) :
--   (∃ (F : X ⥤ A), Nonempty (Adj F G)) ↔
--   (∀ x : X, ∃ (a : A) (u : x ⟶ G.obj a), Nonempty (isUnivArrTo u))
-- := by

/------------- /
/ 左随伴の一意性 /
/ -------------/

def Adj.leftFunc_iso
  [Category X] [Category A] {F₁ F₂ : X ⥤ A} {G : A ⥤ X}
  (σ₁ : Adj F₁ G) (σ₂ : Adj F₂ G) :
  F₁ ≅ F₂
:= {
  hom := {
    app x := (σ₁.unit_isUnivArr x).to' (σ₂.unit.app x)
    naturality := by
      intro x x' f
      have Eg := (σ₁.unit_isUnivArr x).w' (σ₂.unit.app x)
      have Eg' := (σ₁.unit_isUnivArr x').w' (σ₂.unit.app x')
      set g := (σ₁.unit_isUnivArr x).to' (σ₂.unit.app x)
      set g' := (σ₁.unit_isUnivArr x').to' (σ₂.unit.app x')
      have E1 := σ₁.unit.naturality; simp at E1
      have E2 := σ₁.counit.naturality; simp at E2
      have E3 := σ₂.unit.naturality; simp at E3
      have E4 := σ₂.counit.naturality; simp at E4
      have Ht₁ := σ₁.triangle2; injection Ht₁ with Ht₁
      have Ht₁x := congr_fun Ht₁ x; simp at Ht₁x; clear Ht₁
      conv =>
        arg 1
        rw [<- Category.id_comp (F₁.map f), <- Ht₁x]; simp
        rw [<- Category.assoc _ (F₁.map f), <- E2 (F₁.map f)]; simp
        rw [<- E2 g']
        rw [<- Category.assoc, <- Category.assoc, <- F₁.map_comp, <- E1 f]
        rw [<- F₁.map_comp, Category.assoc f, <- Eg']; simp
      conv =>
        arg 2
        rw [<- Category.id_comp g, <- Ht₁x]; simp
        rw [<- Category.assoc _ g, <- E2 g]; simp
        rw [<- Category.assoc (F₁.map (σ₁.unit.app x)), <- F₁.map_comp, <- Eg]; simp
        rw [<- E2, <- Category.assoc, <- F₁.map_comp, <- E3]; simp
  }
  inv := {
    app x := (σ₂.unit_isUnivArr x).to' (σ₁.unit.app x)
    naturality x x' f := by
      have Eg := (σ₂.unit_isUnivArr x).w' (σ₁.unit.app x)
      have Eg' := (σ₂.unit_isUnivArr x').w' (σ₁.unit.app x')
      set g := (σ₂.unit_isUnivArr x).to' (σ₁.unit.app x)
      set g' := (σ₂.unit_isUnivArr x').to' (σ₁.unit.app x')

      have E1 := σ₁.unit.naturality; simp at E1
      have E2 := σ₁.counit.naturality; simp at E2
      have E3 := σ₂.unit.naturality; simp at E3
      have E4 := σ₂.counit.naturality; simp at E4
      have Ht₁ := σ₂.triangle2; injection Ht₁ with Ht₁
      have Ht₁x := congr_fun Ht₁ x; simp at Ht₁x; clear Ht₁
      conv =>
        arg 1
        rw [<- Category.id_comp (F₂.map f), <- Ht₁x]; simp
        rw [<- Category.assoc _ (F₂.map f), <- E4]; simp
        rw [<- Category.assoc, <- F₂.map_comp, <- E3, <- E4, <- Category.assoc, <- F₂.map_comp]
        rw [Category.assoc, <- Eg']; simp
      conv =>
        arg 2
        rw [<- Category.id_comp g, <- Ht₁x]; simp
        rw [<- Category.assoc _ g, <- E4]; simp
        rw [<- Category.assoc (F₂.map (σ₂.unit.app x)), <- F₂.map_comp, <- Eg, <- E4]; simp
        rw [<- Category.assoc, <- F₂.map_comp, <- E1]; simp
  }
  hom_inv_id := by
    ext x; simp
    have Eg :=  (σ₁.unit_isUnivArr x).w' (σ₂.unit.app x)
    have Eg' := (σ₂.unit_isUnivArr x).w' (σ₁.unit.app x)
    set g := (σ₁.unit_isUnivArr x).to' (σ₂.unit.app x)
    set g' := (σ₂.unit_isUnivArr x).to' (σ₁.unit.app x)
    have E := σ₁.triangle2; injection E with E
    have Ex := congr_fun E x; simp at Ex; clear E
    rw [<- Ex, Eg']; simp
    have E1 := σ₁.counit.naturality; simp at E1
    rw [E1 g', Eg]; simp
    rw [<- Category.assoc (F₁.map (G.map g)), E1 g]; simp
    rw [<- Category.assoc, Ex]; simp
  inv_hom_id := by
    ext x; simp
    have E :=  (σ₂.unit_isUnivArr x).w' (σ₁.unit.app x)
    have E' := (σ₁.unit_isUnivArr x).w' (σ₂.unit.app x)
    set g := (σ₂.unit_isUnivArr x).to' (σ₁.unit.app x)
    set g' := (σ₁.unit_isUnivArr x).to' (σ₂.unit.app x)
    have E := σ₂.triangle2; injection E with E
    have Ex := congr_fun E x; simp at Ex; clear E
    rw [<- Ex, E']; simp
    have E1 := σ₂.counit.naturality; simp at E1
    rw [E1 g', E]; simp
    rw [<- Category.assoc (F₂.map (G.map g)), E1 g]; simp
    rw [<- Category.assoc, Ex]; simp
}