[STATEMENT]
lemma universal_arrow_of_if_cat_representation:
  \<comment>\<open>See Proposition 2 in Chapter III-2 in \cite{mac_lane_categories_2010}.\<close>
  assumes "\<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>"
    and "cat_representation \<alpha> \<KK> r \<psi>"
    and "\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>"
  shows "universal_arrow_of
    \<KK> (set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
note r\<psi> = cat_representationD[OF assms(2,1)]
[PROOF STATE]
proof (state)
this:
r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<psi> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>

goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
interpret \<KK>: is_functor \<alpha> \<CC> \<open>cat_Set \<alpha>\<close> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
interpret \<psi>: is_iso_ntcf \<alpha> \<CC> \<open>cat_Set \<alpha>\<close> \<open>Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-)\<close> \<KK> \<psi>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
[PROOF STEP]
by (rule r\<psi>(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
have set_\<aa>: "set {\<aa>} \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ZFC_in_HOL.set {\<aa>} \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: Limit_vsingleton_in_VsetI cat_Set_components(1))
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set {\<aa>} \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
from
    ntcf_cf_comp_is_iso_ntcf[
      OF \<KK>.ntcf_pointed_inv_is_iso_ntcf[OF assms(3)] assms(1)
      ]
[PROOF STATE]
proof (chain)
picking this:
ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : dghm_id (cat_Set \<alpha>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
[PROOF STEP]
have \<aa>\<KK>: "ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> :
    \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha> (set {\<aa>},-) \<circ>\<^sub>C\<^sub>F \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>"
[PROOF STATE]
proof (prove)
using this:
ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : dghm_id (cat_Set \<alpha>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>

goal (1 subgoal):
 1. ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
[PROOF STEP]
by (cs_prems cs_simp: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>

goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
from iso_ntcf_is_iso_arr(1)[OF \<aa>\<KK>] r\<psi> assms(3)
[PROOF STATE]
proof (chain)
picking this:
inv_ntcf (ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<psi> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>
[PROOF STEP]
have [cat_cs_simps]:
    "((ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<psi>)\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>) =
      ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
inv_ntcf (ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>cat_Set \<alpha>(ZFC_in_HOL.set {\<aa>},-) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
r \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
\<psi> : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<alpha>\<^esub>\<CC>(r,-) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o \<KK> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> cat_Set \<alpha>
\<aa> \<in>\<^sub>\<circ> cat_Set \<alpha>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<psi>)\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr> = ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>)
[PROOF STEP]
by
      (
        cs_concl
          cs_simp: cat_cs_simps
          cs_intro: cat_Set_cs_intros cat_cs_intros cat_op_intros
      )
[PROOF STATE]
proof (state)
this:
(ntcf_pointed_inv \<alpha> \<aa> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<psi>)\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr> = ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>)

goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
show "universal_arrow_of
    \<KK> (set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))
[PROOF STEP]
by
      (
        rule \<KK>.cf_universal_arrow_of_if_is_iso_ntcf
          [
            OF r\<psi>(1) set_\<aa> ntcf_vcomp_is_iso_ntcf[OF \<aa>\<KK> r\<psi>(2)], 
            unfolded cat_cs_simps
          ]
      )
[PROOF STATE]
proof (state)
this:
universal_arrow_of \<KK> (ZFC_in_HOL.set {\<aa>}) r (ntcf_paa \<aa> (\<KK>\<lparr>ObjMap\<rparr>\<lparr>r\<rparr>) (\<psi>\<lparr>NTMap\<rparr>\<lparr>r\<rparr>\<lparr>ArrVal\<rparr>\<lparr>\<CC>\<lparr>CId\<rparr>\<lparr>r\<rparr>\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed