Theory CZH_UCAT_Adjoints

(* Copyright 2021 (C) Mihails Milehins *)

section‹Adjoints›
theory CZH_UCAT_Adjoints
  imports 
    CZH_UCAT_Limit
    CZH_Elementary_Categories.CZH_ECAT_Yoneda
begin



subsection‹Background›

named_theorems adj_cs_simps
named_theorems adj_cs_intros
named_theorems adj_field_simps

definition AdjLeft :: V where [adj_field_simps]: "AdjLeft = 0"
definition AdjRight :: V where [adj_field_simps]: "AdjRight = 1ℕ"
definition AdjNT :: V where [adj_field_simps]: "AdjNT = 2ℕ"



subsection‹Definition and elementary properties›


text‹
See subsection 2.1 in cite‹"bodo_categories_1970"› or Chapter IV-1 in
cite‹"mac_lane_categories_2010"›.
›

locale is_cf_adjunction =
  𝒵 α +
  vfsequence Φ +
  L: category α ℭ +
  R: category α 𝔇 +
  LR: is_functor α ℭ 𝔇 𝔉 +
  RL: is_functor α 𝔇 ℭ 𝔊 +
  NT: is_iso_ntcf 
    α 
    ‹op_cat ℭ ×C 𝔇› 
    ‹cat_Set α› 
    ‹HomO.C⇘α⇙𝔇(𝔉-,-)› 
    ‹HomO.C⇘α⇙ℭ(-,𝔊-)› 
    ‹Φ⦇AdjNT⦈›
    for α ℭ 𝔇 𝔉 𝔊 Φ +
  assumes cf_adj_length[adj_cs_simps]: "vcard Φ = 3ℕ"
    and cf_adj_AdjLeft[adj_cs_simps]: "Φ⦇AdjLeft⦈ = 𝔉"
    and cf_adj_AdjRight[adj_cs_simps]: "Φ⦇AdjRight⦈ = 𝔊"

syntax "_is_cf_adjunction" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
  (‹(_ : _ ⇌CF _ : _ ⇌⇌Cı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_cf_adjunction" ⇌ is_cf_adjunction
translations "Φ : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" ⇌ 
  "CONST is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ"

lemmas [adj_cs_simps] = 
  is_cf_adjunction.cf_adj_length
  is_cf_adjunction.cf_adj_AdjLeft
  is_cf_adjunction.cf_adj_AdjRight


text‹Components.›

lemma cf_adjunction_components[adj_cs_simps]:
  "[𝔉, 𝔊, φ]∘⦇AdjLeft⦈ = 𝔉"
  "[𝔉, 𝔊, φ]∘⦇AdjRight⦈ = 𝔊"
  "[𝔉, 𝔊, φ]∘⦇AdjNT⦈ = φ"
  unfolding AdjLeft_def AdjRight_def AdjNT_def 
  by (simp_all add: nat_omega_simps)


text‹Rules.›

lemma (in is_cf_adjunction) is_cf_adjunction_axioms'[adj_cs_intros]:
  assumes "α' = α" and "ℭ' = ℭ" and "𝔇' = 𝔇" and "𝔉' = 𝔉" and "𝔊' = 𝔊"
  shows "Φ : 𝔉' ⇌CF 𝔊' : ℭ' ⇌⇌C⇘α'⇙ 𝔇'"  
  unfolding assms by (rule is_cf_adjunction_axioms)

lemmas (in is_cf_adjunction) [adj_cs_intros] = is_cf_adjunction_axioms

mk_ide rf is_cf_adjunction_def[unfolded is_cf_adjunction_axioms_def]
  |intro is_cf_adjunctionI|
  |dest is_cf_adjunctionD[dest]|
  |elim is_cf_adjunctionE[elim]|

lemmas [adj_cs_intros] = is_cf_adjunctionD(3-6)

lemma (in is_cf_adjunction) cf_adj_is_iso_ntcf':
  assumes "𝔉' = HomO.C⇘α⇙𝔇(𝔉-,-)"
    and "𝔊' = HomO.C⇘α⇙ℭ(-,𝔊-)"
    and "𝔄' = op_cat ℭ ×C 𝔇"
    and "𝔅' = cat_Set α"
  shows "Φ⦇AdjNT⦈ : 𝔉' ↦CF.iso 𝔊' : 𝔄' ↦↦C⇘α⇙ 𝔅'"
  unfolding assms by (auto intro: cat_cs_intros)

lemmas [adj_cs_intros] = is_cf_adjunction.cf_adj_is_iso_ntcf'

lemma cf_adj_eqI:
  assumes "Φ : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    and "Φ' : 𝔉' ⇌CF 𝔊' : ℭ' ⇌⇌C⇘α⇙ 𝔇'"
    and "ℭ = ℭ'"
    and "𝔇 = 𝔇'"
    and "𝔉 = 𝔉'"
    and "𝔊 = 𝔊'"
    and "Φ⦇AdjNT⦈ = Φ'⦇AdjNT⦈"
  shows "Φ = Φ'"
proof-
  interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
  interpret Φ': is_cf_adjunction α ℭ' 𝔇' 𝔉' 𝔊' Φ' by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom: "𝒟∘ Φ = 3ℕ" 
      by (cs_concl cs_shallow cs_simp: V_cs_simps adj_cs_simps)
    show "𝒟∘ Φ = 𝒟∘ Φ'" 
      by (cs_concl cs_shallow cs_simp: V_cs_simps adj_cs_simps dom)
    from assms(4-7) have sup: 
      "Φ⦇AdjLeft⦈ = Φ'⦇AdjLeft⦈" 
      "Φ⦇AdjRight⦈ = Φ'⦇AdjRight⦈" 
      "Φ⦇AdjNT⦈ = Φ'⦇AdjNT⦈"  
      by (simp_all add: adj_cs_simps)
    show "a ∈∘ 𝒟∘ Φ ⟹ Φ⦇a⦈ = Φ'⦇a⦈" for a 
      by (unfold dom, elim_in_numeral, insert sup) 
        (auto simp: adj_field_simps)
  qed (auto simp: Φ.L.vsv_axioms Φ'.vsv_axioms)
qed



subsection‹Opposite adjunction›


subsubsection‹Definition and elementary properties›


text‹See cite‹"kan_adjoint_1958"› for further information.›

abbreviation op_cf_adj_nt :: "V ⇒ V ⇒ V ⇒ V"
  where "op_cf_adj_nt ℭ 𝔇 φ ≡ inv_ntcf (bnt_flip (op_cat ℭ) 𝔇 φ)"

definition op_cf_adj :: "V ⇒ V"
  where "op_cf_adj Φ =
    [
      op_cf (Φ⦇AdjRight⦈),
      op_cf (Φ⦇AdjLeft⦈),
      op_cf_adj_nt (Φ⦇AdjLeft⦈⦇HomDom⦈) (Φ⦇AdjLeft⦈⦇HomCod⦈) (Φ⦇AdjNT⦈)
    ]∘"

lemma op_cf_adj_components:
  shows "op_cf_adj Φ⦇AdjLeft⦈ = op_cf (Φ⦇AdjRight⦈)"
    and "op_cf_adj Φ⦇AdjRight⦈ = op_cf (Φ⦇AdjLeft⦈)"
    and "op_cf_adj Φ⦇AdjNT⦈ = 
      op_cf_adj_nt (Φ⦇AdjLeft⦈⦇HomDom⦈) (Φ⦇AdjLeft⦈⦇HomCod⦈) (Φ⦇AdjNT⦈)"
  unfolding op_cf_adj_def adj_field_simps by (simp_all add: nat_omega_simps)

lemma (in is_cf_adjunction) op_cf_adj_components:
  shows "op_cf_adj Φ⦇AdjLeft⦈ = op_cf 𝔊"
    and "op_cf_adj Φ⦇AdjRight⦈ = op_cf 𝔉"
    and "op_cf_adj Φ⦇AdjNT⦈ = inv_ntcf (bnt_flip (op_cat ℭ) 𝔇 (Φ⦇AdjNT⦈))"
  unfolding op_cf_adj_components by (simp_all add: cat_cs_simps adj_cs_simps)

lemmas [cat_op_simps] = is_cf_adjunction.op_cf_adj_components


text‹The opposite adjunction is an adjunction.›

lemma (in is_cf_adjunction) is_cf_adjunction_op:
  ―‹See comments in subsection 2.1 in \cite{bodo_categories_1970}.›
  "op_cf_adj Φ : op_cf 𝔊 ⇌CF op_cf 𝔉 : op_cat 𝔇 ⇌⇌C⇘α⇙ op_cat ℭ"
proof(intro is_cf_adjunctionI, unfold cat_op_simps, unfold op_cf_adj_components)
  show "vfsequence (op_cf_adj Φ)" unfolding op_cf_adj_def by simp
  show "vcard (op_cf_adj Φ) = 3ℕ"
    unfolding op_cf_adj_def by (simp add: nat_omega_simps)
  note adj = is_cf_adjunctionD[OF is_cf_adjunction_axioms]
  from adj have f_φ: "bnt_flip (op_cat ℭ) 𝔇 (Φ⦇AdjNT⦈) :
    HomO.C⇘α⇙op_cat 𝔇(-,op_cf 𝔉-) ↦CF.iso HomO.C⇘α⇙op_cat ℭ(op_cf 𝔊-,-) :
    𝔇 ×C op_cat ℭ ↦↦C⇘α⇙ cat_Set α"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
      )
  show "op_cf_adj_nt ℭ 𝔇 (Φ⦇AdjNT⦈) :
    HomO.C⇘α⇙op_cat ℭ(op_cf 𝔊-,-) ↦CF.iso HomO.C⇘α⇙op_cat 𝔇(-,op_cf 𝔉-) :
    𝔇 ×C op_cat ℭ ↦↦C⇘α⇙ cat_Set α"
    by (rule CZH_ECAT_NTCF.iso_ntcf_is_iso_arr(1)[OF f_φ])
qed (auto intro: cat_cs_intros cat_op_intros)

lemmas is_cf_adjunction_op = 
  is_cf_adjunction.is_cf_adjunction_op

lemma (in is_cf_adjunction) is_cf_adjunction_op'[cat_op_intros]:
  assumes "𝔊' = op_cf 𝔊"
    and "𝔉' = op_cf 𝔉"
    and "𝔇' = op_cat 𝔇"
    and "ℭ' = op_cat ℭ"
  shows "op_cf_adj Φ : 𝔊' ⇌CF 𝔉' : 𝔇' ⇌⇌C⇘α⇙ ℭ'"
  unfolding assms by (rule is_cf_adjunction_op)

lemmas [cat_op_intros] = is_cf_adjunction.is_cf_adjunction_op'


text‹The operation of taking the opposite adjunction is an involution.›

lemma (in is_cf_adjunction) cf_adjunction_op_cf_adj_op_cf_adj[cat_op_simps]:
  "op_cf_adj (op_cf_adj Φ) = Φ"
proof(rule cf_adj_eqI)
  show Φ': "op_cf_adj (op_cf_adj Φ) : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
  proof(intro is_cf_adjunctionI)
    show "vfsequence (op_cf_adj (op_cf_adj Φ))" unfolding op_cf_adj_def by simp
    from is_cf_adjunction_axioms show "op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈ : 
      HomO.C⇘α⇙𝔇(𝔉-,-) ↦CF.iso HomO.C⇘α⇙ℭ(-,𝔊-) : 
      op_cat ℭ ×C 𝔇 ↦↦C⇘α⇙ cat_Set α"
      by
        (
          cs_concl cs_shallow
            cs_intro: cat_cs_intros cat_op_intros adj_cs_intros
            cs_simp: cat_cs_simps cat_op_simps
        )
    show "vcard (op_cf_adj (op_cf_adj Φ)) = 3ℕ"
      unfolding op_cf_adj_def by (simp add: nat_omega_simps)
    from is_cf_adjunction_axioms show "op_cf_adj (op_cf_adj Φ)⦇AdjLeft⦈ = 𝔉"
      by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
    from is_cf_adjunction_axioms show "op_cf_adj (op_cf_adj Φ)⦇AdjRight⦈ = 𝔊"
      by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
  qed (auto intro: cat_cs_intros)
  interpret Φ': is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 ‹op_cf_adj (op_cf_adj Φ)› 
    by (rule Φ')
  show "op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈ = Φ⦇AdjNT⦈"
  proof(rule ntcf_eqI)
    show op_op_Φ:
      "op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈ :
        HomO.C⇘α⇙𝔇(𝔉-,-) ↦CF HomO.C⇘α⇙ℭ(-,𝔊-) :
        op_cat ℭ ×C 𝔇 ↦↦C⇘α⇙ cat_Set α"
      by (rule Φ'.NT.is_ntcf_axioms)
    show Φ: "Φ⦇AdjNT⦈ :
      HomO.C⇘α⇙𝔇(𝔉-,-) ↦CF HomO.C⇘α⇙ℭ(-,𝔊-) : 
      op_cat ℭ ×C 𝔇 ↦↦C⇘α⇙ cat_Set α"
      by (rule NT.is_ntcf_axioms)
    from op_op_Φ have dom_lhs:
      "𝒟∘ (op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈⦇NTMap⦈) = (op_cat ℭ ×C 𝔇)⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    show "op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈⦇NTMap⦈ = Φ⦇AdjNT⦈⦇NTMap⦈"
    proof(rule vsv_eqI, unfold NT.ntcf_NTMap_vdomain dom_lhs)
      fix cd assume prems: "cd ∈∘ (op_cat ℭ ×C 𝔇)⦇Obj⦈"
      then obtain c d 
        where cd_def: "cd = [c, d]∘"
          and c: "c ∈∘ op_cat ℭ⦇Obj⦈"
          and d: "d ∈∘ 𝔇⦇Obj⦈"
        by (elim cat_prod_2_ObjE[OF L.category_op R.category_axioms prems])
      from is_cf_adjunction_axioms c d L.category_axioms R.category_axioms Φ 
      show "op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈⦇NTMap⦈⦇cd⦈ = Φ⦇AdjNT⦈⦇NTMap⦈⦇cd⦈"
        unfolding cd_def cat_op_simps
        by
          (
            cs_concl 
              cs_intro: 
                cat_arrow_cs_intros 
                ntcf_cs_intros 
                adj_cs_intros 
                cat_op_intros 
                cat_cs_intros 
                cat_prod_cs_intros 
             cs_simp: cat_cs_simps cat_op_simps
         )
    qed (auto intro: inv_ntcf_NTMap_vsv)
  qed simp_all
qed (auto intro: adj_cs_intros)

lemmas [cat_op_simps] = is_cf_adjunction.cf_adjunction_op_cf_adj_op_cf_adj


subsubsection‹Alternative form of the naturality condition›


text‹
The lemmas in this subsection are based on the comments on page 81 in 
cite‹"mac_lane_categories_2010"›.
›

lemma (in is_cf_adjunction) cf_adj_Comp_commute_RL:
  assumes "x ∈∘ ℭ⦇Obj⦈" 
    and "f : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
    and "k : a ↦⇘𝔇⇙ a'"
  shows 
    "𝔊⦇ArrMap⦈⦇k⦈ ∘A⇘ℭ⇙ (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)⦇ArrVal⦈⦇f⦈ =
      (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a'⦈∙)⦇ArrVal⦈⦇k ∘A⇘𝔇⇙ f⦈"
proof-
  from 
    assms 
    is_cf_adjunction_axioms 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have φ_x_a: "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙ :
    Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
    by
      (
        cs_concl 
          cs_simp: cat_cs_simps
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  note φ_x_a_f = 
    cat_Set_ArrVal_app_vrange[OF φ_x_a, unfolded in_Hom_iff, OF assms(2)]
  from 
    is_cf_adjunction_axioms assms 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have φ_x_a': 
    "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a'⦈∙ :
      Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a' ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a'⦈)"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  from is_cf_adjunction_axioms this assms have x_k:
    "[ℭ⦇CId⦈⦇x⦈, k]∘ : [x, a]∘ ↦⇘op_cat ℭ ×C 𝔇⇙ [x, a']∘"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  from 
    NT.ntcf_Comp_commute[OF this] is_cf_adjunction_axioms assms 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have
    "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a'⦈∙ ∘A⇘cat_Set α⇙ cf_hom 𝔇 [𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈, k]∘ =
      cf_hom ℭ [ℭ⦇CId⦈⦇x⦈, 𝔊⦇ArrMap⦈⦇k⦈]∘ ∘A⇘cat_Set α⇙ Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙"
    (is ‹?lhs = ?rhs›)
    by (*slow*)
      (
        cs_prems cs_ist_simple
          cs_simp: cat_cs_simps
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  moreover from 
    is_cf_adjunction_axioms assms φ_x_a' 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have "?lhs⦇ArrVal⦈⦇f⦈ = (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a'⦈∙)⦇ArrVal⦈⦇k ∘A⇘𝔇⇙ f⦈"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  moreover from 
    is_cf_adjunction_axioms assms φ_x_a_f 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have
    "?rhs⦇ArrVal⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇k⦈ ∘A⇘ℭ⇙ (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)⦇ArrVal⦈⦇f⦈"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  ultimately show ?thesis by simp
qed

lemma (in is_cf_adjunction) cf_adj_Comp_commute_LR:
  assumes "x ∈∘ ℭ⦇Obj⦈" 
    and "f : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
    and "h : x' ↦⇘ℭ⇙ x"
  shows
    "(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)⦇ArrVal⦈⦇f⦈ ∘A⇘ℭ⇙ h =
      (Φ⦇AdjNT⦈⦇NTMap⦈⦇x', a⦈∙)⦇ArrVal⦈⦇f ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇h⦈⦈"
proof-
  from 
    is_cf_adjunction_axioms assms 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have φ_x_a: "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙ :
    Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  note φ_x_a_f = 
    cat_Set_ArrVal_app_vrange[OF φ_x_a, unfolded in_Hom_iff, OF assms(2)]
  from is_cf_adjunction_axioms assms have
    "[h, 𝔇⦇CId⦈⦇a⦈]∘ : [x, a]∘ ↦⇘op_cat ℭ ×C 𝔇⇙ [x', a]∘"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  from 
    NT.ntcf_Comp_commute[OF this] is_cf_adjunction_axioms assms 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have
    "Φ⦇AdjNT⦈⦇NTMap⦈⦇x', a⦈∙ ∘A⇘cat_Set α⇙ cf_hom 𝔇 [𝔉⦇ArrMap⦈⦇h⦈, 𝔇⦇CId⦈⦇a⦈]∘ =
      cf_hom ℭ [h, ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈]∘ ∘A⇘cat_Set α⇙ Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙"
    (is ‹?lhs = ?rhs›)
    by (*slow*)
      (
        cs_prems 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )  
  moreover from 
    is_cf_adjunction_axioms assms 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have "?lhs⦇ArrVal⦈⦇f⦈ = (Φ⦇AdjNT⦈⦇NTMap⦈⦇x', a⦈∙)⦇ArrVal⦈⦇f ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇h⦈⦈"
    by 
      (
        cs_concl
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  moreover from 
    is_cf_adjunction_axioms assms φ_x_a_f 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have "?rhs⦇ArrVal⦈⦇f⦈ = (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)⦇ArrVal⦈⦇f⦈ ∘A⇘ℭ⇙ h"
    by 
      (
        cs_concl 
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  ultimately show ?thesis by simp
qed



subsection‹Unit›


subsubsection‹Definition and elementary properties›


text‹See Chapter IV-1 in cite‹"mac_lane_categories_2010"›.›

definition cf_adjunction_unit :: "V ⇒ V" (‹ηC›)
  where "ηC Φ =
    [
      (
        λx∈∘Φ⦇AdjLeft⦈⦇HomDom⦈⦇Obj⦈.
          (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, Φ⦇AdjLeft⦈⦇ObjMap⦈⦇x⦈⦈∙)⦇ArrVal⦈⦇
            Φ⦇AdjLeft⦈⦇HomCod⦈⦇CId⦈⦇Φ⦇AdjLeft⦈⦇ObjMap⦈⦇x⦈⦈
          ⦈
      ),
      cf_id (Φ⦇AdjLeft⦈⦇HomDom⦈),
      (Φ⦇AdjRight⦈) ∘CF (Φ⦇AdjLeft⦈),
      Φ⦇AdjLeft⦈⦇HomDom⦈,
      Φ⦇AdjLeft⦈⦇HomDom⦈
    ]∘"


text‹Components.›

lemma cf_adjunction_unit_components:
  shows "ηC Φ⦇NTMap⦈ =
    (
      λx∈∘Φ⦇AdjLeft⦈⦇HomDom⦈⦇Obj⦈.
        (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, Φ⦇AdjLeft⦈⦇ObjMap⦈⦇x⦈⦈∙)⦇ArrVal⦈⦇
          Φ⦇AdjLeft⦈⦇HomCod⦈⦇CId⦈⦇Φ⦇AdjLeft⦈⦇ObjMap⦈⦇x⦈⦈
        ⦈
    )"
    and "ηC Φ⦇NTDom⦈ = cf_id (Φ⦇AdjLeft⦈⦇HomDom⦈)"
    and "ηC Φ⦇NTCod⦈ = (Φ⦇AdjRight⦈) ∘CF (Φ⦇AdjLeft⦈)"
    and "ηC Φ⦇NTDGDom⦈ = Φ⦇AdjLeft⦈⦇HomDom⦈"
    and "ηC Φ⦇NTDGCod⦈ = Φ⦇AdjLeft⦈⦇HomDom⦈"
  unfolding cf_adjunction_unit_def nt_field_simps 
  by (simp_all add: nat_omega_simps)

context is_cf_adjunction
begin

lemma cf_adjunction_unit_components':
  shows "ηC Φ⦇NTMap⦈ =
    (λx∈∘ℭ⦇Obj⦈. (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, 𝔉⦇ObjMap⦈⦇x⦈⦈∙)⦇ArrVal⦈⦇𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈⦈)"
    and "ηC Φ⦇NTDom⦈ = cf_id ℭ"
    and "ηC Φ⦇NTCod⦈ = 𝔊 ∘CF 𝔉"
    and "ηC Φ⦇NTDGDom⦈ = ℭ"
    and "ηC Φ⦇NTDGCod⦈ = ℭ"
  unfolding cf_adjunction_unit_components
  by (cs_concl cs_shallow cs_simp: cat_cs_simps adj_cs_simps)+

mk_VLambda cf_adjunction_unit_components'(1)
  |vdomain cf_adjunction_unit_NTMap_vdomain[adj_cs_simps]|
  |app cf_adjunction_unit_NTMap_app[adj_cs_simps]|

end

mk_VLambda cf_adjunction_unit_components(1)
  |vsv cf_adjunction_unit_NTMap_vsv[adj_cs_intros]|

lemmas [adj_cs_simps] = 
  is_cf_adjunction.cf_adjunction_unit_NTMap_vdomain
  is_cf_adjunction.cf_adjunction_unit_NTMap_app


subsubsection‹Natural transformation map›

lemma (in is_cf_adjunction) cf_adjunction_unit_NTMap_is_arr: 
  assumes "x ∈∘ ℭ⦇Obj⦈"
  shows "ηC Φ⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
proof-
  from 
    is_cf_adjunction_axioms assms
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have φ_x_𝔉x: 
    "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, 𝔉⦇ObjMap⦈⦇x⦈⦈∙ :
      Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) (𝔉⦇ObjMap⦈⦇x⦈) ↦⇘cat_Set α⇙ 
      Hom ℭ x (𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈)"
    by 
      (
        cs_concl  
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      ) 
  from is_cf_adjunction_axioms assms have CId_𝔉x: 
    "𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ 𝔉⦇ObjMap⦈⦇x⦈"
    by (cs_concl cs_intro: cat_cs_intros adj_cs_intros)   
  from 
    is_cf_adjunction_axioms 
    assms
    cat_Set_ArrVal_app_vrange[OF φ_x_𝔉x, unfolded in_Hom_iff, OF CId_𝔉x]
  show "ηC Φ⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
    by (cs_concl cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
qed

lemma (in is_cf_adjunction) cf_adjunction_unit_NTMap_is_arr': 
  assumes "x ∈∘ ℭ⦇Obj⦈"
    and "a = x"
    and "b = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
    and "ℭ' = ℭ"
  shows "ηC Φ⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ'⇙ b"
  using assms(1) unfolding assms(2-4) by (rule cf_adjunction_unit_NTMap_is_arr)

lemmas [adj_cs_intros] = is_cf_adjunction.cf_adjunction_unit_NTMap_is_arr'

lemma (in is_cf_adjunction) cf_adjunction_unit_NTMap_vrange: 
  "ℛ∘ (ηC Φ⦇NTMap⦈) ⊆∘ ℭ⦇Arr⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold cf_adjunction_unit_NTMap_vdomain)
  fix x assume prems: "x ∈∘ ℭ⦇Obj⦈"
  from cf_adjunction_unit_NTMap_is_arr[OF prems] show "ηC Φ⦇NTMap⦈⦇x⦈ ∈∘ ℭ⦇Arr⦈"
    by auto
qed (auto intro: adj_cs_intros)


subsubsection‹Unit is a natural transformation›

lemma (in is_cf_adjunction) cf_adjunction_unit_is_ntcf:
  "ηC Φ : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
proof(intro is_ntcfI')
  show "vfsequence (ηC Φ)" unfolding cf_adjunction_unit_def by simp
  show "vcard (ηC Φ) = 5ℕ"
    unfolding cf_adjunction_unit_def by (simp add: nat_omega_simps)
  from is_cf_adjunction_axioms show "cf_id ℭ : ℭ ↦↦C⇘α⇙ ℭ"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
  from is_cf_adjunction_axioms show "𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
  from is_cf_adjunction_axioms show "𝒟∘ (ηC Φ⦇NTMap⦈) = ℭ⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
  show "ηC Φ⦇NTMap⦈⦇a⦈ : cf_id ℭ⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (𝔊 ∘CF 𝔉)⦇ObjMap⦈⦇a⦈"
    if "a ∈∘ ℭ⦇Obj⦈" for a
    using is_cf_adjunction_axioms that 
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
  show
    "ηC Φ⦇NTMap⦈⦇b⦈ ∘A⇘ℭ⇙ cf_id ℭ⦇ArrMap⦈⦇f⦈ =
      (𝔊 ∘CF 𝔉)⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ ηC Φ⦇NTMap⦈⦇a⦈"
    if "f : a ↦⇘ℭ⇙ b" for a b f
    using is_cf_adjunction_axioms that
    by 
      (
        cs_concl 
          cs_simp: 
            cf_adj_Comp_commute_RL cf_adj_Comp_commute_LR 
            cat_cs_simps  
            adj_cs_simps 
          cs_intro: cat_cs_intros adj_cs_intros
      )
qed (auto simp: cf_adjunction_unit_components')

lemma (in is_cf_adjunction) cf_adjunction_unit_is_ntcf':
  assumes "𝔖 = cf_id ℭ"
    and "𝔖' = 𝔊 ∘CF 𝔉"
    and "𝔄 = ℭ"
    and "𝔅 = ℭ"
  shows "ηC Φ : 𝔖 ↦CF 𝔖' : 𝔄 ↦↦C⇘α⇙ 𝔅"
  unfolding assms by (rule cf_adjunction_unit_is_ntcf)

lemmas [adj_cs_intros] = is_cf_adjunction.cf_adjunction_unit_is_ntcf'


subsubsection‹Every component of a unit is a universal arrow›


text‹
The lemmas in this subsection are based on elements of the statement of 
Theorem 1 in Chapter IV-1 in cite‹"mac_lane_categories_2010"›.
›

lemma (in is_cf_adjunction) cf_adj_umap_of_unit:
  assumes "x ∈∘ ℭ⦇Obj⦈" and "a ∈∘ 𝔇⦇Obj⦈"
  shows "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙ = umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (ηC Φ⦇NTMap⦈⦇x⦈) a"
  (is ‹Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙ = ?uof_a›)
proof-

  from 
    is_cf_adjunction_axioms assms 
    L.category_axioms R.category_axioms (*speedup*)
    L.category_op R.category_op (*speedup*)
  have φ_xa: "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙ :
    Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
    by
      (
        cs_concl
          cs_simp: cat_cs_simps 
          cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
      )
  then have dom_lhs:
    "𝒟∘ ((Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)⦇ArrVal⦈) = Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from is_cf_adjunction_axioms assms have uof_a:
    "?uof_a : Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
    by (cs_concl cs_intro: cat_cs_intros adj_cs_intros)
  then have dom_rhs: "𝒟∘ (?uof_a⦇ArrVal⦈) = Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a"
    by (cs_concl cs_simp: cat_cs_simps)

  show ?thesis
  proof(rule arr_Set_eqI[of α])
    from φ_xa show arr_Set_φ_xa: "arr_Set α (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)"
      by (auto dest: cat_Set_is_arrD(1))
    from uof_a show arr_Set_uof_a: "arr_Set α ?uof_a" 
      by (auto dest: cat_Set_is_arrD(1))
    show "(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)⦇ArrVal⦈ = ?uof_a⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
      fix g assume prems: "g : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
      from is_cf_adjunction_axioms assms prems show
        "(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)⦇ArrVal⦈⦇g⦈ = ?uof_a⦇ArrVal⦈⦇g⦈"
        by
          (
            cs_concl cs_shallow
              cs_simp:
                cf_adj_Comp_commute_RL
                adj_cs_simps
                cat_cs_simps
                cat_op_simps
                cat_prod_cs_simps
              cs_intro:
                adj_cs_intros
                ntcf_cs_intros
                cat_cs_intros
                cat_op_intros
                cat_prod_cs_intros
          )
    qed (use arr_Set_φ_xa arr_Set_uof_a in auto)
  
  qed (use φ_xa uof_a in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+

qed

lemma (in is_cf_adjunction) cf_adj_umap_of_unit':
  assumes "x ∈∘ ℭ⦇Obj⦈" 
    and "a ∈∘ 𝔇⦇Obj⦈"
    and "η = ηC Φ⦇NTMap⦈⦇x⦈"
    and "𝔉x = 𝔉⦇ObjMap⦈⦇x⦈"
  shows "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙ = umap_of 𝔊 x 𝔉x η a"
  using assms(1,2) unfolding assms(3,4) by (rule cf_adj_umap_of_unit)

lemma (in is_cf_adjunction) cf_adjunction_unit_component_is_ua_of:
  assumes "x ∈∘ ℭ⦇Obj⦈"
  shows "universal_arrow_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (ηC Φ⦇NTMap⦈⦇x⦈)"
    (is ‹universal_arrow_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) ?ηx›)
proof(rule RL.cf_ua_of_if_ntcf_ua_of_is_iso_ntcf)
  from is_cf_adjunction_axioms assms show "𝔉⦇ObjMap⦈⦇x⦈ ∈∘ 𝔇⦇Obj⦈"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros adj_cs_intros)
  from is_cf_adjunction_axioms assms show 
    "ηC Φ⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros adj_cs_intros)
  show 
    "ntcf_ua_of α 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (ηC Φ⦇NTMap⦈⦇x⦈) :
      HomO.C⇘α⇙𝔇(𝔉⦇ObjMap⦈⦇x⦈,-) ↦CF.iso HomO.C⇘α⇙ℭ(x,-) ∘CF 𝔊 :
      𝔇 ↦↦C⇘α⇙ cat_Set α"
    (is ‹?ntcf_ua_of : ?H𝔉 ↦CF.iso ?H𝔊 : 𝔇 ↦↦C⇘α⇙ cat_Set α›)
  proof(rule is_iso_ntcfI)
    from is_cf_adjunction_axioms assms show 
      "?ntcf_ua_of : ?H𝔉 ↦CF ?H𝔊 : 𝔇 ↦↦C⇘α⇙ cat_Set α"
      by (intro RL.cf_ntcf_ua_of_is_ntcf) 
        (cs_concl cs_shallow cs_intro: cat_cs_intros adj_cs_intros)+
    fix a assume prems: "a ∈∘ 𝔇⦇Obj⦈"
    from assms prems have 
      "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙ = umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) ?ηx a"
      (is ‹Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙ = ?uof_a›)
      by (rule cf_adj_umap_of_unit)
    from assms prems L.category_axioms R.category_axioms have
      "[x, a]∘ ∈∘ (op_cat ℭ ×C 𝔇)⦇Obj⦈"
      by (cs_concl cs_shallow cs_intro:  cat_op_intros cat_prod_cs_intros)
    from 
      NT.iso_ntcf_is_iso_arr[
        OF this, unfolded cf_adj_umap_of_unit[OF assms prems]
        ]
      is_cf_adjunction_axioms assms prems
      L.category_axioms R.category_axioms
    have "?uof_a : Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦iso⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
      by 
        (
          cs_prems
            cs_simp: cat_cs_simps 
            cs_intro: 
              cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
        )
    with is_cf_adjunction_axioms assms prems show 
      "?ntcf_ua_of⦇NTMap⦈⦇a⦈ : ?H𝔉⦇ObjMap⦈⦇a⦈ ↦iso⇘cat_Set α⇙ ?H𝔊⦇ObjMap⦈⦇a⦈"
      by 
        (
          cs_concl
            cs_simp: cat_cs_simps 
            cs_intro: cat_cs_intros cat_op_intros adj_cs_intros
        )
  qed
qed



subsection‹Counit›


subsubsection‹Definition and elementary properties›

definition cf_adjunction_counit :: "V ⇒ V" (‹εC›)
  where "εC Φ =
    [
      (
        λx∈∘Φ⦇AdjLeft⦈⦇HomCod⦈⦇Obj⦈.
          (Φ⦇AdjNT⦈⦇NTMap⦈⦇Φ⦇AdjRight⦈⦇ObjMap⦈⦇x⦈, x⦈∙)¯Set⦇ArrVal⦈⦇
            Φ⦇AdjLeft⦈⦇HomDom⦈⦇CId⦈⦇Φ⦇AdjRight⦈⦇ObjMap⦈⦇x⦈⦈
            ⦈
      ), 
      (Φ⦇AdjLeft⦈) ∘CF (Φ⦇AdjRight⦈),
      cf_id (Φ⦇AdjLeft⦈⦇HomCod⦈),
      Φ⦇AdjLeft⦈⦇HomCod⦈,
      Φ⦇AdjLeft⦈⦇HomCod⦈
    ]∘"


text‹Components.›

lemma cf_adjunction_counit_components:
  shows "εC Φ⦇NTMap⦈ =
    (
      λx∈∘Φ⦇AdjLeft⦈⦇HomCod⦈⦇Obj⦈.
        (Φ⦇AdjNT⦈⦇NTMap⦈⦇Φ⦇AdjRight⦈⦇ObjMap⦈⦇x⦈, x⦈∙)¯Set⦇ArrVal⦈⦇
          Φ⦇AdjLeft⦈⦇HomDom⦈⦇CId⦈⦇Φ⦇AdjRight⦈⦇ObjMap⦈⦇x⦈⦈
          ⦈
    )"
    and "εC Φ⦇NTDom⦈ = (Φ⦇AdjLeft⦈) ∘CF (Φ⦇AdjRight⦈)"
    and "εC Φ⦇NTCod⦈ = cf_id (Φ⦇AdjLeft⦈⦇HomCod⦈)"
    and "εC Φ⦇NTDGDom⦈ = Φ⦇AdjLeft⦈⦇HomCod⦈"
    and "εC Φ⦇NTDGCod⦈ = Φ⦇AdjLeft⦈⦇HomCod⦈"
  unfolding cf_adjunction_counit_def nt_field_simps 
  by (simp_all add: nat_omega_simps)

context is_cf_adjunction
begin

lemma cf_adjunction_counit_components':
  shows "εC Φ⦇NTMap⦈ =
    (
      λx∈∘𝔇⦇Obj⦈.
        (Φ⦇AdjNT⦈⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈, x⦈∙)¯Set⦇ArrVal⦈⦇ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈⦈
    )"
    and "εC Φ⦇NTDom⦈ = 𝔉 ∘CF 𝔊"
    and "εC Φ⦇NTCod⦈ = cf_id 𝔇"
    and "εC Φ⦇NTDGDom⦈ = 𝔇"
    and "εC Φ⦇NTDGCod⦈ = 𝔇"
  unfolding cf_adjunction_counit_components
  by (cs_concl cs_shallow cs_simp: cat_cs_simps adj_cs_simps)+

mk_VLambda cf_adjunction_counit_components'(1)
  |vdomain cf_adjunction_counit_NTMap_vdomain[adj_cs_simps]|
  |app cf_adjunction_counit_NTMap_app[adj_cs_simps]|

end

mk_VLambda cf_adjunction_counit_components(1)
  |vsv cf_adjunction_counit_NTMap_vsv[adj_cs_intros]|

lemmas [adj_cs_simps] = 
  is_cf_adjunction.cf_adjunction_counit_NTMap_vdomain
  is_cf_adjunction.cf_adjunction_counit_NTMap_app


subsubsection‹Duality for the unit and counit›

lemma (in is_cf_adjunction) cf_adjunction_unit_NTMap_op:
  "ηC (op_cf_adj Φ)⦇NTMap⦈ = εC Φ⦇NTMap⦈"
proof-
  interpret op_Φ: 
    is_cf_adjunction α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔉› ‹op_cf_adj Φ›
    by (rule is_cf_adjunction_op)
  show ?thesis
  proof
    (
      rule vsv_eqI, 
      unfold 
        cf_adjunction_counit_NTMap_vdomain 
        op_Φ.cf_adjunction_unit_NTMap_vdomain
    )
    fix a assume prems: "a ∈∘ op_cat 𝔇⦇Obj⦈"
    then have a: "a ∈∘ 𝔇⦇Obj⦈" unfolding cat_op_simps by simp
    from is_cf_adjunction_axioms a show 
      "ηC (op_cf_adj Φ)⦇NTMap⦈⦇a⦈ = εC Φ⦇NTMap⦈⦇a⦈"
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_Set_cs_simps cat_cs_simps cat_op_simps adj_cs_simps 
            cs_intro: 
              cat_arrow_cs_intros cat_cs_intros cat_op_intros cat_prod_cs_intros
        )
  qed 
    (
      simp_all add: 
        cat_op_simps cf_adjunction_counit_NTMap_vsv cf_adjunction_unit_NTMap_vsv
    )
qed


lemmas [cat_op_simps] = is_cf_adjunction.cf_adjunction_unit_NTMap_op

lemma (in is_cf_adjunction) cf_adjunction_counit_NTMap_op:
  "εC (op_cf_adj Φ)⦇NTMap⦈ = ηC Φ⦇NTMap⦈"
  by 
    (
      rule is_cf_adjunction.cf_adjunction_unit_NTMap_op[
        OF is_cf_adjunction_op,
        unfolded is_cf_adjunction.cf_adjunction_op_cf_adj_op_cf_adj[
          OF is_cf_adjunction_axioms
          ],
        unfolded cat_op_simps,
        symmetric
      ]
   )

lemmas [cat_op_simps] = is_cf_adjunction.cf_adjunction_counit_NTMap_op

lemma (in is_cf_adjunction) op_ntcf_cf_adjunction_counit:
  "op_ntcf (εC Φ) = ηC (op_cf_adj Φ)"
  (is ‹?ε = ?η›)
proof(rule vsv_eqI)
  interpret op_Φ: 
    is_cf_adjunction α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔉› ‹op_cf_adj Φ›
    by (rule is_cf_adjunction_op)
  have dom_lhs: "𝒟∘ ?ε = 5ℕ" unfolding op_ntcf_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟∘ ?η = 5ℕ" 
    unfolding cf_adjunction_unit_def by (simp add: nat_omega_simps)
  show "𝒟∘ ?ε = 𝒟∘ ?η" unfolding dom_lhs dom_rhs by simp
  show "a ∈∘ 𝒟∘ ?ε ⟹ ?ε⦇a⦈ = ?η⦇a⦈" for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral, 
        fold nt_field_simps, 
        unfold cf_adjunction_unit_NTMap_op,
        unfold 
          cf_adjunction_counit_components' 
          cf_adjunction_unit_components'
          op_Φ.cf_adjunction_counit_components' 
          op_Φ.cf_adjunction_unit_components'
          cat_op_simps
      )
      simp_all
qed (auto simp: op_ntcf_def cf_adjunction_unit_def)

lemmas [cat_op_simps] = is_cf_adjunction.op_ntcf_cf_adjunction_counit

lemma (in is_cf_adjunction) op_ntcf_cf_adjunction_unit:
  "op_ntcf (ηC Φ) = εC (op_cf_adj Φ)"
  (is ‹?η = ?ε›)
proof(rule vsv_eqI)
  interpret op_Φ: 
    is_cf_adjunction α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔉› ‹op_cf_adj Φ›
    by (rule is_cf_adjunction_op)
  have dom_lhs: "𝒟∘ ?η = 5ℕ" 
    unfolding op_ntcf_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟∘ ?ε = 5ℕ" 
    unfolding cf_adjunction_counit_def by (simp add: nat_omega_simps)
  show "𝒟∘ ?η = 𝒟∘ ?ε" unfolding dom_lhs dom_rhs by simp
  show "a ∈∘ 𝒟∘ ?η ⟹ ?η⦇a⦈ = ?ε⦇a⦈" for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral, 
        fold nt_field_simps, 
        unfold cf_adjunction_counit_NTMap_op,
        unfold 
          cf_adjunction_counit_components' 
          cf_adjunction_unit_components'
          op_Φ.cf_adjunction_counit_components' 
          op_Φ.cf_adjunction_unit_components'
          cat_op_simps
      )
      simp_all
qed (auto simp: op_ntcf_def cf_adjunction_counit_def)

lemmas [cat_op_simps] = is_cf_adjunction.op_ntcf_cf_adjunction_unit


subsubsection‹Natural transformation map›

lemma (in is_cf_adjunction) cf_adjunction_counit_NTMap_is_arr: 
  assumes "x ∈∘ 𝔇⦇Obj⦈"
  shows "εC Φ⦇NTMap⦈⦇x⦈ : 𝔉⦇ObjMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ ↦⇘𝔇⇙ x"
proof-
  from assms have x: "x ∈∘ op_cat 𝔇⦇Obj⦈" unfolding cat_op_simps by simp
  show ?thesis
    by 
      (
        rule is_cf_adjunction.cf_adjunction_unit_NTMap_is_arr[
          OF is_cf_adjunction_op x, 
          unfolded cf_adjunction_unit_NTMap_op cat_op_simps
          ]
      )
qed

lemma (in is_cf_adjunction) cf_adjunction_counit_NTMap_is_arr': 
  assumes "x ∈∘ 𝔇⦇Obj⦈"
    and "a = 𝔉⦇ObjMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈"
    and "b = x"
    and "𝔇' = 𝔇"
  shows "εC Φ⦇NTMap⦈⦇x⦈ : a ↦⇘𝔇'⇙ b"
  using assms(1) unfolding assms(2-4) by (rule cf_adjunction_counit_NTMap_is_arr)

lemmas [adj_cs_intros] = is_cf_adjunction.cf_adjunction_counit_NTMap_is_arr'

lemma (in is_cf_adjunction) cf_adjunction_counit_NTMap_vrange: 
  "ℛ∘ (εC Φ⦇NTMap⦈) ⊆∘ 𝔇⦇Arr⦈"
  by 
    (
      rule is_cf_adjunction.cf_adjunction_unit_NTMap_vrange[
        OF is_cf_adjunction_op,
        unfolded cf_adjunction_unit_NTMap_op cat_op_simps
        ]
    )


subsubsection‹Counit is a natural transformation›

lemma (in is_cf_adjunction) cf_adjunction_counit_is_ntcf:
  "εC Φ : 𝔉 ∘CF 𝔊 ↦CF cf_id 𝔇 : 𝔇 ↦↦C⇘α⇙ 𝔇"
proof-
  from is_cf_adjunction.cf_adjunction_unit_is_ntcf[OF is_cf_adjunction_op] have 
    "εC Φ :
      op_cf (op_cf 𝔉 ∘CF op_cf 𝔊) ↦CF op_cf (cf_id (op_cat 𝔇)) :
      op_cat (op_cat 𝔇) ↦↦C⇘α⇙ op_cat (op_cat 𝔇)"
    unfolding
      is_cf_adjunction.op_ntcf_cf_adjunction_unit[
        OF is_cf_adjunction_op, unfolded cat_op_simps, symmetric
        ]
    by (rule is_ntcf.is_ntcf_op)
  then show ?thesis unfolding cat_op_simps .
qed

lemma (in is_cf_adjunction) cf_adjunction_counit_is_ntcf':
  assumes "𝔖 = 𝔉 ∘CF 𝔊"
    and "𝔖' = cf_id 𝔇"
    and "𝔄 = 𝔇"
    and "𝔅 = 𝔇"
  shows "εC Φ : 𝔖 ↦CF 𝔖' : 𝔄 ↦↦C⇘α⇙ 𝔅"
  unfolding assms by (rule cf_adjunction_counit_is_ntcf)

lemmas [adj_cs_intros] = is_cf_adjunction.cf_adjunction_counit_is_ntcf'


subsubsection‹Every component of a counit is a universal arrow›

text‹
The lemmas in this subsection are based on elements of the statement of 
Theorem 1 in Chapter IV-1 in cite‹"mac_lane_categories_2010"›.
›

lemma (in is_cf_adjunction) cf_adj_umap_fo_counit:
  assumes "x ∈∘ 𝔇⦇Obj⦈" and "a ∈∘ ℭ⦇Obj⦈"
  shows "op_cf_adj Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙ =
    umap_fo 𝔉 x (𝔊⦇ObjMap⦈⦇x⦈) (εC Φ⦇NTMap⦈⦇x⦈) a"
  by
    (
      rule is_cf_adjunction.cf_adj_umap_of_unit[
        OF is_cf_adjunction_op,
        unfolded cat_op_simps,
        OF assms,
        unfolded cf_adjunction_unit_NTMap_op
        ]
    )

lemma (in is_cf_adjunction) cf_adjunction_counit_component_is_ua_fo:
  assumes "x ∈∘ 𝔇⦇Obj⦈"
  shows "universal_arrow_fo 𝔉 x (𝔊⦇ObjMap⦈⦇x⦈) (εC Φ⦇NTMap⦈⦇x⦈)"
  by 
    (
      rule is_cf_adjunction.cf_adjunction_unit_component_is_ua_of[
        OF is_cf_adjunction_op, 
        unfolded cat_op_simps, 
        OF assms,
        unfolded cf_adjunction_unit_NTMap_op
        ]
    )


subsubsection‹Further properties›

lemma (in is_cf_adjunction) cf_adj_AdjNT_cf_adjunction_unit:
  ―‹See Chapter IV-1 in \cite{mac_lane_categories_2010}.›
  assumes "x ∈∘ ℭ⦇Obj⦈" and "f : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
  shows 
    "𝔊⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ ηC Φ⦇NTMap⦈⦇x⦈ =
      (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)⦇ArrVal⦈⦇f⦈"
proof-
  from assms(1) have "𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ 𝔉⦇ObjMap⦈⦇x⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from cf_adj_Comp_commute_RL[OF assms(1) this assms(2)] assms show ?thesis
    by
      (
        cs_prems cs_shallow 
          cs_simp: 
            cat_cs_simps
            is_cf_adjunction.cf_adjunction_unit_NTMap_app[symmetric]
          cs_intro: adj_cs_intros
      )
qed

lemma (in is_cf_adjunction) cf_adj_AdjNT_cf_adjunction_counit:
  ―‹See Chapter IV-1 in \cite{mac_lane_categories_2010}.›
  assumes "x ∈∘ 𝔇⦇Obj⦈" and "g : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇x⦈"
  shows
    "εC Φ⦇NTMap⦈⦇x⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇g⦈ =
      (Φ⦇AdjNT⦈⦇NTMap⦈⦇a, x⦈∙)¯C⇘cat_Set α⇙⦇ArrVal⦈⦇g⦈"
  using
    is_cf_adjunction.cf_adj_AdjNT_cf_adjunction_unit
      [
        OF is_cf_adjunction_op, 
        unfolded cat_op_simps cf_adjunction_unit_NTMap_op, 
        OF assms
      ]
    assms
  by (*slow*)
    (
      cs_prems
        cs_simp: cat_cs_simps cat_op_simps
        cs_intro:
          cat_cs_intros
          adj_cs_intros
          cat_op_intros
          cat_prod_cs_intros
    )

lemma (in is_cf_adjunction) cf_adj_counit_unit_app[adj_cs_simps]:
  ―‹See Chapter IV-1 in \cite{mac_lane_categories_2010}.›
  assumes "x ∈∘ 𝔇⦇Obj⦈" and "g : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇x⦈"
  shows "𝔊⦇ArrMap⦈⦇εC Φ⦇NTMap⦈⦇x⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇g⦈⦈ ∘A⇘ℭ⇙ ηC Φ⦇NTMap⦈⦇a⦈ = g"
proof-
  from assms(2) have a: "a ∈∘ ℭ⦇Obj⦈" by auto
  from assms have inv_Φ_g: 
    "(Φ⦇AdjNT⦈⦇NTMap⦈⦇a, x⦈∙)¯C⇘cat_Set α⇙⦇ArrVal⦈⦇g⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ x"
    by (*slow*)
      (
        cs_concl 
          cs_simp: cat_cs_simps cat_op_simps
          cs_intro:
            cat_arrow_cs_intros
            cat_cs_intros
            adj_cs_intros
            cat_prod_cs_intros
            cat_op_intros
      )
  from assms show ?thesis
    unfolding
      cf_adj_AdjNT_cf_adjunction_counit[OF assms]
      cf_adj_AdjNT_cf_adjunction_unit[OF a inv_Φ_g]
    by (*slow*)
      (
        cs_concl 
          cs_simp: cat_cs_simps cat_op_simps
          cs_intro:
            cat_arrow_cs_intros 
            cat_cs_intros 
            adj_cs_intros 
            cat_prod_cs_intros 
            cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_cf_adjunction.cf_adj_counit_unit_app

lemma (in is_cf_adjunction) cf_adj_unit_counit_app[adj_cs_simps]:
  ―‹See Chapter IV-1 in \cite{mac_lane_categories_2010}.›
  assumes "x ∈∘ ℭ⦇Obj⦈" and "f : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
  shows "εC Φ⦇NTMap⦈⦇a⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ ηC Φ⦇NTMap⦈⦇x⦈⦈ = f"
proof-
  from assms(2) have a: "a ∈∘ 𝔇⦇Obj⦈" by auto
  from assms have Φ_f: 
    "(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈∙)⦇ArrVal⦈⦇f⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇a⦈"
    by
      (
        cs_concl 
          cs_simp: cat_cs_simps cat_op_simps 
          cs_intro:
            cat_arrow_cs_intros
            cat_cs_intros 
            adj_cs_intros
            cat_prod_cs_intros
            cat_op_intros
      )
  from assms show ?thesis
    unfolding
      cf_adj_AdjNT_cf_adjunction_unit[OF assms]
      cf_adj_AdjNT_cf_adjunction_counit[OF a Φ_f]
    by
      (
        cs_concl 
          cs_simp: cat_cs_simps cat_op_simps
          cs_intro: 
            cat_arrow_cs_intros
            cat_cs_intros
            adj_cs_intros
            cat_prod_cs_intros
            cat_op_intros
      )
qed

lemmas [cat_cs_simps] = is_cf_adjunction.cf_adj_unit_counit_app



subsection‹Counit-unit equations›


text‹
The following equations appear as part of the statement of 
Theorem 1 in Chapter IV-1 in cite‹"mac_lane_categories_2010"›.
These equations also appear in cite‹"noauthor_wikipedia_2001"›,
where they are named ‹counit-unit equations›.
›

lemma (in is_cf_adjunction) cf_adjunction_counit_unit:
  "(𝔊 ∘CF-NTCF εC Φ) ∙NTCF (ηC Φ ∘NTCF-CF 𝔊) = ntcf_id 𝔊"
  (is ‹(𝔊 ∘CF-NTCF ?ε) ∙NTCF (?η ∘NTCF-CF 𝔊) = ntcf_id 𝔊›)
proof(rule ntcf_eqI)
  from is_cf_adjunction_axioms show 
    "(𝔊 ∘CF-NTCF ?ε) ∙NTCF (?η ∘NTCF-CF 𝔊) : 𝔊 ↦CF 𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
  show "ntcf_id 𝔊 : 𝔊 ↦CF 𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    by (rule is_functor.cf_ntcf_id_is_ntcf[OF RL.is_functor_axioms])
  from is_cf_adjunction_axioms have dom_lhs:
    "𝒟∘ (((𝔊 ∘CF-NTCF ?ε) ∙NTCF (?η ∘NTCF-CF 𝔊))⦇NTMap⦈) = 𝔇⦇Obj⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros
      )
  from is_cf_adjunction_axioms have dom_rhs: "𝒟∘ (ntcf_id 𝔊⦇NTMap⦈) = 𝔇⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: adj_cs_intros)
  show "((𝔊 ∘CF-NTCF ?ε) ∙NTCF (?η ∘NTCF-CF 𝔊))⦇NTMap⦈ = ntcf_id 𝔊⦇NTMap⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    fix a assume prems: "a ∈∘ 𝔇⦇Obj⦈"
    let ?φ_aa = ‹Φ⦇AdjNT⦈⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇a⦈, a⦈∙›
    have "category α (cat_Set α)"
      by (rule category_cat_Set)
    from is_cf_adjunction_axioms prems
      L.category_axioms R.category_axioms (*speedup*)
      L.category_op R.category_op (*speedup*)
      LR.is_functor_axioms RL.is_functor_axioms (*speedup*)
      category_cat_Set (*speedup*)
    have
      "?φ_aa⦇ArrVal⦈⦇?ε⦇NTMap⦈⦇a⦈⦈ =
        (?φ_aa ∘A⇘cat_Set α⇙ ?φ_aa¯C⇘cat_Set α⇙)⦇ArrVal⦈⦇ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈⦈"
      by 
        (
          cs_concl cs_shallow
            cs_simp: 
              𝒵.cat_Set_Comp_ArrVal 
              cat_Set_the_inverse[symmetric] 
              cat_cs_simps adj_cs_simps cat_prod_cs_simps 
            cs_intro:
              cat_arrow_cs_intros 
              cat_cs_intros 
              cat_op_intros 
              adj_cs_intros 
              cat_prod_cs_intros
        )
    also from 
      is_cf_adjunction_axioms prems 
      L.category_axioms R.category_axioms (*speedup*)
      L.category_op R.category_op (*speedup*)
      LR.is_functor_axioms RL.is_functor_axioms (*speedup*)
      category_cat_Set (*speedup*)   
    have "… = ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈"
      by 
        (
          cs_concl
            cs_simp: 
              cat_cs_simps
              cat_Set_components(1)
              category.cat_the_inverse_Comp_CId
            cs_intro:
              cat_arrow_cs_intros
              cat_cs_intros
              cat_op_intros
              cat_prod_cs_intros
        )
    finally have [cat_cs_simps]: 
      "?φ_aa⦇ArrVal⦈⦇?ε⦇NTMap⦈⦇a⦈⦈ = ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈"
      by simp
    from 
      prems is_cf_adjunction_axioms 
      L.category_axioms R.category_axioms (*speedup*)
    show "((𝔊 ∘CF-NTCF ?ε) ∙NTCF (?η ∘NTCF-CF 𝔊))⦇NTMap⦈⦇a⦈ = ntcf_id 𝔊⦇NTMap⦈⦇a⦈"
      by
        (
          cs_concl
            cs_simp:
              cat_Set_the_inverse[symmetric]
              cf_adj_Comp_commute_RL
              cat_cs_simps
              adj_cs_simps
              cat_prod_cs_simps
              cat_op_simps
            cs_intro:
              cat_arrow_cs_intros
              cat_cs_intros
              adj_cs_intros
              cat_prod_cs_intros
              cat_op_intros
        )

  qed (auto intro: cat_cs_intros)

qed simp_all

lemmas [adj_cs_simps] = is_cf_adjunction.cf_adjunction_counit_unit

lemma (in is_cf_adjunction) cf_adjunction_unit_counit:
  "(εC Φ ∘NTCF-CF 𝔉) ∙NTCF (𝔉 ∘CF-NTCF ηC Φ) = ntcf_id 𝔉"
  (is ‹(?ε ∘NTCF-CF 𝔉) ∙NTCF (𝔉 ∘CF-NTCF ?η) = ntcf_id 𝔉›)
proof-
  from is_cf_adjunction_axioms have 𝔉η:
    "𝔉 ∘CF-NTCF ?η : 𝔉 ↦CF 𝔉 ∘CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
  from is_cf_adjunction_axioms have ε𝔉:
    "?ε ∘NTCF-CF 𝔉 : 𝔉 ∘CF 𝔊 ∘CF 𝔉 ↦CF 𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
  from 𝔉η ε𝔉 have ε𝔉_𝔉η: 
    "(?ε ∘NTCF-CF 𝔉) ∙NTCF (𝔉 ∘CF-NTCF ?η) : 𝔉 ↦CF 𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  from 
    is_cf_adjunction.cf_adjunction_counit_unit[
      OF is_cf_adjunction_op, 
      unfolded 
        op_ntcf_cf_adjunction_unit[symmetric]
        op_ntcf_cf_adjunction_counit[symmetric]
        op_ntcf_cf_ntcf_comp[symmetric]
        op_ntcf_ntcf_cf_comp[symmetric]
        op_ntcf_ntcf_vcomp[symmetric]
        op_ntcf_ntcf_vcomp[symmetric, OF ε𝔉 𝔉η]
        LR.cf_ntcf_id_op_cf
      ]
  have 
    "op_ntcf (op_ntcf ((?ε ∘NTCF-CF 𝔉) ∙NTCF (𝔉 ∘CF-NTCF ?η))) =
      op_ntcf (op_ntcf (ntcf_id 𝔉))"
    by simp
  from this is_cf_adjunction_axioms ε𝔉_𝔉η show ?thesis
    by 
      (
        cs_prems cs_shallow 
          cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_prod_cs_intros 
      )
qed

lemmas [adj_cs_simps] = is_cf_adjunction.cf_adjunction_unit_counit



subsection‹
Construction of an adjunction from universal morphisms 
from objects to functors
›


text‹
The subsection presents the construction of an adjunction given 
a structured collection of universal morphisms from objects to functors.
The content of this subsection follows the statement and the proof
of Theorem 2-i in Chapter IV-1 in cite‹"mac_lane_categories_2010"›.
›


subsubsection‹
The natural transformation associated with the adjunction
constructed from universal morphisms from objects to functors
›

definition cf_adjunction_AdjNT_of_unit :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η =
    [
      (λcd∈∘(op_cat (𝔉⦇HomDom⦈) ×C 𝔉⦇HomCod⦈)⦇Obj⦈.
        umap_of 𝔊 (cd⦇0⦈) (𝔉⦇ObjMap⦈⦇cd⦇0⦈⦈) (η⦇NTMap⦈⦇cd⦇0⦈⦈) (cd⦇1ℕ⦈)),
      HomO.C⇘α⇙𝔉⦇HomCod⦈(𝔉-,-),
      HomO.C⇘α⇙𝔉⦇HomDom⦈(-,𝔊-),
      op_cat (𝔉⦇HomDom⦈) ×C (𝔉⦇HomCod⦈),
      cat_Set α
    ]∘"


text‹Components.›

lemma cf_adjunction_AdjNT_of_unit_components:
  shows "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈ =
    (
      λcd∈∘(op_cat (𝔉⦇HomDom⦈) ×C 𝔉⦇HomCod⦈)⦇Obj⦈.
        umap_of 𝔊 (cd⦇0⦈) (𝔉⦇ObjMap⦈⦇cd⦇0⦈⦈) (η⦇NTMap⦈⦇cd⦇0⦈⦈)  (cd⦇1ℕ⦈)
    )"
    and "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTDom⦈ = HomO.C⇘α⇙𝔉⦇HomCod⦈(𝔉-,-)"
    and "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTCod⦈ = HomO.C⇘α⇙𝔉⦇HomDom⦈(-,𝔊-)"
    and "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTDGDom⦈ =
      op_cat (𝔉⦇HomDom⦈) ×C (𝔉⦇HomCod⦈)"
    and "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTDGCod⦈ = cat_Set α"
  unfolding cf_adjunction_AdjNT_of_unit_def nt_field_simps
  by (simp_all add: nat_omega_simps)


subsubsection‹Natural transformation map›

lemma cf_adjunction_AdjNT_of_unit_NTMap_vsv[adj_cs_intros]:
  "vsv (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈)"
  unfolding cf_adjunction_AdjNT_of_unit_components by simp

lemma cf_adjunction_AdjNT_of_unit_NTMap_vdomain[adj_cs_simps]:
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
  shows "𝒟∘ (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈) = (op_cat ℭ ×C 𝔇)⦇Obj⦈"
proof-
  interpret is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
  show ?thesis 
    unfolding cf_adjunction_AdjNT_of_unit_components 
    by (simp add: cat_cs_simps)
qed

lemma cf_adjunction_AdjNT_of_unit_NTMap_app[adj_cs_simps]:
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇" and "c ∈∘ ℭ⦇Obj⦈" and "d ∈∘ 𝔇⦇Obj⦈"
  shows 
    "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇c, d⦈∙ =
      umap_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈) d"
proof-
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
  from assms have "[c, d]∘ ∈∘ (op_cat ℭ ×C 𝔇)⦇Obj⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_prod_cs_intros
      )
  then show "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈ ⦇c, d⦈∙ = 
    umap_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈) d"
    unfolding cf_adjunction_AdjNT_of_unit_components 
    by (simp add: nat_omega_simps cat_cs_simps)
qed

lemma cf_adjunction_AdjNT_of_unit_NTMap_vrange:
  assumes "category α ℭ"
    and "category α 𝔇"
    and "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "η : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
  shows "ℛ∘ (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈) ⊆∘ cat_Set α⦇Arr⦈"
proof-
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
  show ?thesis
  proof
    (
      rule vsv.vsv_vrange_vsubset, 
      unfold cf_adjunction_AdjNT_of_unit_NTMap_vdomain[OF assms(3)]
    )
    show "vsv (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈)" 
      by (intro adj_cs_intros)
    fix cd assume prems: "cd ∈∘ (op_cat ℭ ×C 𝔇)⦇Obj⦈"
    then obtain c d where cd_def: "cd = [c, d]∘"
      and c: "c ∈∘ ℭ⦇Obj⦈"
      and d: "d ∈∘ 𝔇⦇Obj⦈"
      by 
        (
          auto 
            simp: cat_op_simps 
            elim: 
              cat_prod_2_ObjE[OF 𝔉.HomDom.category_op 𝔉.HomCod.category_axioms]
        )
    from assms c d show 
      "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇cd⦈ ∈∘ cat_Set α⦇Arr⦈"
      unfolding cd_def
      by 
        (
          cs_concl  
            cs_simp: cat_cs_simps adj_cs_simps cs_intro: cat_cs_intros
        )
  qed
qed


subsubsection‹
Adjunction constructed from universal morphisms 
from objects to functors is an adjunction
›

lemma cf_adjunction_AdjNT_of_unit_is_ntcf:
  assumes "category α ℭ"
    and "category α 𝔇"
    and "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "η : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
  shows "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η :
    HomO.C⇘α⇙𝔇(𝔉-,-) ↦CF HomO.C⇘α⇙ℭ(-,𝔊-) :
    op_cat ℭ ×C 𝔇 ↦↦C⇘α⇙ cat_Set α"
proof-

  interpret ℭ: category α ℭ by (rule assms(1))
  interpret 𝔇: category α 𝔇 by (rule assms(2))
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
  interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
  interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘CF 𝔉› η by (rule assms(5))

  show ?thesis
  proof(intro is_ntcfI')

    show "vfsequence (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η)"
      unfolding cf_adjunction_AdjNT_of_unit_def by simp
    show "vcard (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η) = 5ℕ"
      unfolding cf_adjunction_AdjNT_of_unit_def by (simp add: nat_omega_simps)
    from assms(2,3) show 
      "HomO.C⇘α⇙𝔇(𝔉-,-) : op_cat ℭ ×C 𝔇 ↦↦C⇘α⇙ cat_Set α"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    from assms show "HomO.C⇘α⇙ℭ(-,𝔊-) : op_cat ℭ ×C 𝔇 ↦↦C⇘α⇙ cat_Set α"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    show "vsv (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈)" 
      by (intro adj_cs_intros)
    from assms show 
      "𝒟∘ (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈) = (op_cat ℭ ×C 𝔇)⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps adj_cs_simps)

    show "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇cd⦈ :
      HomO.C⇘α⇙𝔇(𝔉-,-)⦇ObjMap⦈⦇cd⦈ ↦⇘cat_Set α⇙
      HomO.C⇘α⇙ℭ(-,𝔊-)⦇ObjMap⦈⦇cd⦈"
      if "cd ∈∘ (op_cat ℭ ×C 𝔇)⦇Obj⦈" for cd
    proof-
      from that obtain c d 
        where cd_def: "cd = [c, d]∘" and c: "c ∈∘ ℭ⦇Obj⦈" and d: "d ∈∘ 𝔇⦇Obj⦈"
        by 
          (
            auto 
              simp: cat_op_simps 
              elim: cat_prod_2_ObjE[OF ℭ.category_op 𝔇.category_axioms]
          )
      from assms c d show ?thesis
        unfolding cd_def
        by 
          (
            cs_concl cs_shallow
              cs_simp: adj_cs_simps cat_cs_simps cat_op_simps 
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed

    show 
      "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇c'd'⦈ ∘A⇘cat_Set α⇙
        HomO.C⇘α⇙𝔇(𝔉-,-)⦇ArrMap⦈⦇gf⦈ =
          HomO.C⇘α⇙ℭ(-,𝔊-)⦇ArrMap⦈⦇gf⦈ ∘A⇘cat_Set α⇙
            cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇cd⦈"
      if "gf : cd ↦⇘op_cat ℭ ×C 𝔇⇙ c'd'" for cd c'd' gf 
    proof-
      from that obtain g f c c' d d'
        where gf_def: "gf = [g, f]∘"
          and cd_def: "cd = [c, d]∘"
          and c'd'_def: "c'd' = [c', d']∘"
          and g: "g : c' ↦⇘ℭ⇙ c" 
          and f: "f : d ↦⇘𝔇⇙ d'"
        by 
          (
            auto 
              simp: cat_op_simps 
              elim: cat_prod_2_is_arrE[OF ℭ.category_op 𝔇.category_axioms]
          ) 
      from assms g f that show ?thesis
        unfolding gf_def cd_def c'd'_def
        by 
          (
            cs_concl 
              cs_simp: cf_umap_of_cf_hom_unit_commute adj_cs_simps cat_cs_simps
              cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
          )
    qed

  qed (auto simp: cf_adjunction_AdjNT_of_unit_components cat_cs_simps)

qed

lemma cf_adjunction_AdjNT_of_unit_is_ntcf'[adj_cs_intros]:
  assumes "category α ℭ"
    and "category α 𝔇"
    and "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "η : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
    and "𝔖 = HomO.C⇘α⇙𝔇(𝔉-,-)"
    and "𝔖' = HomO.C⇘α⇙ℭ(-,𝔊-)"
    and "𝔄 = op_cat ℭ ×C 𝔇"
    and "𝔅 = cat_Set α"
  shows "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η : 𝔖 ↦CF 𝔖' : 𝔄 ↦↦C⇘α⇙ 𝔅"
  using assms(1-5) unfolding assms(6-9) 
  by (rule cf_adjunction_AdjNT_of_unit_is_ntcf)


subsubsection‹
Adjunction constructed from universal morphisms from objects to functors
›

definition cf_adjunction_of_unit :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "cf_adjunction_of_unit α 𝔉 𝔊 η =
    [𝔉, 𝔊, cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η]∘"


text‹Components.›

lemma cf_adjunction_of_unit_components:
  shows [adj_cs_simps]: "cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjLeft⦈ = 𝔉"
    and [adj_cs_simps]: "cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjRight⦈ = 𝔊"
    and "cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjNT⦈ =
      cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η"
  unfolding cf_adjunction_of_unit_def adj_field_simps
  by (simp_all add: nat_omega_simps)


text‹Natural transformation map.›

lemma cf_adjunction_of_unit_AdjNT_NTMap_vdomain[adj_cs_simps]:
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
  shows "𝒟∘ (cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjNT⦈⦇NTMap⦈) = 
    (op_cat ℭ ×C 𝔇)⦇Obj⦈"
  using assms 
  unfolding cf_adjunction_of_unit_components(3)
  by (rule cf_adjunction_AdjNT_of_unit_NTMap_vdomain)

lemma cf_adjunction_of_unit_AdjNT_NTMap_app[adj_cs_simps]:
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇" and "c ∈∘ ℭ⦇Obj⦈" and "d ∈∘ 𝔇⦇Obj⦈"
  shows 
    "cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjNT⦈⦇NTMap⦈⦇c, d⦈∙ =
      umap_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈) d"
  using assms 
  unfolding cf_adjunction_of_unit_components(3)
  by (rule cf_adjunction_AdjNT_of_unit_NTMap_app)


text‹
The adjunction constructed from universal morphisms from objects to 
functors is an adjunction.
›

lemma cf_adjunction_of_unit_is_cf_adjunction:
  assumes "category α ℭ"
    and "category α 𝔇"
    and "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "η : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
    and "⋀x. x ∈∘ ℭ⦇Obj⦈ ⟹ universal_arrow_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈)"
  shows "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    and "ηC (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
proof-

  interpret ℭ: category α ℭ by (rule assms(1))
  interpret 𝔇: category α 𝔇 by (rule assms(2))
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
  interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
  interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘CF 𝔉› η by (rule assms(5))

  show caou_η: "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
  proof
    (
      intro 
        is_cf_adjunctionI[OF _ _ assms(1-4)] 
        is_iso_ntcf_if_bnt_proj_snd_is_iso_ntcf[
          OF ℭ.category_op 𝔇.category_axioms
          ],
      unfold cat_op_simps cf_adjunction_of_unit_components
    )
    show caou_η: "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η :
      HomO.C⇘α⇙𝔇(𝔉-,-) ↦CF HomO.C⇘α⇙ℭ(-,𝔊-) :
      op_cat ℭ ×C 𝔇 ↦↦C⇘α⇙ cat_Set α"
      unfolding cf_adjunction_of_unit_components
      by (rule cf_adjunction_AdjNT_of_unit_is_ntcf[OF assms(1-5)])
    fix a assume prems: "a ∈∘ ℭ⦇Obj⦈"
    have ua_of_ηa:
      "ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈) :
        HomO.C⇘α⇙𝔇(𝔉⦇ObjMap⦈⦇a⦈,-) ↦CF.iso HomO.C⇘α⇙ℭ(a,-) ∘CF 𝔊 :
        𝔇 ↦↦C⇘α⇙ cat_Set α"
      by 
        (
          rule is_functor.cf_ntcf_ua_of_is_iso_ntcf[
            OF assms(4) assms(6)[OF prems]
            ]
        )
    have [adj_cs_simps]:
      "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)NTCF =
        ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈)"
    proof(rule ntcf_eqI)
      from assms(1-5) caou_η prems show lhs: 
        "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)NTCF :
          HomO.C⇘α⇙𝔇(𝔉⦇ObjMap⦈⦇a⦈,-) ↦CF HomO.C⇘α⇙ℭ(a,-) ∘CF 𝔊 :
          𝔇 ↦↦C⇘α⇙ cat_Set α"
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_op_simps 
              cs_intro: cat_cs_intros cat_op_intros
          )
      from ua_of_ηa show rhs:
        "ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈) :
          HomO.C⇘α⇙𝔇(𝔉⦇ObjMap⦈⦇a⦈,-) ↦CF HomO.C⇘α⇙ℭ(a,-) ∘CF 𝔊 :
          𝔇 ↦↦C⇘α⇙ cat_Set α"
        by (cs_concl cs_shallow cs_intro: ntcf_cs_intros)
      from lhs have dom_lhs:
        "𝒟∘ ((cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)NTCF)⦇NTMap⦈) =
          𝔇⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      from lhs assms(4) have dom_rhs:
        "𝒟∘ (ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈)⦇NTMap⦈) = 𝔇⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      show 
        "(cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)NTCF)⦇NTMap⦈ =
          ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈)⦇NTMap⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix d assume prems': "d ∈∘ 𝔇⦇Obj⦈"
        from assms(3,4) prems prems' show 
          "(cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)NTCF)⦇NTMap⦈⦇d⦈ =
            ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈)⦇NTMap⦈⦇d⦈"
          by (cs_concl cs_shallow cs_simp: adj_cs_simps cat_cs_simps)
      qed (simp_all add: bnt_proj_snd_NTMap_vsv 𝔊.ntcf_ua_of_NTMap_vsv)
    qed simp_all
    from assms(1-5) assms(6)[OF prems] prems show 
      "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)NTCF :
        HomO.C⇘α⇙𝔇(𝔉-,-)⇘op_cat ℭ,𝔇⇙(a,-)CF ↦CF.iso
        HomO.C⇘α⇙ℭ(-,𝔊-)⇘op_cat ℭ,𝔇⇙(a,-)CF :
        𝔇 ↦↦C⇘α⇙ cat_Set α"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: adj_cs_simps cat_cs_simps cs_intro: cat_cs_intros
        )
  qed (auto simp: cf_adjunction_of_unit_def nat_omega_simps)

  show "ηC (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
  proof(rule ntcf_eqI)
    from caou_η show lhs:
      "ηC (cf_adjunction_of_unit α 𝔉 𝔊 η) :
        cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
      by (cs_concl cs_shallow cs_intro: adj_cs_intros)
    show rhs: "η : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
      by (auto intro: cat_cs_intros)
    from lhs have dom_lhs:
      "𝒟∘ (ηC (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈) = ℭ⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    have dom_rhs: "𝒟∘ (η⦇NTMap⦈) = ℭ⦇Obj⦈" by (auto simp: cat_cs_simps)
    show "ηC (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈ = η⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume prems: "a ∈∘ ℭ⦇Obj⦈"
      from assms(1-5) prems caou_η show 
        "ηC (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈⦇a⦈ = η⦇NTMap⦈⦇a⦈"
        by 
          (
            cs_concl cs_shallow
              cs_simp: 
                adj_cs_simps cat_cs_simps cf_adjunction_of_unit_components(3) 
              cs_intro: cat_cs_intros
          )
    qed (auto intro: adj_cs_intros)
  qed simp_all

qed



subsection‹
Construction of an adjunction from a functor and universal morphisms 
from objects to functors
›


text‹
The subsection presents the construction of an adjunction given 
a functor and a structured collection of universal morphisms 
from objects to functors.
The content of this subsection follows the statement and the proof
of Theorem 2-ii in Chapter IV-1 in cite‹"mac_lane_categories_2010"›.
›


subsubsection‹Left adjoint›

definition cf_la_of_ra :: "(V ⇒ V) ⇒ V ⇒ V ⇒ V"
  where "cf_la_of_ra F 𝔊 η =
    [
      (λx∈∘𝔊⦇HomCod⦈⦇Obj⦈. F x),
      (
        λh∈∘𝔊⦇HomCod⦈⦇Arr⦈. THE f'.
          f' : F (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈) ↦⇘𝔊⦇HomDom⦈⇙ F (𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈) ∧
            η⦇𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈⦈ ∘A⇘𝔊⦇HomCod⦈⇙ h =
              (
                umap_of
                  𝔊
                  (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈)
                  (F (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈))
                  (η⦇𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈⦈)
                  (F (𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈))
              )⦇ArrVal⦈⦇f'⦈
      ),
      𝔊⦇HomCod⦈,
      𝔊⦇HomDom⦈
    ]∘"


text‹Components.›

lemma cf_la_of_ra_components:
  shows "cf_la_of_ra F 𝔊 η⦇ObjMap⦈ = (λx∈∘𝔊⦇HomCod⦈⦇Obj⦈. F x)"
    and "cf_la_of_ra F 𝔊 η⦇ArrMap⦈ =
      (
        λh∈∘𝔊⦇HomCod⦈⦇Arr⦈. THE f'.
          f' : F (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈) ↦⇘𝔊⦇HomDom⦈⇙ F (𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈) ∧
          η⦇𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈⦈ ∘A⇘𝔊⦇HomCod⦈⇙ h =
            (
              umap_of
                𝔊 
                (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈)
                (F (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈))
                (η⦇𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈⦈)
                (F (𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈))
            )⦇ArrVal⦈⦇f'⦈
      )"
    and "cf_la_of_ra F 𝔊 η⦇HomDom⦈ = 𝔊⦇HomCod⦈"
    and "cf_la_of_ra F 𝔊 η⦇HomCod⦈ = 𝔊⦇HomDom⦈"
  unfolding cf_la_of_ra_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda cf_la_of_ra_components(1)
  |vsv cf_la_of_ra_ObjMap_vsv[adj_cs_intros]|

mk_VLambda (in is_functor) 
  cf_la_of_ra_components(1)[where ?𝔊=𝔉, unfolded cf_HomCod]
  |vdomain cf_la_of_ra_ObjMap_vdomain[adj_cs_simps]|
  |app cf_la_of_ra_ObjMap_app[adj_cs_simps]|

lemmas [adj_cs_simps] =
  is_functor.cf_la_of_ra_ObjMap_vdomain
  is_functor.cf_la_of_ra_ObjMap_app
  

subsubsection‹Arrow map›

mk_VLambda cf_la_of_ra_components(2)
  |vsv cf_la_of_ra_ArrMap_vsv[adj_cs_intros]|

mk_VLambda (in is_functor) 
  cf_la_of_ra_components(2)[where ?𝔊=𝔉, unfolded cf_HomCod cf_HomDom]
  |vdomain cf_la_of_ra_ArrMap_vdomain[adj_cs_simps]|
  |app cf_la_of_ra_ArrMap_app| (*not for general use*)

lemmas [adj_cs_simps] = is_functor.cf_la_of_ra_ArrMap_vdomain

lemma (in is_functor) cf_la_of_ra_ArrMap_app':
  assumes "h : a ↦⇘𝔅⇙ b"
  shows 
    "cf_la_of_ra F 𝔉 η⦇ArrMap⦈⦇h⦈ =
      (
        THE f'.
          f' : F a ↦⇘𝔄⇙ F b ∧
          η⦇b⦈ ∘A⇘𝔅⇙ h = umap_of 𝔉 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇f'⦈
      )"
proof-
  from assms have h: "h ∈∘ 𝔅⦇Arr⦈" by (simp add: cat_cs_intros)
  from assms have h_Dom: "𝔅⦇Dom⦈⦇h⦈ = a" and h_Cod: "𝔅⦇Cod⦈⦇h⦈ = b"
    by (simp_all add: cat_cs_simps)
  show ?thesis by (rule cf_la_of_ra_ArrMap_app[OF h, unfolded h_Dom h_Cod])
qed

lemma cf_la_of_ra_ArrMap_app_unique:
  assumes "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "f : a ↦⇘ℭ⇙ b"
    and "universal_arrow_of 𝔊 a (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇a⦈) (η⦇a⦈)"
    and "universal_arrow_of 𝔊 b (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈) (η⦇b⦈)"
  shows "cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ : F a ↦⇘𝔇⇙ F b"
    and "η⦇b⦈ ∘A⇘ℭ⇙ f = 
      umap_of 𝔊 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈⦈"
    and "⋀f'.
      ⟦
        f' : F a ↦⇘𝔇⇙ F b;
        η⦇b⦈ ∘A⇘ℭ⇙ f = umap_of 𝔊 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇f'⦈
      ⟧ ⟹ cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ = f'"
proof-

  interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(1))

  from assms(2) have a: "a ∈∘ ℭ⦇Obj⦈" and b: "b ∈∘ ℭ⦇Obj⦈" 
    by (simp_all add: cat_cs_intros)
  note ua_η_a = 𝔊.universal_arrow_ofD[OF assms(3)]
  note ua_η_b = 𝔊.universal_arrow_ofD[OF assms(4)]
  from ua_η_b(2) have [cat_cs_intros]: 
    "⟦ c = b; c' = 𝔊⦇ObjMap⦈⦇cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈⦈ ⟧ ⟹ η⦇b⦈ : c ↦⇘ℭ⇙ c'"
    for c c'
    by auto
  from assms(1,2) ua_η_a(2) have ηa_f:
    "η⦇b⦈ ∘A⇘ℭ⇙ f : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms(1,2) have lara_a: "cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇a⦈ = F a"
    and lara_b: "cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈ = F b"
    by (cs_concl cs_simp: adj_cs_simps cs_intro: cat_cs_intros)+

  from theD
    [
      OF 
        ua_η_a(3)[OF ua_η_b(1) ηa_f, unfolded lara_a lara_b] 
        𝔊.cf_la_of_ra_ArrMap_app'[OF assms(2), of F η]
    ]
  show "cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ : F a ↦⇘𝔇⇙ F b"
    and "η⦇b⦈ ∘A⇘ℭ⇙ f = umap_of
      𝔊 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈⦈"
    and "⋀f'.
      ⟦
        f' : F a ↦⇘𝔇⇙ F b;
        η⦇b⦈ ∘A⇘ℭ⇙ f = umap_of 𝔊 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇f'⦈
      ⟧ ⟹ cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ = f'"
    by blast+

qed

lemma cf_la_of_ra_ArrMap_app_is_arr[adj_cs_intros]:
  assumes "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "f : a ↦⇘ℭ⇙ b"
    and "universal_arrow_of 𝔊 a (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇a⦈) (η⦇a⦈)"
    and "universal_arrow_of 𝔊 b (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈) (η⦇b⦈)"
    and "Fa = F a"
    and "Fb = F b"
  shows "cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ : Fa ↦⇘𝔇⇙ Fb"
  using assms(1-4) unfolding assms(5,6) by (rule cf_la_of_ra_ArrMap_app_unique)


subsubsection‹
An adjunction constructed from a functor and universal morphisms 
from objects to functors is an adjunction
›

lemma cf_la_of_ra_is_functor:
  assumes "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ F c ∈∘ 𝔇⦇Obj⦈"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹
      universal_arrow_of 𝔊 c (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇c⦈) (η⦇c⦈)"
    and "⋀c c' h. h : c ↦⇘ℭ⇙ c' ⟹
      𝔊⦇ArrMap⦈⦇cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇h⦈⦈ ∘A⇘ℭ⇙ η⦇c⦈ = η⦇c'⦈ ∘A⇘ℭ⇙ h"
  shows "cf_la_of_ra F 𝔊 η : ℭ ↦↦C⇘α⇙ 𝔇" (is ‹?𝔉 : ℭ ↦↦C⇘α⇙ 𝔇›)
proof-

  interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(1))

  show "cf_la_of_ra F 𝔊 η : ℭ ↦↦C⇘α⇙ 𝔇"
  proof(rule is_functorI')

    show "vfsequence ?𝔉" unfolding cf_la_of_ra_def by auto
    show "vcard ?𝔉 = 4ℕ" 
      unfolding cf_la_of_ra_def by (simp add: nat_omega_simps)
    show "ℛ∘ (?𝔉⦇ObjMap⦈) ⊆∘ 𝔇⦇Obj⦈"
    proof(rule vsv.vsv_vrange_vsubset, unfold 𝔊.cf_la_of_ra_ObjMap_vdomain)
      fix x assume "x ∈∘ ℭ⦇Obj⦈"
      with assms(1) show "?𝔉⦇ObjMap⦈⦇x⦈ ∈∘ 𝔇⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: adj_cs_simps cs_intro: assms(2))
    qed (auto intro: adj_cs_intros)

    show "?𝔉⦇ArrMap⦈⦇f⦈ : ?𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ ?𝔉⦇ObjMap⦈⦇b⦈"
      if "f : a ↦⇘ℭ⇙ b" for a b f
    proof-
      from that have a: "a ∈∘ ℭ⦇Obj⦈" and b: "b ∈∘ ℭ⦇Obj⦈" 
        by (simp_all add: cat_cs_intros)
      have ua_η_a: "universal_arrow_of 𝔊 a (?𝔉⦇ObjMap⦈⦇a⦈) (η⦇a⦈)"
        and ua_η_b: "universal_arrow_of 𝔊 b (?𝔉⦇ObjMap⦈⦇b⦈) (η⦇b⦈)"
        by (intro assms(3)[OF a] assms(3)[OF b])+
      from a b cf_la_of_ra_ArrMap_app_unique(1)[OF assms(1) that ua_η_a ua_η_b] 
      show ?thesis 
        by (cs_concl cs_shallow cs_simp: adj_cs_simps)
    qed

    show "?𝔉⦇ArrMap⦈⦇g ∘A⇘ℭ⇙ f⦈ = ?𝔉⦇ArrMap⦈⦇g⦈ ∘A⇘𝔇⇙ ?𝔉⦇ArrMap⦈⦇f⦈"
      if "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b" for b c g a f
    proof-

      from that have a: "a ∈∘ ℭ⦇Obj⦈" and b: "b ∈∘ ℭ⦇Obj⦈" and c: "c ∈∘ ℭ⦇Obj⦈" 
        by (simp_all add: cat_cs_intros)
      from assms(1) that have gf: "g ∘A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

      note ua_η_a = assms(3)[OF a]
        and ua_η_b = assms(3)[OF b]
        and ua_η_c = assms(3)[OF c]

      note lara_f = 
        cf_la_of_ra_ArrMap_app_unique[OF assms(1) that(2) ua_η_a ua_η_b]
      note lara_g = 
        cf_la_of_ra_ArrMap_app_unique[OF assms(1) that(1) ua_η_b ua_η_c]
      note lara_gf = 
        cf_la_of_ra_ArrMap_app_unique[OF assms(1) gf ua_η_a ua_η_c]

      note ua_η_a = 𝔊.universal_arrow_ofD[OF ua_η_a]
        and ua_η_b = 𝔊.universal_arrow_ofD[OF ua_η_b]
        and ua_η_c = 𝔊.universal_arrow_ofD[OF ua_η_c]
      
      from ua_η_a(2) assms(1) that have ηa: 
        "η⦇a⦈ : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇F a⦈"
        by (cs_prems cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
      from ua_η_b(2) assms(1) that have ηb: 
        "η⦇b⦈ : b ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇F b⦈"
        by (cs_prems cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
      from ua_η_c(2) assms(1) that have ηc: 
        "η⦇c⦈ : c ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇F c⦈"
        by (cs_prems cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)

      from assms(1) that ηc have
        "η⦇c⦈ ∘A⇘ℭ⇙ (g ∘A⇘ℭ⇙ f) = (η⦇c⦈ ∘A⇘ℭ⇙ g) ∘A⇘ℭ⇙ f"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      also from assms(1) lara_g(1) that(2) ηb have 
        "… = 𝔊⦇ArrMap⦈⦇?𝔉⦇ArrMap⦈⦇g⦈⦈ ∘A⇘ℭ⇙ (η⦇b⦈ ∘A⇘ℭ⇙ f)"
        by 
          (
            cs_concl 
              cs_simp: lara_g(2) cat_cs_simps 
              cs_intro: cat_cs_intros cat_prod_cs_intros
          )
      also from assms(1) lara_f(1) ηa have "… =
        𝔊⦇ArrMap⦈⦇?𝔉⦇ArrMap⦈⦇g⦈⦈ ∘A⇘ℭ⇙ 
          (𝔊⦇ArrMap⦈⦇?𝔉⦇ArrMap⦈⦇f⦈⦈ ∘A⇘ℭ⇙ η⦇a⦈)"
        by (cs_concl cs_shallow cs_simp: lara_f(2) cat_cs_simps)
      finally have [symmetric, cat_cs_simps]: 
        "η⦇c⦈ ∘A⇘ℭ⇙ (g ∘A⇘ℭ⇙ f) = …".
      from assms(1) this ηa ηb ηc lara_g(1) lara_f(1) have 
        "η⦇c⦈ ∘A⇘ℭ⇙ (g ∘A⇘ℭ⇙ f) =
          umap_of 𝔊 a (F a) (η⦇a⦈) (F c)⦇ArrVal⦈⦇?𝔉⦇ArrMap⦈⦇g⦈ ∘A⇘𝔇⇙
          ?𝔉⦇ArrMap⦈⦇f⦈⦈"
        by 
          ( 
            cs_concl cs_shallow
              cs_simp: adj_cs_simps cat_cs_simps 
              cs_intro: adj_cs_intros cat_cs_intros
          )
      moreover from assms(1) lara_g(1) lara_f(1) have 
        "?𝔉⦇ArrMap⦈⦇g⦈ ∘A⇘𝔇⇙ ?𝔉⦇ArrMap⦈⦇f⦈ : F a ↦⇘𝔇⇙ F c"
        by (cs_concl cs_shallow cs_intro: adj_cs_intros cat_cs_intros)
      ultimately show ?thesis by (intro lara_gf(3))

    qed

    show "?𝔉⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = 𝔇⦇CId⦈⦇?𝔉⦇ObjMap⦈⦇c⦈⦈" if "c ∈∘ ℭ⦇Obj⦈" for c 
    proof-
      note lara_c = cf_la_of_ra_ArrMap_app_unique[
          OF 
            assms(1) 
            𝔊.HomCod.cat_CId_is_arr[OF that] 
            assms(3)[OF that] 
            assms(3)[OF that]
          ]
      from assms(1) that have 𝔇c: "𝔇⦇CId⦈⦇F c⦈ : F c ↦⇘𝔇⇙ F c "
        by (cs_concl cs_simp: cat_cs_simps cs_intro: assms(2) cat_cs_intros)
      from 𝔊.universal_arrow_ofD(2)[OF assms(3)[OF that]] assms(1) that have ηc: 
        "η⦇c⦈ : c ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇F c⦈"
        by (cs_prems cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
      from assms(1) that ηc have 
        "η⦇c⦈ ∘A⇘ℭ⇙ ℭ⦇CId⦈⦇c⦈ =
          umap_of 𝔊 c (F c) (η⦇c⦈) (F c)⦇ArrVal⦈⦇𝔇⦇CId⦈⦇F c⦈⦈"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: assms(2) cat_cs_intros)
      note [cat_cs_simps] = lara_c(3)[OF 𝔇c this]
      from assms(1) that 𝔇c show ?thesis
        by 
          (
            cs_concl cs_shallow 
              cs_simp: adj_cs_simps cat_cs_simps cs_intro: cat_cs_intros
          )
    qed
  qed (auto simp: cf_la_of_ra_components cat_cs_intros cat_cs_simps)

qed

lemma cf_la_of_ra_is_ntcf:  
  fixes F ℭ 𝔉 𝔊 ηm η
  defines "𝔉 ≡ cf_la_of_ra F 𝔊 ηm"
    and "η ≡ [ηm, cf_id ℭ, 𝔊 ∘CF 𝔉, ℭ, ℭ]∘"
  assumes "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ F c ∈∘ 𝔇⦇Obj⦈"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ universal_arrow_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈)"
    and "⋀c c' h. h : c ↦⇘ℭ⇙ c' ⟹
      𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇h⦈⦈ ∘A⇘ℭ⇙ (η⦇NTMap⦈⦇c⦈) = (η⦇NTMap⦈⦇c'⦈) ∘A⇘ℭ⇙ h"
    and "vsv (η⦇NTMap⦈)"
    and "𝒟∘ (η⦇NTMap⦈) = ℭ⦇Obj⦈"
  shows "η : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
proof-
  interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(3))
  have η_components: 
    "η⦇NTMap⦈ = ηm"
    "η⦇NTDom⦈ = cf_id ℭ"
    "η⦇NTCod⦈ = 𝔊 ∘CF 𝔉"
    "η⦇NTDGDom⦈ = ℭ"
    "η⦇NTDGCod⦈ = ℭ"
    unfolding η_def nt_field_simps by (simp_all add: nat_omega_simps)
  note 𝔉_def = 𝔉_def[folded η_components(1)]
  have 𝔉: "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    unfolding 𝔉_def
    by (auto intro: cf_la_of_ra_is_functor[OF assms(3-6)[unfolded 𝔉_def]])
  show "η : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
  proof(rule is_ntcfI')
    show "vfsequence η" unfolding η_def by simp
    show "vcard η = 5ℕ" unfolding η_def by (simp_all add: nat_omega_simps)
    from assms(2) show "cf_id ℭ : ℭ ↦↦C⇘α⇙ ℭ"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms(2) 𝔉 show "𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show "η⦇NTMap⦈⦇a⦈ : cf_id ℭ⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (𝔊 ∘CF 𝔉)⦇ObjMap⦈⦇a⦈"
      if "a ∈∘ ℭ⦇Obj⦈" for a
      using assms(2) 𝔉 that 𝔊.universal_arrow_ofD(2)[OF assms(5)[OF that]]
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    show 
      "η⦇NTMap⦈⦇b⦈ ∘A⇘ℭ⇙ cf_id ℭ⦇ArrMap⦈⦇f⦈ =
        (𝔊 ∘CF 𝔉)⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ η⦇NTMap⦈⦇a⦈"
      if "f : a ↦⇘ℭ⇙ b" for a b f
      using assms(3) 𝔉 that 
      by 
        (
          cs_concl cs_shallow 
            cs_simp: assms(6) cat_cs_simps cs_intro: cat_cs_intros
        )
  qed (auto simp: η_components(2-5) assms(7-8))
qed

lemma cf_la_of_ra_is_unit:  
  fixes F ℭ 𝔉 𝔊 ηm η
  defines "𝔉 ≡ cf_la_of_ra F 𝔊 ηm"
    and "η ≡ [ηm, cf_id ℭ, 𝔊 ∘CF 𝔉, ℭ, ℭ]∘"
  assumes "category α ℭ"
    and "category α 𝔇"
    and "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹ F c ∈∘ 𝔇⦇Obj⦈"
    and "⋀c. c ∈∘ ℭ⦇Obj⦈ ⟹
      universal_arrow_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈)"
    and "⋀c c' h. h : c ↦⇘ℭ⇙ c' ⟹
      𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇h⦈⦈ ∘A⇘ℭ⇙ (η⦇NTMap⦈⦇c⦈) = (η⦇NTMap⦈⦇c'⦈) ∘A⇘ℭ⇙ h"
    and "vsv (η⦇NTMap⦈)"
    and "𝒟∘ (η⦇NTMap⦈) = ℭ⦇Obj⦈"
  shows "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    and "ηC (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
proof-
  have η_components: 
    "η⦇NTMap⦈ = ηm"
    "η⦇NTDom⦈ = cf_id ℭ"
    "η⦇NTCod⦈ = 𝔊 ∘CF 𝔉"
    "η⦇NTDGDom⦈ = ℭ"
    "η⦇NTDGCod⦈ = ℭ"
    unfolding η_def nt_field_simps by (simp_all add: nat_omega_simps)
  note 𝔉_def = 𝔉_def[folded η_components(1)]
  note 𝔉 = cf_la_of_ra_is_functor
    [
      where F=F and ℭ=ℭ and 𝔊=𝔊 and η=ηm, 
      folded 𝔉_def[unfolded η_components(1)], 
      folded η_components(1),
      OF assms(5-8),
      simplified
    ]
  note η = cf_la_of_ra_is_ntcf
    [
      where F=F and ℭ=ℭ and 𝔊=𝔊 and ηm=ηm, 
      folded 𝔉_def[unfolded η_components(1)], 
      folded η_def, 
      OF assms(5-10),
      simplified
    ]
  show "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    and "ηC (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
    by 
      (
        intro cf_adjunction_of_unit_is_cf_adjunction[
          OF assms(3,4) 𝔉 assms(5) η assms(7), simplified, folded 𝔉_def
          ]
      )+
qed



subsection‹
Construction of an adjunction from universal morphisms 
from functors to objects
›


subsubsection‹Definition and elementary properties›


text‹
The subsection presents the construction of an adjunction given 
a structured collection of universal morphisms from functors to objects.
The content of this subsection follows the statement and the proof
of Theorem 2-iii in Chapter IV-1 in cite‹"mac_lane_categories_2010"›.
›

definition cf_adjunction_of_counit :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "cf_adjunction_of_counit α 𝔉 𝔊 ε =
    op_cf_adj (cf_adjunction_of_unit α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε))"


text‹Components.›

lemma cf_adjunction_of_counit_components:
  shows "cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjLeft⦈ = op_cf (op_cf 𝔉)"
    and "cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjRight⦈ = op_cf (op_cf 𝔊)"
    and "cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈ = op_cf_adj_nt
      (op_cf 𝔊⦇HomDom⦈)
      (op_cf 𝔊⦇HomCod⦈)
      (cf_adjunction_AdjNT_of_unit α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε))"
  unfolding 
    cf_adjunction_of_counit_def 
    op_cf_adj_components 
    cf_adjunction_of_unit_components
  by (simp_all add: cat_op_simps)


subsubsection‹Natural transformation map›

lemma cf_adjunction_of_counit_NTMap_vsv: 
  "vsv (cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈)"
  unfolding cf_adjunction_of_counit_components by (rule inv_ntcf_NTMap_vsv)
  


subsubsection‹
An adjunction constructed from universal morphisms 
from functors to objects is an adjunction
›

lemma cf_adjunction_of_counit_is_cf_adjunction:
  assumes "category α ℭ"
    and "category α 𝔇"
    and "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "ε : 𝔉 ∘CF 𝔊 ↦CF cf_id 𝔇 : 𝔇 ↦↦C⇘α⇙ 𝔇"
    and "⋀x. x ∈∘ 𝔇⦇Obj⦈ ⟹ universal_arrow_fo 𝔉 x (𝔊⦇ObjMap⦈⦇x⦈) (ε⦇NTMap⦈⦇x⦈)"
  shows "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    and "εC (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
    and "𝒟∘ (cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈) = 
      (op_cat ℭ ×C 𝔇)⦇Obj⦈"
    and "⋀c d. ⟦ c ∈∘ ℭ⦇Obj⦈; d ∈∘ 𝔇⦇Obj⦈ ⟧ ⟹
      cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈⦇c, d⦈∙ =
        (umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c)¯Set"
proof-

  interpret ℭ: category α ℭ by (rule assms(1))
  interpret 𝔇: category α 𝔇 by (rule assms(2))
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
  interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
  interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘CF 𝔊› ‹cf_id 𝔇› ε by (rule assms(5))
  
  note cf_adjunction_of_counit_def' = 
    cf_adjunction_of_counit_def[where 𝔉=𝔉, unfolded 𝔉.cf_HomDom 𝔉.cf_HomCod]
  
  have ua:
    "universal_arrow_of (op_cf 𝔉) x (op_cf 𝔊⦇ObjMap⦈⦇x⦈) (op_ntcf ε⦇NTMap⦈⦇x⦈)"
    if "x ∈∘ op_cat 𝔇⦇Obj⦈" for x
    using that unfolding cat_op_simps by (rule assms(6))
  
  let ?aou = ‹cf_adjunction_of_unit α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε)›
  from 
    cf_adjunction_of_unit_is_cf_adjunction
      [
        OF 
          𝔇.category_op
          ℭ.category_op
          𝔊.is_functor_op
          𝔉.is_functor_op
          ε.is_ntcf_op[unfolded cat_op_simps]
          ua,
        simplified cf_adjunction_of_counit_def[symmetric]
      ]
  have aou: "?aou : op_cf 𝔊 ⇌CF op_cf 𝔉 : op_cat 𝔇 ⇌⇌C⇘α⇙ op_cat ℭ"
    and η_aou: "ηC ?aou = op_ntcf ε"
    by auto
  interpret aou: 
    is_cf_adjunction α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔉› ?aou
    by (rule aou)
  from η_aou have
    "op_ntcf (ηC ?aou) = op_ntcf (op_ntcf ε)"
    by simp
  then show "εC (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
    unfolding 
      ε.ntcf_op_ntcf_op_ntcf
      is_cf_adjunction.op_ntcf_cf_adjunction_unit[OF aou]
      cf_adjunction_of_counit_def'[symmetric]
    by (simp add: cat_op_simps)
  show aoc_ε: "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    by 
      (
        rule 
          is_cf_adjunction_op[
            OF aou, folded cf_adjunction_of_counit_def', unfolded cat_op_simps
          ]
      )
  interpret aoc_ε: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 ‹cf_adjunction_of_counit α 𝔉 𝔊 ε›
    by (rule aoc_ε)

  from aoc_ε.NT.is_ntcf_axioms show
    "𝒟∘ (cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈) = (op_cat ℭ ×C 𝔇)⦇Obj⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)

  show "⋀c d. ⟦ c ∈∘ ℭ⦇Obj⦈; d ∈∘ 𝔇⦇Obj⦈ ⟧ ⟹
    cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈⦇c, d⦈∙ =
      (umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c)¯Set"
  proof-
    fix c d assume prems: "c ∈∘ ℭ⦇Obj⦈" "d ∈∘ 𝔇⦇Obj⦈"
    from assms(1-4) prems have aou_dc:
      "cf_adjunction_AdjNT_of_unit 
        α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε)⦇NTMap⦈⦇d, c⦈∙ =
        umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_op_simps adj_cs_simps cs_intro: cat_op_intros
        )
    from assms(1-4) aou prems have ufo_ε_dc:
      "umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c :
        HomO.C⇘α⇙op_cat ℭ(op_cf 𝔊-,-)⦇ObjMap⦈⦇d, c⦈∙ ↦iso⇘cat_Set α⇙
        HomO.C⇘α⇙op_cat 𝔇(-,op_cf 𝔉-)⦇ObjMap⦈⦇d, c⦈∙"
      by 
        (
          cs_concl cs_shallow
            cs_simp: 
              aou_dc[symmetric] cf_adjunction_of_unit_components(3)[symmetric]
            cs_intro: 
              is_iso_ntcf.iso_ntcf_is_iso_arr' 
              adj_cs_intros 
              cat_cs_intros 
              cat_op_intros
              cat_prod_cs_intros
        )
    from 
      assms(1-4) 
      aoc_ε[unfolded cf_adjunction_of_counit_def'] 
      aou 
      prems 
      ufo_ε_dc
    show
      "cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈⦇c, d⦈∙ =
        (umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c)¯Set"
      unfolding cf_adjunction_of_counit_def'
      by 
        ( 
          cs_concl
            cs_simp: cat_op_simps adj_cs_simps cat_cs_simps cat_Set_cs_simps 
            cs_intro: adj_cs_intros cat_cs_intros cat_prod_cs_intros
        )
  qed

qed



subsection‹
Construction of an adjunction from a functor and universal morphisms
from functors to objects
›


text‹
The subsection presents the construction of an adjunction given 
a functor and a structured collection of universal morphisms 
from functors to objects.
The content of this subsection follows the statement and the proof
of Theorem 2-iv in Chapter IV-1 in cite‹"mac_lane_categories_2010"›.
›


subsubsection‹Definition and elementary properties›

definition cf_ra_of_la :: "(V ⇒ V) ⇒ V ⇒ V ⇒ V"
  where "cf_ra_of_la F 𝔉 ε = op_cf (cf_la_of_ra F (op_cf 𝔉) ε)"


subsubsection‹Object map›

lemma cf_ra_of_la_ObjMap_vsv[adj_cs_intros]: "vsv (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈)"
  unfolding cf_ra_of_la_def op_cf_components by (auto intro: adj_cs_intros)

lemma (in is_functor) cf_ra_of_la_ObjMap_vdomain: 
  "𝒟∘ (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈) = 𝔅⦇Obj⦈"
  unfolding cf_ra_of_la_def cf_la_of_ra_components cat_op_simps 
  by (simp add: cat_cs_simps)

lemmas [adj_cs_simps] = is_functor.cf_ra_of_la_ObjMap_vdomain

lemma (in is_functor) cf_ra_of_la_ObjMap_app: 
  assumes "d ∈∘ 𝔅⦇Obj⦈"
  shows "cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇d⦈ = F d"
  using assms 
  unfolding cf_ra_of_la_def cf_la_of_ra_components cat_op_simps
  by (simp add: cat_cs_simps)

lemmas [adj_cs_simps] = is_functor.cf_ra_of_la_ObjMap_app


subsubsection‹Arrow map›

lemma cf_ra_of_la_ArrMap_app_unique:
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "f : a ↦⇘𝔇⇙ b"
    and "universal_arrow_fo 𝔉 a (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇a⦈) (ε⦇a⦈)"
    and "universal_arrow_fo 𝔉 b (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇b⦈) (ε⦇b⦈)"
  shows "cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ : F a ↦⇘ℭ⇙ F b"
    and "f ∘A⇘𝔇⇙ ε⦇a⦈ =
      umap_fo 𝔉 b (F b) (ε⦇b⦈) (F a)⦇ArrVal⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈⦈"
    and "⋀f'.
      ⟦
        f' : F a ↦⇘ℭ⇙ F b;
        f ∘A⇘𝔇⇙ ε⦇a⦈ = umap_fo 𝔉 b (F b) (ε⦇b⦈) (F a)⦇ArrVal⦈⦇f'⦈
      ⟧ ⟹ cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ = f'"
proof-
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
  from assms(2) have op_f: "f : b ↦⇘op_cat 𝔇⇙ a" unfolding cat_op_simps by simp
  let ?lara = ‹cf_la_of_ra F (op_cf 𝔉) ε›
  have lara_ObjMap_eq_op: "?lara⦇ObjMap⦈ = (op_cf ?lara⦇ObjMap⦈)"
    and lara_ArrMap_eq_op: "?lara⦇ArrMap⦈ = (op_cf ?lara⦇ArrMap⦈)"
    unfolding cat_op_simps by simp_all
  note ua_η_a = 𝔉.universal_arrow_foD[OF assms(3)]
    and ua_η_b = 𝔉.universal_arrow_foD[OF assms(4)]
  from assms(1,2) ua_η_a(2) have [cat_op_simps]:
    "ε⦇a⦈ ∘A⇘op_cat 𝔇⇙ f = f ∘A⇘𝔇⇙ ε⦇a⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_op_simps)
  show "cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ : F a ↦⇘ℭ⇙ F b"
    and "f ∘A⇘𝔇⇙ ε⦇a⦈ =
      umap_fo 𝔉 b (F b) (ε⦇b⦈) (F a)⦇ArrVal⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈⦈"
    and "⋀f'.
      ⟦
        f' : F a ↦⇘ℭ⇙ F b;
        f ∘A⇘𝔇⇙ ε⦇a⦈ = umap_fo 𝔉 b (F b) (ε⦇b⦈) (F a)⦇ArrVal⦈⦇f'⦈
      ⟧ ⟹ cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ = f'"
    by 
      (
        intro 
          cf_la_of_ra_ArrMap_app_unique
            [
              where η=ε and F=F,
                OF 𝔉.is_functor_op op_f, 
                unfolded 
                  𝔉.op_cf_universal_arrow_of 
                  lara_ObjMap_eq_op
                  lara_ArrMap_eq_op,
                folded cf_ra_of_la_def,
                unfolded cat_op_simps, OF assms(4,3)
            ]
      )+
qed

lemma cf_ra_of_la_ArrMap_app_is_arr[adj_cs_intros]:
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "f : a ↦⇘𝔇⇙ b"
    and "universal_arrow_fo 𝔉 a (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇a⦈) (ε⦇a⦈)"
    and "universal_arrow_fo 𝔉 b (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇b⦈) (ε⦇b⦈)"
    and "Fa = F a"
    and "Fb = F b"
  shows "cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ : Fa ↦⇘ℭ⇙ Fb"
  using assms(1-4) unfolding assms(5,6) by (rule cf_ra_of_la_ArrMap_app_unique)


subsubsection‹
An adjunction constructed from a functor and universal morphisms 
from functors to objects is an adjunction
›

lemma op_cf_cf_la_of_ra_op[cat_op_simps]: 
  "op_cf (cf_la_of_ra F (op_cf 𝔉) ε) = cf_ra_of_la F 𝔉 ε"
  unfolding cf_ra_of_la_def by simp

lemma cf_ra_of_la_commute_op:
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "⋀d. d ∈∘ 𝔇⦇Obj⦈ ⟹
      universal_arrow_fo 𝔉 d (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇d⦈) (ε⦇d⦈)"
    and "⋀d d' h. h : d ↦⇘𝔇⇙ d' ⟹
      ε⦇d'⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇h⦈⦈ =
        h ∘A⇘𝔇⇙ ε⦇d⦈"
    and "h : c' ↦⇘𝔇⇙ c"
  shows "𝔉⦇ArrMap⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇h⦈⦈ ∘A⇘op_cat 𝔇⇙ ε⦇c⦈ =
    ε⦇c'⦈ ∘A⇘op_cat 𝔇⇙ h"
proof-
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
  from assms(4) have c': "c' ∈∘ 𝔇⦇Obj⦈" and c: "c ∈∘ 𝔇⦇Obj⦈" by auto
  note ua_η_c' = 𝔉.universal_arrow_foD[OF assms(2)[OF c']]
    and ua_η_c = 𝔉.universal_arrow_foD[OF assms(2)[OF c]]
  note rala_f = cf_ra_of_la_ArrMap_app_unique[
      OF assms(1) assms(4) assms(2)[OF c'] assms(2)[OF c]
      ]
  from assms(1) assms(4) ua_η_c'(2) ua_η_c(2) rala_f(1) show ?thesis
    by 
      (
        cs_concl cs_shallow
          cs_simp: assms(3) cat_op_simps adj_cs_simps cat_cs_simps 
          cs_intro: cat_cs_intros
      )
qed

lemma 
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "⋀d. d ∈∘ 𝔇⦇Obj⦈ ⟹ F d ∈∘ ℭ⦇Obj⦈"
    and "⋀d. d ∈∘ 𝔇⦇Obj⦈ ⟹
      universal_arrow_fo 𝔉 d (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇d⦈) (ε⦇d⦈)"
    and "⋀d d' h. h : d ↦⇘𝔇⇙ d' ⟹
      ε⦇d'⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇h⦈⦈ =
        h ∘A⇘𝔇⇙ ε⦇d⦈"
  shows cf_ra_of_la_is_functor: "cf_ra_of_la F 𝔉 ε : 𝔇 ↦↦C⇘α⇙ ℭ"
    and cf_la_of_ra_op_is_functor:  
      "cf_la_of_ra F (op_cf 𝔉) ε : op_cat 𝔇 ↦↦C⇘α⇙ op_cat ℭ"
proof-
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
  have 𝔉h_εc: 
    "𝔉⦇ArrMap⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇h⦈⦈ ∘A⇘op_cat 𝔇⇙ ε⦇c⦈ =
      ε⦇c'⦈ ∘A⇘op_cat 𝔇⇙ h"
    if "h : c' ↦⇘𝔇⇙ c" for c c' h
  proof-
    from that have c': "c' ∈∘ 𝔇⦇Obj⦈" and c: "c ∈∘ 𝔇⦇Obj⦈" by auto
    note ua_η_c' = 𝔉.universal_arrow_foD[OF assms(3)[OF c']]
      and ua_η_c = 𝔉.universal_arrow_foD[OF assms(3)[OF c]]
    note rala_f = cf_ra_of_la_ArrMap_app_unique[
        OF assms(1) that assms(3)[OF c'] assms(3)[OF c]
        ]
    from assms(1) that ua_η_c'(2) ua_η_c(2) rala_f(1) show ?thesis
      by
        (
          cs_concl cs_shallow
            cs_simp: assms(4) cat_op_simps adj_cs_simps cat_cs_simps 
            cs_intro: cat_cs_intros
        )
  qed
  let ?lara = ‹cf_la_of_ra F (op_cf 𝔉) ε›
  have lara_ObjMap_eq_op: "?lara⦇ObjMap⦈ = (op_cf ?lara⦇ObjMap⦈)"
    and lara_ArrMap_eq_op: "?lara⦇ArrMap⦈ = (op_cf ?lara⦇ArrMap⦈)"
    by (simp_all add: cat_op_simps del: op_cf_cf_la_of_ra_op)
  show "cf_la_of_ra F (op_cf 𝔉) ε : op_cat 𝔇 ↦↦C⇘α⇙ op_cat ℭ"
    by 
      (
        intro cf_la_of_ra_is_functor
          [
            where F=F and η=ε,
            OF 𝔉.is_functor_op,
            unfolded cat_op_simps,
            OF assms(2),
            simplified,
            unfolded lara_ObjMap_eq_op lara_ArrMap_eq_op,
            folded cf_ra_of_la_def,
            OF assms(3) 𝔉h_εc, 
            simplified
         ]
      )
  from 
    is_functor.is_functor_op[
      OF this, unfolded cat_op_simps, folded cf_ra_of_la_def
      ]
  show "cf_ra_of_la F 𝔉 ε : 𝔇 ↦↦C⇘α⇙ ℭ".
qed

lemma cf_ra_of_la_is_ntcf:
  fixes F 𝔇 𝔉 𝔊 εm ε
  defines "𝔊 ≡ cf_ra_of_la F 𝔉 εm"
    and "ε ≡ [εm, 𝔉 ∘CF 𝔊, cf_id 𝔇, 𝔇, 𝔇]∘"
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "⋀d. d ∈∘ 𝔇⦇Obj⦈ ⟹ F d ∈∘ ℭ⦇Obj⦈"
    and "⋀d. d ∈∘ 𝔇⦇Obj⦈ ⟹
      universal_arrow_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈)"
    and "⋀d d' h. h : d ↦⇘𝔇⇙ d' ⟹
      ε⦇NTMap⦈⦇d'⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇h⦈⦈ = h ∘A⇘𝔇⇙ ε⦇NTMap⦈⦇d⦈"
    and "vsv (ε⦇NTMap⦈)"
    and "𝒟∘ (ε⦇NTMap⦈) = 𝔇⦇Obj⦈"
  shows "ε : 𝔉 ∘CF 𝔊 ↦CF cf_id 𝔇 : 𝔇 ↦↦C⇘α⇙ 𝔇"
proof-
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
  have ε_components: 
    "ε⦇NTMap⦈ = εm"
    "ε⦇NTDom⦈ = 𝔉 ∘CF 𝔊"
    "ε⦇NTCod⦈ = cf_id 𝔇"
    "ε⦇NTDGDom⦈ = 𝔇"
    "ε⦇NTDGCod⦈ = 𝔇"
    unfolding ε_def nt_field_simps by (simp_all add: nat_omega_simps)
  note 𝔊_def = 𝔊_def[folded ε_components(1)]
  interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 
    unfolding 𝔊_def
    by (auto intro: cf_ra_of_la_is_functor[OF assms(3-6)[unfolded 𝔊_def]])
  interpret op_ε: is_functor 
    α ‹op_cat 𝔇› ‹op_cat ℭ› ‹cf_la_of_ra F (op_cf 𝔉) (ε⦇NTMap⦈)›
    by 
      (
        intro cf_la_of_ra_op_is_functor[
          where F=F and ε=‹ε⦇NTMap⦈›, OF assms(3-6)[unfolded 𝔊_def], simplified
          ]
      )
  interpret ε: vfsequence ε unfolding ε_def by simp
  have [cat_op_simps]: "op_ntcf (op_ntcf ε) = ε"
  proof(rule vsv_eqI)
    have dom_lhs: "𝒟∘ (op_ntcf (op_ntcf ε)) = 5ℕ"
      unfolding op_ntcf_def by (simp add: nat_omega_simps)
    from assms(7) show "𝒟∘ (op_ntcf (op_ntcf ε)) = 𝒟∘ ε" 
      unfolding dom_lhs by (simp add: ε_def ε.vfsequence_vdomain nat_omega_simps)
    have sup: 
      "op_ntcf (op_ntcf ε)⦇NTDom⦈ = ε⦇NTDom⦈" 
      "op_ntcf (op_ntcf ε)⦇NTCod⦈ = ε⦇NTCod⦈" 
      "op_ntcf (op_ntcf ε)⦇NTDGDom⦈ = ε⦇NTDGDom⦈" 
      "op_ntcf (op_ntcf ε)⦇NTDGCod⦈ = ε⦇NTDGCod⦈" 
      unfolding op_ntcf_components cat_op_simps ε_components
      by simp_all
    show "a ∈∘ 𝒟∘ (op_ntcf (op_ntcf ε)) ⟹ op_ntcf (op_ntcf ε)⦇a⦈ = ε⦇a⦈" for a
      by (unfold dom_lhs, elim_in_numeral, fold nt_field_simps, unfold sup)
        (simp_all add: cat_op_simps)
  qed (auto simp: op_ntcf_def)
  let ?lara = ‹cf_la_of_ra F (op_cf 𝔉) (ε⦇NTMap⦈)›
  have lara_ObjMap_eq_op: "?lara⦇ObjMap⦈ = (op_cf ?lara⦇ObjMap⦈)"
    and lara_ArrMap_eq_op: "?lara⦇ArrMap⦈ = (op_cf ?lara⦇ArrMap⦈)"
    by (simp_all add: cat_op_simps del: op_cf_cf_la_of_ra_op)
  have seq: "vfsequence (op_ntcf ε)" unfolding op_ntcf_def by auto
  have card: "vcard (op_ntcf ε) = 5ℕ" 
    unfolding op_ntcf_def by (simp add: nat_omega_simps)
  have op_cf_NTCod: "op_cf (ε⦇NTCod⦈) = cf_id (op_cat 𝔇)"
    unfolding ε_components cat_op_simps by simp
  from assms(3) have op_cf_NTDom:
    "op_cf (ε⦇NTDom⦈) = op_cf 𝔉 ∘CF cf_la_of_ra F (op_cf 𝔉) (ε⦇NTMap⦈)"
    unfolding ε_components  
    by
      (
        simp 
          add: cat_op_simps 𝔊_def cf_ra_of_la_def ε_components(1)[symmetric] 
          del: op_cf_cf_la_of_ra_op
      )
  note cf_la_of_ra_is_ntcf
    [
      where F=F and ηm=‹ε⦇NTMap⦈›,
      OF is_functor.is_functor_op[OF assms(3)],
      unfolded cat_op_simps,
      OF assms(4),
      unfolded ε_components(1),
      folded op_cf_NTCod op_cf_NTDom[unfolded ε_components(1)]  ε_components(1),
      folded op_ntcf_def[of ε, unfolded ε_components(4,5)],
      unfolded 
        cat_op_simps 
        lara_ObjMap_eq_op lara_ArrMap_eq_op cf_ra_of_la_def[symmetric],
      folded 𝔊_def,
      simplified,
      OF 
        assms(5)  
        cf_ra_of_la_commute_op[
          OF assms(3,5,6)[unfolded 𝔊_def], folded 𝔊_def
          ]
        assms(7,8),
      unfolded ε_components,
      simplified
    ]
  from is_ntcf.is_ntcf_op[OF this, unfolded cat_op_simps 𝔊_def[symmetric]] show 
    "ε : 𝔉 ∘CF 𝔊 ↦CF cf_id 𝔇 : 𝔇 ↦↦C⇘α⇙ 𝔇".
qed

lemma cf_ra_of_la_is_counit: 
  fixes F 𝔇 𝔉 𝔊 εm ε
  defines "𝔊 ≡ cf_ra_of_la F 𝔉 εm"
    and "ε ≡ [εm, 𝔉 ∘CF 𝔊, cf_id 𝔇, 𝔇, 𝔇]∘"
  assumes "category α ℭ"
    and "category α 𝔇"
    and "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "⋀d. d ∈∘ 𝔇⦇Obj⦈ ⟹ F d ∈∘ ℭ⦇Obj⦈"
    and "⋀d. d ∈∘ 𝔇⦇Obj⦈ ⟹
      universal_arrow_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈)"
    and "⋀d d' h. h : d ↦⇘𝔇⇙ d' ⟹
      ε⦇NTMap⦈⦇d'⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇h⦈⦈ = h ∘A⇘𝔇⇙ ε⦇NTMap⦈⦇d⦈"
    and "vfsequence ε"
    and "vsv (ε⦇NTMap⦈)"
    and "𝒟∘ (ε⦇NTMap⦈) = 𝔇⦇Obj⦈"
  shows "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    and "εC (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
proof-
  have ε_components: 
    "ε⦇NTMap⦈ = εm"
    "ε⦇NTDom⦈ = 𝔉 ∘CF 𝔊"
    "ε⦇NTCod⦈ = cf_id 𝔇"
    "ε⦇NTDGDom⦈ = 𝔇"
    "ε⦇NTDGCod⦈ = 𝔇"
    unfolding ε_def nt_field_simps by (simp_all add: nat_omega_simps)
  note 𝔊_def = 𝔊_def[folded ε_components(1)]
  note 𝔉 = cf_ra_of_la_is_functor[
    where F=F and ε=‹ε⦇NTMap⦈›, OF assms(5-8)[unfolded 𝔊_def], simplified
    ]
  note ε = cf_ra_of_la_is_ntcf
    [
      where F=F and εm=‹εm› and 𝔇=𝔇 and 𝔉=𝔉, 
      folded 𝔊_def[unfolded ε_components(1)], 
      folded ε_def, 
      OF assms(5-8) assms(10,11),
      simplified
    ]
  show "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    and "εC (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
    by 
      (
        intro cf_adjunction_of_counit_is_cf_adjunction
          [
            OF assms(3-5) 𝔉, 
            folded 𝔊_def, 
            OF ε assms(7)[folded 𝔊_def], 
            simplified
          ]
      )+
qed



subsection‹Construction of an adjunction from the counit-unit equations›


text‹
The subsection presents the construction of an adjunction given 
two natural transformations satisfying counit-unit equations.
The content of this subsection follows the statement and the proof
of Theorem 2-v in Chapter IV-1 in cite‹"mac_lane_categories_2010"›.
›

lemma counit_unit_is_cf_adjunction:
  assumes "category α ℭ"
    and "category α 𝔇"
    and "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "η : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
    and "ε : 𝔉 ∘CF 𝔊 ↦CF cf_id 𝔇 : 𝔇 ↦↦C⇘α⇙ 𝔇"
    and "(𝔊 ∘CF-NTCF ε) ∙NTCF (η ∘NTCF-CF 𝔊) = ntcf_id 𝔊"
    and "(ε ∘NTCF-CF 𝔉) ∙NTCF (𝔉 ∘CF-NTCF η) = ntcf_id 𝔉"
  shows "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    and "ηC (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
    and "εC (cf_adjunction_of_unit α 𝔉 𝔊 η) = ε"
proof-

  interpret ℭ: category α ℭ by (rule assms(1))
  interpret 𝔇: category α 𝔇 by (rule assms(2))
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
  interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
  interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘CF 𝔉› η by (rule assms(5))
  interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘CF 𝔊› ‹cf_id 𝔇› ε by (rule assms(6))

  have 𝔊εx_η𝔊x[cat_cs_simps]:
    "𝔊⦇ArrMap⦈⦇ε⦇NTMap⦈⦇x⦈⦈ ∘A⇘ℭ⇙ η⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ = ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈"
    if "x ∈∘ 𝔇⦇Obj⦈" for x
  proof-
    from assms(7) have 
      "((𝔊 ∘CF-NTCF ε) ∙NTCF (η ∘NTCF-CF 𝔊))⦇NTMap⦈⦇x⦈ = ntcf_id 𝔊⦇NTMap⦈⦇x⦈"
      by simp
    from this assms(1-6) that show 
      "𝔊⦇ArrMap⦈⦇ε⦇NTMap⦈⦇x⦈⦈ ∘A⇘ℭ⇙ η⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ = 
        ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈"
      by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed
  have [cat_cs_simps]:
    "𝔊⦇ArrMap⦈⦇ε⦇NTMap⦈⦇x⦈⦈ ∘A⇘ℭ⇙ (η⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ ∘A⇘ℭ⇙ f) =
      ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ ∘A⇘ℭ⇙ f"
    if "x ∈∘ 𝔇⦇Obj⦈" and "f : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇x⦈" for x f a
    using assms(1-6) that
    by (intro ℭ.cat_assoc_helper)
      (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+

  have [cat_cs_simps]:
    "ε⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇η⦇NTMap⦈⦇x⦈⦈ = 𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
    if "x ∈∘ ℭ⦇Obj⦈" for x
  proof-
    from assms(8) have 
      "((ε ∘NTCF-CF 𝔉) ∙NTCF (𝔉 ∘CF-NTCF η))⦇NTMap⦈⦇x⦈ = ntcf_id 𝔉⦇NTMap⦈⦇x⦈"
      by simp
    from this assms(1-6) that show
      "ε⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇η⦇NTMap⦈⦇x⦈⦈ = 𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
      by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  qed

  have ua_𝔉x_ηx: "universal_arrow_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈)"
    if "x ∈∘ ℭ⦇Obj⦈" for x 
  proof(intro is_functor.universal_arrow_ofI)
    from assms(3) that show "𝔉⦇ObjMap⦈⦇x⦈ ∈∘ 𝔇⦇Obj⦈"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    from assms(3-6) that show "η⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    fix r' u' assume prems': "r' ∈∘ 𝔇⦇Obj⦈" "u' : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇r'⦈"
    show "∃!f'.
      f' : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ r' ∧
      u' = umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈) r'⦇ArrVal⦈⦇f'⦈"
    proof(intro ex1I conjI; (elim conjE)?)
      from assms(3-6) that prems' show 
        "ε⦇NTMap⦈⦇r'⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇u'⦈ : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ r'"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      from assms(3-6) prems' have 𝔊𝔉u':
        "(𝔊 ∘CF 𝔉)⦇ArrMap⦈⦇u'⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇u'⦈⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      note [cat_cs_simps] = 
        η.ntcf_Comp_commute[symmetric, OF prems'(2), unfolded 𝔊𝔉u']
      from assms(3-6) that prems' show 
        "u' =
          umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈) r'⦇ArrVal⦈⦇ε⦇NTMap⦈⦇r'⦈ ∘A⇘𝔇⇙
          𝔉⦇ArrMap⦈⦇u'⦈⦈"
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_prod_cs_intros
          )
      fix f' assume prems'':
        "f' : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ r'"
        "u' = umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈) r'⦇ArrVal⦈⦇f'⦈" 
      from prems''(2,1) assms(3-6) that have u'_def:
        "u' = 𝔊⦇ArrMap⦈⦇f'⦈ ∘A⇘ℭ⇙ η⦇NTMap⦈⦇x⦈"
        by 
          (
            cs_prems cs_shallow
              cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_prod_cs_intros
          )
      from 
        ε.ntcf_Comp_commute[OF prems''(1)] 
        assms(3-6) 
        prems''(1) 
      have [cat_cs_simps]:
        "ε⦇NTMap⦈⦇r'⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇f'⦈⦈ =
          f' ∘A⇘𝔇⇙ ε⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
        by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      have [cat_cs_simps]:
        "ε⦇NTMap⦈⦇r'⦈ ∘A⇘𝔇⇙ (𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇f'⦈⦈ ∘A⇘𝔇⇙ f) =
          (f' ∘A⇘𝔇⇙ ε⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈) ∘A⇘𝔇⇙ f"
        if "f : a ↦⇘𝔇⇙ 𝔉⦇ObjMap⦈⦇𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈⦈" for f a
        using assms(1-6) prems''(1) prems' that
        by (intro 𝔇.cat_assoc_helper)
          (
            cs_concl 
              cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_prod_cs_intros
          )+
      from prems''(2,1) assms(3-6) that show 
        "f' = ε⦇NTMap⦈⦇r'⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇u'⦈"
        unfolding u'_def 
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_prod_cs_intros
          )
    qed
  qed (auto intro: cat_cs_intros)

  show aou: "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    by (intro cf_adjunction_of_unit_is_cf_adjunction ua_𝔉x_ηx assms(1-5))
  from ℭ.category_axioms 𝔇.category_axioms show 
    "ηC (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
    by 
      (
        cs_concl cs_shallow 
          cs_intro: cf_adjunction_of_unit_is_cf_adjunction assms(1-5) ua_𝔉x_ηx
      )

  interpret aou: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 ‹cf_adjunction_of_unit α 𝔉 𝔊 η›
    by (rule aou)

  show "εC (cf_adjunction_of_unit α 𝔉 𝔊 η) = ε"
  proof(rule ntcf_eqI)
    show ε_η: "εC (cf_adjunction_of_unit α 𝔉 𝔊 η) :
      𝔉 ∘CF 𝔊 ↦CF cf_id 𝔇 : 𝔇 ↦↦C⇘α⇙ 𝔇"
      by (rule aou.cf_adjunction_counit_is_ntcf)
    from assms(1-6) ε_η have dom_lhs:
      "𝒟∘ (εC (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈) = 𝔇⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    from assms(1-6) ε_η have dom_rhs: "𝒟∘ (ε⦇NTMap⦈) = 𝔇⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    show "εC (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈ = ε⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a ∈∘ 𝔇⦇Obj⦈"
      with aou.is_cf_adjunction_axioms assms(1-6) show 
        "εC (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈⦇a⦈ = ε⦇NTMap⦈⦇a⦈"
        by
          (
            cs_concl 
              cs_intro:
                cat_arrow_cs_intros
                cat_op_intros
                cat_cs_intros
                cat_prod_cs_intros
              cs_simp: 
                aou.cf_adj_umap_of_unit'[symmetric]
                cat_Set_the_inverse[symmetric]
                adj_cs_simps cat_cs_simps cat_op_simps
          )
    qed (auto simp: adj_cs_intros)
  qed (auto simp: assms) 

qed

lemma counit_unit_cf_adjunction_of_counit_is_cf_adjunction:
  assumes "category α ℭ"
    and "category α 𝔇"
    and "𝔉 : ℭ ↦↦C⇘α⇙ 𝔇"
    and "𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "η : cf_id ℭ ↦CF 𝔊 ∘CF 𝔉 : ℭ ↦↦C⇘α⇙ ℭ"
    and "ε : 𝔉 ∘CF 𝔊 ↦CF cf_id 𝔇 : 𝔇 ↦↦C⇘α⇙ 𝔇"
    and "(𝔊 ∘CF-NTCF ε) ∙NTCF (η ∘NTCF-CF 𝔊) = ntcf_id 𝔊"
    and "(ε ∘NTCF-CF 𝔉) ∙NTCF (𝔉 ∘CF-NTCF η) = ntcf_id 𝔉"
  shows "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    and "ηC (cf_adjunction_of_counit α 𝔉 𝔊 ε) = η"
    and "εC (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
proof-

  interpret ℭ: category α ℭ by (rule assms(1))
  interpret 𝔇: category α 𝔇 by (rule assms(2))
  interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
  interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
  interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘CF 𝔉› η by (rule assms(5))
  interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘CF 𝔊› ‹cf_id 𝔇› ε by (rule assms(6))

  have unit_op: "cf_adjunction_of_unit α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε) :
    op_cf 𝔊 ⇌CF op_cf 𝔉 : op_cat 𝔇 ⇌⇌C⇘α⇙ op_cat ℭ"
    by (rule counit_unit_is_cf_adjunction(1)[where ε=‹op_ntcf η›])
      (
        cs_concl 
          cs_simp:
            cat_op_simps cat_cs_simps 
            𝔊.cf_ntcf_id_op_cf
            𝔉.cf_ntcf_id_op_cf
            op_ntcf_ntcf_vcomp[symmetric]
            op_ntcf_ntcf_cf_comp[symmetric]
            op_ntcf_cf_ntcf_comp[symmetric]
            assms(7,8) 
          cs_intro: cat_op_intros cat_cs_intros
      )+
  then show aou: "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇"
    unfolding cf_adjunction_of_counit_def
    by
      (
        subst 𝔉.cf_op_cf_op_cf[symmetric],
        subst 𝔊.cf_op_cf_op_cf[symmetric],
        subst ℭ.cat_op_cat_op_cat[symmetric],
        subst 𝔇.cat_op_cat_op_cat[symmetric],
        rule is_cf_adjunction_op
      )

  interpret aou: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 ‹cf_adjunction_of_counit α 𝔉 𝔊 ε›
    by (rule aou)

  show "ηC (cf_adjunction_of_counit α 𝔉 𝔊 ε) = η"
    unfolding cf_adjunction_of_counit_def
    by (*slow*)
      (
        cs_concl_step is_cf_adjunction.op_ntcf_cf_adjunction_counit[symmetric], 
        rule unit_op, 
        cs_concl_step counit_unit_is_cf_adjunction(3)[where ε=‹op_ntcf η›],
        insert ℭ.category_op 𝔇.category_op,
        rule 𝔇.category_op, rule ℭ.category_op
      )
      (
        cs_concl 
          cs_simp:
            cat_op_simps cat_cs_simps 
            𝔊.cf_ntcf_id_op_cf
            𝔉.cf_ntcf_id_op_cf
            op_ntcf_ntcf_vcomp[symmetric]
            op_ntcf_ntcf_cf_comp[symmetric]
            op_ntcf_cf_ntcf_comp[symmetric]
            assms(7,8) 
          cs_intro: cat_op_intros cat_cs_intros
      )+ 

  show "εC (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
    unfolding cf_adjunction_of_counit_def
    by
      (
        cs_concl_step is_cf_adjunction.op_ntcf_cf_adjunction_unit[symmetric], 
        rule unit_op, 
        cs_concl_step counit_unit_is_cf_adjunction(2)[where ε=‹op_ntcf η›],
        insert ℭ.category_op 𝔇.category_op,
        rule 𝔇.category_op, rule ℭ.category_op
      )
      (
        cs_concl 
          cs_simp:
            cat_op_simps cat_cs_simps 
            𝔊.cf_ntcf_id_op_cf
            𝔉.cf_ntcf_id_op_cf
            op_ntcf_ntcf_vcomp[symmetric]
            op_ntcf_ntcf_cf_comp[symmetric]
            op_ntcf_cf_ntcf_comp[symmetric]
            assms(7,8) 
          cs_intro: cat_op_intros cat_cs_intros
      )+

qed



subsection‹Adjoints are unique up to isomorphism›


text‹
The content of the following subsection is based predominantly on
the statement and the proof of Corollary 1 in 
Chapter IV-1 in cite‹"mac_lane_categories_2010"›. However, similar 
results can also be found in section 4 in cite‹"riehl_category_2016"›
and in subsection 2.1 in cite‹"bodo_categories_1970"›.
›


subsubsection‹Definitions and elementary properties›

definition cf_adj_LR_iso :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ =
    [
      (
        λx∈∘ℭ⦇Obj⦈. THE f'.
        let
          η = ηC Φ;
          η' = ηC Ψ;
          𝔉x = 𝔉⦇ObjMap⦈⦇x⦈;
          𝔉'x = 𝔉'⦇ObjMap⦈⦇x⦈
        in
          f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
          η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x (𝔉x) (η⦇NTMap⦈⦇x⦈) (𝔉'x)⦇ArrVal⦈⦇f'⦈
      ),
      𝔉,
      𝔉',
      ℭ,
      𝔇
    ]∘"

definition cf_adj_RL_iso :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
  where "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ =
    [
      (
        λx∈∘𝔇⦇Obj⦈. THE f'.
        let
          ε = εC Φ;
          ε' = εC Ψ;
          𝔊x = 𝔊⦇ObjMap⦈⦇x⦈;
          𝔊'x = 𝔊'⦇ObjMap⦈⦇x⦈
        in
          f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
          ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈
      ),
      𝔊',
      𝔊,
      𝔇,
      ℭ
    ]∘"


text‹Components.›

lemma cf_adj_LR_iso_components:
  shows "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈ =
    (
      λx∈∘ℭ⦇Obj⦈. THE f'.
      let
        η = ηC Φ;
        η' = ηC Ψ;
        𝔉x = 𝔉⦇ObjMap⦈⦇x⦈;
        𝔉'x = 𝔉'⦇ObjMap⦈⦇x⦈
      in
        f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
        η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈
    )"
    and [adj_cs_simps]: "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTDom⦈ = 𝔉"
    and [adj_cs_simps]: "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTCod⦈ = 𝔉'"
    and [adj_cs_simps]: "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTDGDom⦈ = ℭ"
    and [adj_cs_simps]: "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTDGCod⦈ = 𝔇"
  unfolding cf_adj_LR_iso_def nt_field_simps
  by (simp_all add: nat_omega_simps) (*slow*)

lemma cf_adj_RL_iso_components:
  shows "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈ =
    (
        λx∈∘𝔇⦇Obj⦈. THE f'.
        let
          ε = εC Φ;
          ε' = εC Ψ;
          𝔊x = 𝔊⦇ObjMap⦈⦇x⦈;
          𝔊'x = 𝔊'⦇ObjMap⦈⦇x⦈
        in
          f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
          ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈
    )"
    and [adj_cs_simps]: "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTDom⦈ = 𝔊'"
    and [adj_cs_simps]: "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTCod⦈ = 𝔊"
    and [adj_cs_simps]: "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTDGDom⦈ = 𝔇"
    and [adj_cs_simps]: "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTDGCod⦈ = ℭ"
  unfolding cf_adj_RL_iso_def nt_field_simps
  by (simp_all add: nat_omega_simps) (*slow*)


subsubsection‹Natural transformation map›

lemma cf_adj_LR_iso_vsv[adj_cs_intros]: 
  "vsv (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈)"
  unfolding cf_adj_LR_iso_components by simp

lemma cf_adj_RL_iso_vsv[adj_cs_intros]: 
  "vsv (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈)"
  unfolding cf_adj_RL_iso_components by simp

lemma cf_adj_LR_iso_vdomain[adj_cs_simps]:
  "𝒟∘ (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈) = ℭ⦇Obj⦈"
  unfolding cf_adj_LR_iso_components by simp

lemma cf_adj_RL_iso_vdomain[adj_cs_simps]:
  "𝒟∘ (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈) = 𝔇⦇Obj⦈"
  unfolding cf_adj_RL_iso_components by simp

lemma cf_adj_LR_iso_app:
  fixes ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ
  assumes "x ∈∘ ℭ⦇Obj⦈"
  defines "𝔉x ≡ 𝔉⦇ObjMap⦈⦇x⦈"
    and "𝔉'x ≡ 𝔉'⦇ObjMap⦈⦇x⦈"
    and "η ≡ ηC Φ" 
    and "η' ≡ ηC Ψ"
  shows "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈⦇x⦈ =
    (
      THE f'.
        f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
        η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈
    )"
  using assms(1) unfolding cf_adj_LR_iso_components assms(2-5) by simp meson

lemma cf_adj_RL_iso_app:
  fixes ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ
  assumes "x ∈∘ 𝔇⦇Obj⦈"
  defines "𝔊x ≡ 𝔊⦇ObjMap⦈⦇x⦈"
    and "𝔊'x ≡ 𝔊'⦇ObjMap⦈⦇x⦈"
    and "ε ≡ εC Φ" 
    and "ε' ≡ εC Ψ"
  shows "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈⦇x⦈ =
    (
      THE f'.
        f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
        ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈
    )"
  using assms(1) unfolding cf_adj_RL_iso_components assms(2-5) Let_def by simp

lemma cf_adj_LR_iso_app_unique:
  fixes ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ
  assumes "Φ : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" 
    and "Ψ : 𝔉' ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" 
    and "x ∈∘ ℭ⦇Obj⦈"
  defines "𝔉x ≡ 𝔉⦇ObjMap⦈⦇x⦈"
    and "𝔉'x ≡ 𝔉'⦇ObjMap⦈⦇x⦈"
    and "η ≡ ηC Φ" 
    and "η' ≡ ηC Ψ"
    and "f ≡ cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈⦇x⦈"
  shows
    "∃!f'.
      f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
      η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈"
    "f : 𝔉x ↦iso⇘𝔇⇙ 𝔉'x"
    "η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f⦈"
proof-
  interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
  interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉' 𝔊 Ψ by (rule assms(2))
  note 𝔉a_η =
    is_cf_adjunction.cf_adjunction_unit_component_is_ua_of[
      OF assms(1) assms(3), folded assms(4-8)
      ]
  note 𝔉'a_η = 
    is_cf_adjunction.cf_adjunction_unit_component_is_ua_of[
      OF assms(2) assms(3), folded assms(4-8)
      ]
  from 
    is_functor.cf_universal_arrow_of_unique[
      OF Φ.RL.is_functor_axioms 𝔉a_η 𝔉'a_η, folded assms(4-8)
      ]
  obtain f' 
    where f': "f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x"
      and η'_def: 
        "η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈"
      and unique_f': 
        "⟦
          f'' : 𝔉x ↦⇘𝔇⇙ 𝔉'x;
          η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f''⦈
        ⟧ ⟹ f'' = f'"
    for f''
    by metis
  show unique_f': "∃!f'.
    f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
    η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈"
    by 
      (
        rule is_functor.cf_universal_arrow_of_unique[
          OF Φ.RL.is_functor_axioms 𝔉a_η 𝔉'a_η, folded assms(4-8)
          ]
      )
  from
    theD
      [
        OF unique_f' cf_adj_LR_iso_app[
          OF assms(3), of 𝔇 𝔊 𝔉 Φ 𝔉' Ψ, folded assms(4-8)
          ]
      ]
  have f: "f : 𝔉x ↦⇘𝔇⇙ 𝔉'x"
    and η': "η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f⦈"
    by simp_all
  show "η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f⦈" by (rule η')
  show "f : 𝔉x ↦iso⇘𝔇⇙ 𝔉'x"
    by
      (
        rule 
          is_functor.cf_universal_arrow_of_is_iso_arr[
            OF Φ.RL.is_functor_axioms 𝔉a_η 𝔉'a_η f η'
            ]
      )
qed


subsubsection‹Main results›

lemma cf_adj_LR_iso_is_iso_functor:
  ―‹See Corollary 1 in Chapter IV-1 in \cite{mac_lane_categories_2010}.›
  assumes "Φ : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" and "Ψ : 𝔉' ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" 
  shows "∃!θ. θ : 𝔉 ↦CF 𝔉' : ℭ ↦↦C⇘α⇙ 𝔇 ∧ ηC Ψ = (𝔊 ∘CF-NTCF θ) ∙NTCF ηC Φ"
    and "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ : 𝔉 ↦CF.iso 𝔉' : ℭ ↦↦C⇘α⇙ 𝔇"
    and "ηC Ψ = (𝔊 ∘CF-NTCF cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ) ∙NTCF ηC Φ"
proof-

  interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
  interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉' 𝔊 Ψ by (rule assms(2))

  let ?η = ‹ηC Φ›
  let ?η' = ‹ηC Ψ›
  let ?ΦΨ = ‹cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ›

  show 𝔉'Ψ: "?ΦΨ : 𝔉 ↦CF.iso 𝔉' : ℭ ↦↦C⇘α⇙ 𝔇"
  proof(intro is_iso_ntcfI is_ntcfI')

    show "vfsequence ?ΦΨ" unfolding cf_adj_LR_iso_def by auto
    show "vcard ?ΦΨ = 5ℕ" 
      unfolding cf_adj_LR_iso_def by (simp add: nat_omega_simps)
    show "?ΦΨ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
      if "a ∈∘ ℭ⦇Obj⦈" for a
      using cf_adj_LR_iso_app_unique(2)[OF assms that] by auto

    show "?ΦΨ⦇NTMap⦈⦇b⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉'⦇ArrMap⦈⦇f⦈ ∘A⇘𝔇⇙ ?ΦΨ⦇NTMap⦈⦇a⦈"
      if "f : a ↦⇘ℭ⇙ b" for a b f
    proof-

      from that have a: "a ∈∘ ℭ⦇Obj⦈" and b: "b ∈∘ ℭ⦇Obj⦈" by auto
      note unique_a = cf_adj_LR_iso_app_unique[OF assms a]
      note unique_b = cf_adj_LR_iso_app_unique[OF assms b]

      from unique_a(2) have a_is_arr:
        "?ΦΨ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
        by auto
      from unique_b(2) have b_is_arr:
        "?ΦΨ⦇NTMap⦈⦇b⦈ : 𝔉⦇ObjMap⦈⦇b⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇b⦈"
        by auto

      interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘CF 𝔉› ?η
        by (rule Φ.cf_adjunction_unit_is_ntcf)
      interpret η': is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘CF 𝔉'› ?η'
        by (rule Ψ.cf_adjunction_unit_is_ntcf)

      from unique_a(3) a_is_arr a b have η'_a_def: 
        "?η'⦇NTMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈ ∘A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈"
        by 
          (
            cs_prems cs_shallow
              cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
          )
      from unique_b(3) b_is_arr a b have η'_b_def:
        "?η'⦇NTMap⦈⦇b⦈ = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘A⇘ℭ⇙ ?η⦇NTMap⦈⦇b⦈"
        by 
          (
            cs_prems cs_shallow 
              cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
          )
     
      from that a b a_is_arr have 
        "𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘A⇘ℭ⇙ 
          (𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈ ∘A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈) = 
            𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘A⇘ℭ⇙ ?η'⦇NTMap⦈⦇a⦈"
        by
          (
            cs_concl cs_shallow 
              cs_simp: cat_cs_simps η'_a_def cs_intro: cat_cs_intros
          )
      also from η'.ntcf_Comp_commute[OF that, symmetric] that a b have 
        "… = ?η'⦇NTMap⦈⦇b⦈ ∘A⇘ℭ⇙ f"
        by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      also from that a b b_is_arr have
        "… = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘A⇘ℭ⇙
          (?η⦇NTMap⦈⦇b⦈ ∘A⇘ℭ⇙ f)" 
        by 
          ( 
            cs_concl cs_shallow 
              cs_simp: cat_cs_simps η'_b_def cs_intro: cat_cs_intros
          )
      also from that have 
        "… = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘A⇘ℭ⇙
          ((𝔊 ∘CF 𝔉)⦇ArrMap⦈⦇f⦈ ∘A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈)"
        unfolding η.ntcf_Comp_commute[OF that, symmetric]
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_cs_simps η'_b_def cs_intro: cat_cs_intros
          )
      also from that b_is_arr have 
        "… = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘A⇘ℭ⇙
          (𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈ ∘A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈)"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
      finally have [cat_cs_simps]:
        "𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘A⇘ℭ⇙ (𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈ ∘A⇘ℭ⇙ 
          ?η⦇NTMap⦈⦇a⦈) =
          𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘A⇘ℭ⇙
            (𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈ ∘A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈)"
        by simp

      note unique_f_a = is_functor.universal_arrow_ofD
        [
          OF 
            Φ.RL.is_functor_axioms 
            Φ.cf_adjunction_unit_component_is_ua_of[OF a]
        ]

      from that a b a_is_arr b_is_arr have 𝔊𝔉f_ηa:
        "𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈  ∘A⇘ℭ⇙ ?η'⦇NTMap⦈⦇a⦈ :
          a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉'⦇ObjMap⦈⦇b⦈⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

      from b have 𝔉'b: "𝔉'⦇ObjMap⦈⦇b⦈ ∈∘ 𝔇⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)

      from unique_f_a(3)[OF 𝔉'b 𝔊𝔉f_ηa] obtain f' 
        where f': "f' : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇b⦈"
          and ηa: "𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘A⇘ℭ⇙ ?η'⦇NTMap⦈⦇a⦈ =
          umap_of 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (?η⦇NTMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)⦇ArrVal⦈⦇f'⦈"
          and unique_f':
            "⟦
              f'' : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇b⦈;
              𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘A⇘ℭ⇙ ?η'⦇NTMap⦈⦇a⦈ =
                umap_of 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (?η⦇NTMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)⦇ArrVal⦈⦇f''⦈
             ⟧ ⟹ f'' = f'"
        for f''
        by metis
      have "?ΦΨ⦇NTMap⦈⦇b⦈ ∘A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇f⦈ = f'"
        by (rule unique_f', insert a b a_is_arr b_is_arr that)
          (
            cs_concl cs_shallow 
              cs_simp: η'_a_def cat_cs_simps cs_intro: cat_cs_intros
          )
      moreover have "𝔉'⦇ArrMap⦈⦇f⦈ ∘A⇘𝔇⇙ ?ΦΨ⦇NTMap⦈⦇a⦈ = f'"
        by (rule unique_f', insert a b a_is_arr b_is_arr that)
          (
            cs_concl cs_shallow 
              cs_simp: η'_a_def cat_cs_simps cs_intro: cat_cs_intros
          )
      ultimately show ?thesis by simp
    qed 

  qed 
    (
      auto 
        intro: cat_cs_intros adj_cs_intros  
        simp: adj_cs_simps cf_adj_LR_iso_app_unique(2)[OF assms]
    )

  interpret 𝔉'Ψ: is_iso_ntcf α ℭ 𝔇 𝔉 𝔉' ‹?ΦΨ› by (rule 𝔉'Ψ)

  show η'_def: "?η' = 𝔊 ∘CF-NTCF ?ΦΨ ∙NTCF ηC Φ"
  proof(rule ntcf_eqI)
    have dom_lhs: "𝒟∘ (?η'⦇NTMap⦈) = ℭ⦇Obj⦈"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: adj_cs_intros)
    have dom_rhs: "𝒟∘ ((𝔊 ∘CF-NTCF ?ΦΨ ∙NTCF ηC Φ)⦇NTMap⦈) = ℭ⦇Obj⦈"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
        )
    show "?η'⦇NTMap⦈ = (𝔊 ∘CF-NTCF ?ΦΨ ∙NTCF ηC Φ)⦇NTMap⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume prems: "a ∈∘ ℭ⦇Obj⦈"
      note unique_a = cf_adj_LR_iso_app_unique[OF assms prems]
      from unique_a(2) have a_is_arr:
        "?ΦΨ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
        by auto  
      interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘CF 𝔉› ?η
        by (rule Φ.cf_adjunction_unit_is_ntcf)
      from unique_a(3) a_is_arr prems have η'_a_def: 
        "?η'⦇NTMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈ ∘A⇘ℭ⇙ ηC Φ⦇NTMap⦈⦇a⦈"
        by
          (
            cs_prems cs_shallow 
              cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
          )
      from prems a_is_arr show 
        "?η'⦇NTMap⦈⦇a⦈ =  (𝔊 ∘CF-NTCF ?ΦΨ ∙NTCF ?η)⦇NTMap⦈⦇a⦈"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: η'_a_def cat_cs_simps cs_intro: cat_cs_intros
          )
    qed (auto intro: cat_cs_intros adj_cs_intros)
  qed 
    (
      cs_concl cs_shallow 
        cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
    )+

  show "∃!θ. θ : 𝔉 ↦CF 𝔉' : ℭ ↦↦C⇘α⇙ 𝔇 ∧ ?η' = (𝔊 ∘CF-NTCF θ) ∙NTCF ?η"
  proof(intro ex1I conjI; (elim conjE)?)
    from 𝔉'Ψ show "?ΦΨ : 𝔉 ↦CF 𝔉' : ℭ ↦↦C⇘α⇙ 𝔇" by auto
    show "?η' = 𝔊 ∘CF-NTCF ?ΦΨ ∙NTCF ηC Φ" by (rule η'_def)
    fix θ assume prems:
      "θ : 𝔉 ↦CF 𝔉' : ℭ ↦↦C⇘α⇙ 𝔇"
      "?η' = 𝔊 ∘CF-NTCF θ ∙NTCF ηC Φ"
    interpret θ: is_ntcf α ℭ 𝔇 𝔉 𝔉' θ by (rule prems(1))
    from prems have η'_a: 
      "?η'⦇NTMap⦈⦇a⦈ = (𝔊 ∘CF-NTCF θ ∙NTCF ηC Φ)⦇NTMap⦈⦇a⦈" 
      for a
      by simp
    have η'a: "ηC Ψ⦇NTMap⦈⦇a⦈ =
      𝔊⦇ArrMap⦈⦇θ⦇NTMap⦈⦇a⦈⦈ ∘A⇘ℭ⇙ ηC Φ⦇NTMap⦈⦇a⦈"
      if "a ∈∘ ℭ⦇Obj⦈" for a
      using η'_a[where a=a] that
      by 
        (
          cs_prems cs_shallow 
            cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
        )
    show "θ = ?ΦΨ"
    proof(rule ntcf_eqI)
      have dom_lhs: "𝒟∘ (θ⦇NTMap⦈) = ℭ⦇Obj⦈" 
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      have dom_rhs: "𝒟∘ (?ΦΨ⦇NTMap⦈) = ℭ⦇Obj⦈"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps)
      show "θ⦇NTMap⦈ = ?ΦΨ⦇NTMap⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix a assume prems': "a ∈∘ ℭ⦇Obj⦈"
        let ?uof = ‹umap_of 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (?η⦇NTMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇a⦈)›
        from cf_adj_LR_iso_app_unique[OF assms prems'] obtain f' 
          where f': "f' : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
            and η_def: "?η'⦇NTMap⦈⦇a⦈ = ?uof⦇ArrVal⦈⦇f'⦈"
            and unique_f': "⋀f''.
              ⟦
                f'' : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈;
                ?η'⦇NTMap⦈⦇a⦈ = ?uof⦇ArrVal⦈⦇f''⦈
              ⟧ ⟹ f'' = f'"
          by metis
        from prems' have θa: "θ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
          by (cs_concl cs_shallow cs_intro: cat_cs_intros)
        from η_def f' prems' have 
          "ηC Ψ⦇NTMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇f'⦈ ∘A⇘ℭ⇙ ηC Φ⦇NTMap⦈⦇a⦈"
          by 
            (
              cs_prems
                cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
            )
        from prems' have "ηC Ψ⦇NTMap⦈⦇a⦈ = ?uof⦇ArrVal⦈⦇θ⦇NTMap⦈⦇a⦈⦈"
          by 
            (
              cs_concl
                cs_simp: cat_cs_simps η'a[OF prems'] 
                cs_intro: adj_cs_intros cat_cs_intros
            )
        from unique_f'[OF θa this] have θa: "θ⦇NTMap⦈⦇a⦈ = f'".
        from prems' have Ψa: 
          "?ΦΨ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
        from prems' have "ηC Ψ⦇NTMap⦈⦇a⦈ = ?uof⦇ArrVal⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈"
          by
            (
              cs_concl
                cs_simp: cf_adj_LR_iso_app_unique(3)[OF assms] cat_cs_simps 
                cs_intro: adj_cs_intros cat_cs_intros
            )
        from unique_f'[OF Ψa this] have 𝔉'Ψ_def: "?ΦΨ⦇NTMap⦈⦇a⦈ = f'".
        show "θ⦇NTMap⦈⦇a⦈ = ?ΦΨ⦇NTMap⦈⦇a⦈" unfolding θa 𝔉'Ψ_def ..
      qed auto
    qed (cs_concl cs_shallow cs_intro: cat_cs_intros)+
  qed

qed

lemma op_ntcf_cf_adj_RL_iso[cat_op_simps]:
  assumes "Φ : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" 
    and "Ψ : 𝔉 ⇌CF 𝔊' : ℭ ⇌⇌C⇘α⇙ 𝔇" 
  defines "op_𝔇 ≡ op_cat 𝔇"
    and "op_ℭ ≡ op_cat ℭ"
    and "op_𝔉 ≡ op_cf 𝔉"
    and "op_𝔊 ≡ op_cf 𝔊"
    and "op_Φ ≡ op_cf_adj Φ"
    and "op_𝔊' ≡ op_cf 𝔊'"
    and "op_Ψ ≡ op_cf_adj Ψ"
  shows
    "op_ntcf (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ) =
      cf_adj_LR_iso op_𝔇 op_ℭ op_𝔉 op_𝔊 op_Φ op_𝔊' op_Ψ"
proof-
  interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
  interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊' Ψ by (rule assms(2))
  interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘CF 𝔊› ‹cf_id 𝔇› ‹εC Φ›
    by (rule Φ.cf_adjunction_counit_is_ntcf)
  have dom_lhs: "𝒟∘ (op_ntcf (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ)) = 5ℕ"
    unfolding op_ntcf_def by (simp add: nat_omega_simps)
  show ?thesis
  proof(rule vsv_eqI, unfold dom_lhs)
    fix a assume prems: "a ∈∘ 5ℕ"
    then have "a ∈∘ 5ℕ" unfolding dom_lhs by simp
    then show 
      "op_ntcf (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ)⦇a⦈ =
        cf_adj_LR_iso op_𝔇 op_ℭ op_𝔉 op_𝔊 op_Φ op_𝔊' op_Ψ⦇a⦈"
      by 
        (
          elim_in_numeral, 
          fold nt_field_simps, 
          unfold 
            cf_adj_LR_iso_components 
            op_ntcf_components 
            cf_adj_RL_iso_components
            Let_def
            Φ.cf_adjunction_unit_NTMap_op 
            Ψ.cf_adjunction_unit_NTMap_op
            assms(3-9)
            cat_op_simps
        )
        simp_all
  qed (auto simp: op_ntcf_def cf_adj_LR_iso_def nat_omega_simps)
qed

lemma op_ntcf_cf_adj_LR_iso[cat_op_simps]:
  assumes "Φ : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" and "Ψ : 𝔉' ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" 
  defines "op_𝔇 ≡ op_cat 𝔇"
    and "op_ℭ ≡ op_cat ℭ"
    and "op_𝔉 ≡ op_cf 𝔉"
    and "op_𝔊 ≡ op_cf 𝔊"
    and "op_Φ ≡ op_cf_adj Φ"
    and "op_𝔉' ≡ op_cf 𝔉'"
    and "op_Ψ ≡ op_cf_adj Ψ"
  shows
    "op_ntcf (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ) =
      cf_adj_RL_iso op_𝔇 op_ℭ op_𝔊 op_𝔉 op_Φ op_𝔉' op_Ψ"
proof-
  interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
  interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉' 𝔊 Ψ by (rule assms(2))
  interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘CF 𝔊› ‹cf_id 𝔇› ‹εC Φ›
    by (rule Φ.cf_adjunction_counit_is_ntcf)
  have dom_lhs: "𝒟∘ (op_ntcf (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ)) = 5ℕ"
    unfolding op_ntcf_def by (simp add: nat_omega_simps)
  show ?thesis
  proof(rule vsv_eqI, unfold dom_lhs)
    fix a assume prems: "a ∈∘ 5ℕ"
    then show
      "op_ntcf (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ)⦇a⦈ =
        cf_adj_RL_iso op_𝔇 op_ℭ op_𝔊 op_𝔉 op_Φ op_𝔉' op_Ψ⦇a⦈"
      by
        (
          elim_in_numeral, 
          use nothing in 
            ‹
              fold nt_field_simps,
              unfold 
                cf_adj_LR_iso_components
                op_ntcf_components
                cf_adj_RL_iso_components
                Let_def
                Φ.op_ntcf_cf_adjunction_unit[symmetric]
                Ψ.op_ntcf_cf_adjunction_unit[symmetric]
                assms(3-9)
                cat_op_simps
            ›
        )
        simp_all
  qed (auto simp: op_ntcf_def cf_adj_RL_iso_def nat_omega_simps)
qed

lemma cf_adj_RL_iso_app_unique:
  fixes ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ
  assumes "Φ : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" 
    and "Ψ : 𝔉 ⇌CF 𝔊' : ℭ ⇌⇌C⇘α⇙ 𝔇" 
    and "x ∈∘ 𝔇⦇Obj⦈"
  defines "𝔊x ≡ 𝔊⦇ObjMap⦈⦇x⦈"
    and "𝔊'x ≡ 𝔊'⦇ObjMap⦈⦇x⦈"
    and "ε ≡ εC Φ" 
    and "ε' ≡ εC Ψ"
    and "f ≡ cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈⦇x⦈"
  shows
    "∃!f'.
      f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
      ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈"
    "f : 𝔊'x ↦iso⇘ℭ⇙ 𝔊x"
    "ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f⦈"
proof-
  interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
  interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊' Ψ by (rule assms(2))
  interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘CF 𝔊› ‹cf_id 𝔇› ‹εC Φ›
    by (rule Φ.cf_adjunction_counit_is_ntcf)
  show
    "∃!f'.
      f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
      ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈"
    "f : 𝔊'x ↦iso⇘ℭ⇙ 𝔊x"
    "ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f⦈"
    by 
      (
        intro cf_adj_LR_iso_app_unique
          [
            OF Φ.is_cf_adjunction_op Ψ.is_cf_adjunction_op,
            unfolded cat_op_simps,
            OF assms(3),
            unfolded Ψ.cf_adjunction_unit_NTMap_op,
            folded Φ.op_ntcf_cf_adjunction_counit,
            folded op_ntcf_cf_adj_RL_iso[OF assms(1,2)],
            unfolded cat_op_simps,
            folded assms(4-8)
          ]
      )+
qed

lemma cf_adj_RL_iso_is_iso_functor:
  ―‹See Corollary 1 in Chapter IV-1 in \cite{mac_lane_categories_2010}.›
  assumes "Φ : 𝔉 ⇌CF 𝔊 : ℭ ⇌⇌C⇘α⇙ 𝔇" and "Ψ : 𝔉 ⇌CF 𝔊' : ℭ ⇌⇌C⇘α⇙ 𝔇" 
  shows "∃!θ.
    θ : 𝔊' ↦CF 𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ ∧
    εC Ψ = εC Φ ∙NTCF (𝔉 ∘CF-NTCF θ)"
    and "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ : 𝔊' ↦CF.iso 𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    and "εC Ψ =
      εC Φ ∙NTCF (𝔉 ∘CF-NTCF cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ)"
proof-
  interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
  interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊' Ψ by (rule assms(2))
  interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘CF 𝔊› ‹cf_id 𝔇› ‹εC Φ›
    by (rule Φ.cf_adjunction_counit_is_ntcf)
  note cf_adj_LR_iso_is_iso_functor_op = cf_adj_LR_iso_is_iso_functor
    [
      OF Φ.is_cf_adjunction_op Ψ.is_cf_adjunction_op,
      folded 
        Φ.op_ntcf_cf_adjunction_counit 
        Ψ.op_ntcf_cf_adjunction_counit
        op_ntcf_cf_adj_RL_iso[OF assms]
    ]
  from cf_adj_LR_iso_is_iso_functor_op(1) obtain θ 
    where θ: "θ : op_cf 𝔊 ↦CF op_cf 𝔊' : op_cat 𝔇 ↦↦C⇘α⇙ op_cat ℭ"
      and op_ntcf_ε_def: "op_ntcf (εC Ψ) =
        op_cf 𝔉 ∘CF-NTCF θ ∙NTCF op_ntcf (εC Φ)"
      and unique_θ': 
        "⟦
          θ' : op_cf 𝔊 ↦CF op_cf 𝔊' : op_cat 𝔇 ↦↦C⇘α⇙ op_cat ℭ;
          op_ntcf (εC Ψ) = op_cf 𝔉 ∘CF-NTCF θ' ∙NTCF op_ntcf (εC Φ)
         ⟧ ⟹ θ' = θ"
      for θ'
    by metis
  interpret θ: is_ntcf α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔊'› θ 
    by (rule θ)
  show "∃!θ. θ : 𝔊' ↦CF 𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ ∧ εC Ψ = εC Φ ∙NTCF (𝔉 ∘CF-NTCF θ)"
  proof(intro ex1I conjI; (elim conjE)?)
    show op_θ: "op_ntcf θ : 𝔊' ↦CF 𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
      by (rule θ.is_ntcf_op[unfolded cat_op_simps])
    from op_ntcf_ε_def have
      "op_ntcf (op_ntcf (εC Ψ)) =
        op_ntcf (op_cf 𝔉 ∘CF-NTCF θ ∙NTCF op_ntcf (εC Φ))"
      by simp
    then show ε_def: "εC Ψ = εC Φ ∙NTCF (𝔉 ∘CF-NTCF op_ntcf θ)"
      by 
        (
          cs_prems cs_shallow
            cs_simp: cat_op_simps 
            cs_intro: adj_cs_intros cat_cs_intros cat_op_intros
        )
    fix θ' assume prems: 
      "θ' : 𝔊' ↦CF 𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
      "εC Ψ = εC Φ ∙NTCF (𝔉 ∘CF-NTCF θ')"
    interpret θ': is_ntcf α 𝔇 ℭ 𝔊' 𝔊 θ' by (rule prems(1))   
    have "op_ntcf (εC Ψ) = op_cf 𝔉 ∘CF-NTCF op_ntcf θ' ∙NTCF op_ntcf (εC Φ)"
      by 
        (
          cs_concl cs_shallow
            cs_simp: 
              prems(2) 
              op_ntcf_cf_ntcf_comp[symmetric] 
              op_ntcf_ntcf_vcomp[symmetric] 
            cs_intro: cat_cs_intros
        )
    from unique_θ'[OF θ'.is_ntcf_op this, symmetric] have
      "op_ntcf θ = op_ntcf (op_ntcf θ')"
      by simp
    then show "θ' = op_ntcf θ"  
      by (cs_prems cs_shallow cs_simp: cat_cs_simps cat_op_simps) simp
  qed
  from is_iso_ntcf.is_iso_ntcf_op[OF cf_adj_LR_iso_is_iso_functor_op(2)] show 
    "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ : 𝔊' ↦CF.iso 𝔊 : 𝔇 ↦↦C⇘α⇙ ℭ"
    by 
      (
        cs_prems cs_shallow 
          cs_simp: cat_op_simps cs_intro: adj_cs_intros cat_op_intros
      )
  from cf_adj_LR_iso_is_iso_functor_op(3) have 
    "op_ntcf (op_ntcf (εC Ψ)) =
      op_ntcf
        (
          op_cf 𝔉 ∘CF-NTCF op_ntcf (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ) ∙NTCF 
          op_ntcf (εC Φ)
        )"
    by simp
  from 
    this 
    cf_adj_LR_iso_is_iso_functor_op(2)[ 
      unfolded op_ntcf_cf_adj_RL_iso[OF assms]
      ]
  show "εC Ψ = εC Φ ∙NTCF (𝔉 ∘CF-NTCF cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ)"
    by 
      (
        cs_prems cs_shallow
          cs_simp: cat_op_simps cat_op_simps 
          cs_intro: ntcf_cs_intros adj_cs_intros cat_cs_intros cat_op_intros
      )
qed



subsection‹Further properties of the adjoint functors›

lemma (in is_cf_adjunction) cf_adj_exp_cf_cat:
  ―‹See Proposition 4.4.6 in \cite{riehl_category_2016}.›
  assumes "𝒵 β" and "α ∈∘ β" and "category α 𝔍"
  shows
    "cf_adjunction_of_unit
      β
      (exp_cf_cat α 𝔉 𝔍)
      (exp_cf_cat α 𝔊 𝔍)
      (exp_ntcf_cat α (ηC Φ) 𝔍) :
      exp_cf_cat α 𝔉 𝔍 ⇌CF exp_cf_cat α 𝔊 𝔍 :
      cat_FUNCT α 𝔍 ℭ ⇌⇌C⇘β⇙ cat_FUNCT α 𝔍 𝔇"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  interpret 𝔍: category α 𝔍 by (rule assms(3))
  show ?thesis
  proof
    (
      rule counit_unit_is_cf_adjunction(1)[
        where ε = ‹exp_ntcf_cat α (εC Φ) 𝔍›
        ]
    )
    from assms show "exp_ntcf_cat α (ηC Φ) 𝔍 :
      cf_id (cat_FUNCT α 𝔍 ℭ) ↦CF exp_cf_cat α 𝔊 𝔍 ∘CF exp_cf_cat α 𝔉 𝔍 :
      cat_FUNCT α 𝔍 ℭ ↦↦C⇘β⇙ cat_FUNCT α 𝔍 ℭ"
      by 
        (
          cs_concl 
            cs_simp:
              cat_cs_simps cat_FUNCT_cs_simps 
              exp_cf_cat_cf_id_cat[symmetric] exp_cf_cat_cf_comp[symmetric] 
            cs_intro:
              cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros adj_cs_intros
        )
    from assms show 
      "exp_ntcf_cat α (εC Φ) 𝔍 :
        exp_cf_cat α 𝔉 𝔍 ∘CF exp_cf_cat α 𝔊 𝔍 ↦CF cf_id (cat_FUNCT α 𝔍 𝔇) :
        cat_FUNCT α 𝔍 𝔇 ↦↦C⇘β⇙ cat_FUNCT α 𝔍 𝔇"
      by
        (
          cs_concl 
            cs_simp:
              cat_cs_simps 
              cat_FUNCT_cs_simps 
              exp_cf_cat_cf_id_cat[symmetric] 
              exp_cf_cat_cf_comp[symmetric] 
            cs_intro:
              cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros adj_cs_intros
        )
    note [symmetric, cat_cs_simps] =
      ntcf_id_exp_cf_cat 
      exp_ntcf_cat_ntcf_vcomp 
      exp_ntcf_cat_ntcf_cf_comp
      exp_ntcf_cat_cf_ntcf_comp
    from assms show
      "(exp_cf_cat α 𝔊 𝔍 ∘CF-NTCF exp_ntcf_cat α (εC Φ) 𝔍) ∙NTCF
        (exp_ntcf_cat α (ηC Φ) 𝔍 ∘NTCF-CF exp_cf_cat α 𝔊 𝔍) =
        ntcf_id (exp_cf_cat α 𝔊 𝔍)"
      by 
        (
          cs_concl cs_shallow
            cs_simp: adj_cs_simps cat_cs_simps  
            cs_intro: adj_cs_intros cat_cs_intros
        )
    from assms show
      "exp_ntcf_cat α (εC Φ) 𝔍 ∘NTCF-CF exp_cf_cat α 𝔉 𝔍 ∙NTCF
      (exp_cf_cat α 𝔉 𝔍 ∘CF-NTCF exp_ntcf_cat α (ηC Φ) 𝔍) =
      ntcf_id (exp_cf_cat α 𝔉 𝔍)"
      by 
        (
          cs_concl cs_shallow
            cs_simp: adj_cs_simps cat_cs_simps  
            cs_intro: adj_cs_intros cat_cs_intros
        )
  qed
    (
      use assms in 
        ‹
          cs_concl 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        ›
    )+
qed

lemma (in is_cf_adjunction) cf_adj_exp_cf_cat_exp_cf_cat:
  ―‹See Proposition 4.4.6 in \cite{riehl_category_2016}.›
  assumes "𝒵 β" and "α ∈∘ β" and "category α 𝔄"
  shows
    "cf_adjunction_of_unit
      β
      (exp_cat_cf α 𝔄 𝔊)
      (exp_cat_cf α 𝔄 𝔉)
      (exp_cat_ntcf α 𝔄 (ηC Φ)) :
      exp_cat_cf α 𝔄 𝔊 ⇌CF exp_cat_cf α 𝔄 𝔉 :
      cat_FUNCT α ℭ 𝔄 ⇌⇌C⇘β⇙ cat_FUNCT α 𝔇 𝔄"
proof-

  interpret β: 𝒵 β by (rule assms(1))
  interpret 𝔄: category α 𝔄 by (rule assms(3))

  show ?thesis
  proof
    (
      rule counit_unit_is_cf_adjunction(1)[
        where ε = ‹exp_cat_ntcf α 𝔄 (εC Φ)›
        ]
    )
    from assms is_cf_adjunction_axioms show
      "exp_cat_ntcf α 𝔄 (ηC Φ) :
        cf_id (cat_FUNCT α ℭ 𝔄) ↦CF exp_cat_cf α 𝔄 𝔉 ∘CF exp_cat_cf α 𝔄 𝔊 :
        cat_FUNCT α ℭ 𝔄 ↦↦C⇘β⇙ cat_FUNCT α ℭ 𝔄"
      by 
        (
          cs_concl 
            cs_simp:
              exp_cat_cf_cat_cf_id[symmetric] exp_cat_cf_cf_comp[symmetric] 
            cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros adj_cs_intros
        )
    from assms is_cf_adjunction_axioms show 
      "exp_cat_ntcf α 𝔄 (εC Φ) :
        exp_cat_cf α 𝔄 𝔊 ∘CF exp_cat_cf α 𝔄 𝔉 ↦CF cf_id (cat_FUNCT α 𝔇 𝔄) :
        cat_FUNCT α 𝔇 𝔄 ↦↦C⇘β⇙ cat_FUNCT α 𝔇 𝔄"
      by
        (
          cs_concl 
            cs_simp: 
              exp_cat_cf_cat_cf_id[symmetric] exp_cat_cf_cf_comp[symmetric] 
            cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros adj_cs_intros
        )
    note [symmetric, cat_cs_simps] =
      ntcf_id_exp_cat_cf
      exp_cat_ntcf_ntcf_vcomp
      exp_cat_ntcf_ntcf_cf_comp
      exp_cat_ntcf_cf_ntcf_comp
    from assms show
      "exp_cat_cf α 𝔄 𝔉 ∘CF-NTCF exp_cat_ntcf α 𝔄 (εC Φ) ∙NTCF
        (exp_cat_ntcf α 𝔄 (ηC Φ) ∘NTCF-CF exp_cat_cf α 𝔄 𝔉) =
        ntcf_id (exp_cat_cf α 𝔄 𝔉)"
      by
        (
          cs_concl cs_shallow
            cs_simp: adj_cs_simps cat_cs_simps
            cs_intro: adj_cs_intros cat_cs_intros
        )
    from assms show
      "exp_cat_ntcf α 𝔄 (εC Φ) ∘NTCF-CF exp_cat_cf α 𝔄 𝔊 ∙NTCF
        (exp_cat_cf α 𝔄 𝔊 ∘CF-NTCF exp_cat_ntcf α 𝔄 (ηC Φ)) =
          ntcf_id (exp_cat_cf α 𝔄 𝔊)"
      by 
        (
          cs_concl cs_shallow
            cs_simp: adj_cs_simps cat_cs_simps
            cs_intro: adj_cs_intros cat_cs_intros
        )
  qed
    (
      use assms in 
        ‹
          cs_concl 
            cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
        ›
    )+

qed



subsection‹Adjoints on limits›

lemma cf_AdjRight_preserves_limits:
  ―‹See Chapter V-5 in \cite{mac_lane_categories_2010}.›
  assumes "Φ : 𝔉 ⇌CF 𝔊 : 𝔛 ⇌⇌C⇘α⇙ 𝔄"
  shows "is_cf_continuous α 𝔊"
proof(intro is_cf_continuousI)
 
  interpret Φ: is_cf_adjunction α 𝔛 𝔄 𝔉 𝔊 Φ by (rule assms(1))

  show "𝔊 : 𝔄 ↦↦C⇘α⇙ 𝔛" by (rule Φ.RL.is_functor_axioms)

  fix 𝔗 𝔍 assume prems: "𝔗 : 𝔍 ↦↦C⇘α⇙ 𝔄"

  show "cf_preserves_limits α 𝔊 𝔗"
  proof(intro cf_preserves_limitsI, rule prems, rule Φ.RL.is_functor_axioms)

    fix τ a assume "τ : a <CF.lim 𝔗 : 𝔍 ↦↦C⇘α⇙ 𝔄"
    then interpret τ: is_cat_limit α 𝔍 𝔄 𝔗 a τ . 

    show "𝔊 ∘CF-NTCF τ : 𝔊⦇ObjMap⦈⦇a⦈ <CF.lim 𝔊 ∘CF 𝔗 : 𝔍 ↦↦C⇘α⇙ 𝔛"
    proof(intro is_cat_limitI)

      show "𝔊 ∘CF-NTCF τ : 𝔊⦇ObjMap⦈⦇a⦈ <CF.cone 𝔊 ∘CF 𝔗 : 𝔍 ↦↦C⇘α⇙ 𝔛"
        by
          (
            intro cf_ntcf_comp_cf_cat_cone prems, 
            rule τ.is_cat_cone_axioms, 
            intro Φ.RL.is_functor_axioms
          )

      fix σ' b' assume "σ' : b' <CF.cone 𝔊 ∘CF 𝔗 : 𝔍 ↦↦C⇘α⇙ 𝔛"
      then interpret σ': is_cat_cone α b' 𝔍 𝔛 ‹𝔊 ∘CF 𝔗› σ' .

      have "εC Φ ∘NTCF-CF 𝔗 : 𝔉 ∘CF (𝔊 ∘CF 𝔗) ↦CF 𝔗 : 𝔍 ↦↦C⇘α⇙ 𝔄"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
      moreover have "𝔉 ∘CF-NTCF σ' :
        𝔉⦇ObjMap⦈⦇b'⦈ <CF.cone 𝔉 ∘CF (𝔊 ∘CF 𝔗) : 𝔍 ↦↦C⇘α⇙ 𝔄"
        by 
          (
            intro cf_ntcf_comp_cf_cat_cone, 
            rule σ'.is_cat_cone_axioms, 
            rule Φ.LR.is_functor_axioms
          )
      ultimately have "(εC Φ ∘NTCF-CF 𝔗) ∙NTCF (𝔉 ∘CF-NTCF σ') :
        𝔉⦇ObjMap⦈⦇b'⦈ <CF.cone 𝔗 : 𝔍 ↦↦C⇘α⇙ 𝔄"
        by (rule ntcf_vcomp_is_cat_cone)
      from τ.cat_lim_unique_cone'[OF this] obtain h 
        where h: "h : 𝔉⦇ObjMap⦈⦇b'⦈ ↦⇘𝔄⇙ a"
          and ε𝔗_𝔉σ': "⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹
            ((εC Φ ∘NTCF-CF 𝔗) ∙NTCF (𝔉 ∘CF-NTCF σ'))⦇NTMap⦈⦇j⦈ = τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ h"
          and h_unique:
            "⟦
              h' : 𝔉⦇ObjMap⦈⦇b'⦈ ↦⇘𝔄⇙ a;
              ⋀j. j ∈∘ 𝔍⦇Obj⦈ ⟹
                ((εC Φ ∘NTCF-CF 𝔗) ∙NTCF (𝔉 ∘CF-NTCF σ'))⦇NTMap⦈⦇j⦈ =
                  τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ h'
             ⟧ ⟹ h' = h"
        for h'
        by metis
      have ε𝔗_𝔉σ:
        "εC Φ⦇NTMap⦈⦇𝔗⦇ObjMap⦈⦇j⦈⦈ ∘A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇σ'⦇NTMap⦈⦇j⦈⦈ = 
          τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ h"
        if "j ∈∘ 𝔍⦇Obj⦈" for j
        using ε𝔗_𝔉σ'[OF that] that
        by
          (
            cs_prems cs_shallow 
              cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
          )

      show "∃!f'.
        f' : b' ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇a⦈ ∧ σ' = 𝔊 ∘CF-NTCF τ ∙NTCF ntcf_const 𝔍 𝔛 f'"
      proof(intro ex1I conjI; (elim conjE)?)
        let ?h' = ‹𝔊⦇ArrMap⦈⦇h⦈ ∘A⇘𝔛⇙ ηC Φ⦇NTMap⦈⦇b'⦈›
        from h show "?h' : b' ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇a⦈"
          by 
            (
              cs_concl cs_shallow 
                cs_intro: cat_cs_intros cat_lim_cs_intros adj_cs_intros
            )
        show "σ' = 𝔊 ∘CF-NTCF τ ∙NTCF ntcf_const 𝔍 𝔛 ?h'"
        proof(rule ntcf_eqI)
          show "σ' : cf_const 𝔍 𝔛 b' ↦CF 𝔊 ∘CF 𝔗 : 𝔍 ↦↦C⇘α⇙ 𝔛"
            by (rule σ'.is_ntcf_axioms)
          then have dom_lhs: "𝒟∘ (σ'⦇NTMap⦈) = 𝔍⦇Obj⦈" 
            by (cs_concl cs_shallow cs_simp: cat_cs_simps)
          from h show 
            "𝔊 ∘CF-NTCF τ ∙NTCF ntcf_const 𝔍 𝔛 ?h' : 
              cf_const 𝔍 𝔛 b' ↦CF 𝔊 ∘CF 𝔗 : 𝔍 ↦↦C⇘α⇙ 𝔛"
            by
              (
                cs_concl 
                  cs_simp: cat_cs_simps 
                  cs_intro: cat_lim_cs_intros adj_cs_intros cat_cs_intros
              )
          then have dom_rhs:
            "𝒟∘ ((𝔊 ∘CF-NTCF τ ∙NTCF ntcf_const 𝔍 𝔛 ?h')⦇NTMap⦈) = 𝔍⦇Obj⦈" 
            by (cs_concl cs_simp: cat_cs_simps)
          show "σ'⦇NTMap⦈ = (𝔊 ∘CF-NTCF τ ∙NTCF ntcf_const 𝔍 𝔛 ?h')⦇NTMap⦈"
          proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
            fix j assume prems': "j ∈∘ 𝔍⦇Obj⦈"
            note [cat_cs_simps] = Φ.L.cat_assoc_helper
              [
                  where h=‹𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈› 
                    and g=‹𝔊⦇ArrMap⦈⦇h⦈› 
                    and f=‹ηC Φ⦇NTMap⦈⦇b'⦈›
                    and q=‹𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ h⦈›
              ]
            from prems' h have [cat_cs_simps]: 
              "𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ h⦈ ∘A⇘𝔛⇙ ηC Φ⦇NTMap⦈⦇b'⦈ = σ'⦇NTMap⦈⦇j⦈"
              by 
                (
                  cs_concl cs_shallow 
                    cs_simp: cat_cs_simps ε𝔗_𝔉σ[OF prems', symmetric] 
                    cs_intro: adj_cs_intros cat_cs_intros
                )
            from prems' h show 
              "σ'⦇NTMap⦈⦇j⦈ = (𝔊 ∘CF-NTCF τ ∙NTCF ntcf_const 𝔍 𝔛 ?h')⦇NTMap⦈⦇j⦈"
              by 
                (
                  cs_concl 
                    cs_simp: cat_cs_simps  
                    cs_intro: cat_lim_cs_intros adj_cs_intros cat_cs_intros
                )
          qed (cs_concl cs_intro: V_cs_intros cat_cs_intros)+
        qed simp_all

        fix f' assume prems':
          "f' : b' ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇a⦈"
          "σ' = 𝔊 ∘CF-NTCF τ ∙NTCF ntcf_const 𝔍 𝔛 f'"

        from prems'(2) have σ'_j_def':
          "σ'⦇NTMap⦈⦇j⦈ = (𝔊 ∘CF-NTCF τ ∙NTCF ntcf_const 𝔍 𝔛 f')⦇NTMap⦈⦇j⦈"
          for j
          by simp
        have σ'_j_def: "σ'⦇NTMap⦈⦇j⦈ = 𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈ ∘A⇘𝔛⇙ f'" 
          if "j ∈∘ 𝔍⦇Obj⦈" for j
          using σ'_j_def'[of j] that prems'(1)
          by
            (
              cs_prems 
                cs_simp: cat_cs_simps cs_intro: cat_lim_cs_intros cat_cs_intros
            )

        from prems'(1) have εa_𝔉f':
          "εC Φ⦇NTMap⦈⦇a⦈ ∘A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇f'⦈ : 𝔉⦇ObjMap⦈⦇b'⦈ ↦⇘𝔄⇙ a"
          by (cs_concl cs_intro: cat_lim_cs_intros cat_cs_intros adj_cs_intros)

        interpret ε: is_ntcf α 𝔄 𝔄 ‹𝔉 ∘CF 𝔊› ‹cf_id 𝔄› ‹εC Φ›
          by (rule Φ.cf_adjunction_counit_is_ntcf)

        have 
          "(εC Φ ∘NTCF-CF 𝔗 ∙NTCF (𝔉 ∘CF-NTCF σ'))⦇NTMap⦈⦇j⦈ =
            τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ (εC Φ⦇NTMap⦈⦇a⦈ ∘A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇f'⦈)"
          if "j ∈∘ 𝔍⦇Obj⦈" for j
        proof-
          from that have "τ⦇NTMap⦈⦇j⦈ : a ↦⇘𝔄⇙ 𝔗⦇ObjMap⦈⦇j⦈"
            by 
              (
                cs_concl cs_shallow 
                  cs_simp: cat_cs_simps cs_intro: cat_cs_intros
              )
          from ε.ntcf_Comp_commute[OF this] that have [cat_cs_simps]:
            "εC Φ⦇NTMap⦈⦇𝔗⦇ObjMap⦈⦇j⦈⦈ ∘A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈⦈ =
              τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ εC Φ⦇NTMap⦈⦇a⦈"
            by 
              (
                cs_prems cs_shallow 
                  cs_simp: cat_cs_simps cs_intro: cat_cs_intros
              )
          note [cat_cs_simps] = Φ.R.cat_assoc_helper
            [
              where h=‹εC Φ⦇NTMap⦈⦇𝔗⦇ObjMap⦈⦇j⦈⦈› 
                and g=‹𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈⦈›
                and q=‹τ⦇NTMap⦈⦇j⦈ ∘A⇘𝔄⇙ εC Φ⦇NTMap⦈⦇a⦈›
            ]
          show ?thesis
          using that prems'(1)
            by
              (
                cs_concl
                  cs_simp: cat_cs_simps σ'_j_def
                  cs_intro: cat_lim_cs_intros cat_cs_intros adj_cs_intros
              )
        qed
        from h_unique[OF εa_𝔉f' this] have 
          "𝔊⦇ArrMap⦈⦇εC Φ⦇NTMap⦈⦇a⦈ ∘A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇f'⦈⦈ ∘A⇘𝔛⇙ ηC Φ⦇NTMap⦈⦇b'⦈ = ?h'"
          by simp
        from this prems'(1) show "f' = 𝔊⦇ArrMap⦈⦇h⦈ ∘A⇘𝔛⇙ ηC Φ⦇NTMap⦈⦇b'⦈"
          by
            (
              cs_prems 
                cs_simp: cat_cs_simps Φ.cf_adj_counit_unit_app 
                cs_intro: cat_lim_cs_intros cat_cs_intros
            )
      qed

    qed

  qed

qed

text‹\newpage›

end