[STATEMENT]
lemma the_ntcf_lKe_is_cat_lKe:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<And>c. c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> lim_Obj c\<lparr>UArr\<rparr> :
      \<TT> \<circ>\<^sub>C\<^sub>F \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj :
    \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<KK>: is_functor \<alpha> \<BB> \<CC> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
interpret \<TT>: is_functor \<alpha> \<BB> \<AA> \<TT>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
assume prems: "c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
c \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
from assms(3)[OF this]
[PROOF STATE]
proof (chain)
picking this:
lim_Obj c\<lparr>UArr\<rparr> : \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have lim_Obj_UArr: "lim_Obj c\<lparr>UArr\<rparr> :
      \<TT> \<circ>\<^sub>C\<^sub>F \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
lim_Obj c\<lparr>UArr\<rparr> : \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. lim_Obj c\<lparr>UArr\<rparr> : \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lim_Obj c\<lparr>UArr\<rparr> : \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lim_Obj c\<lparr>UArr\<rparr> : \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret lim_Obj_c: is_cat_colimit
      \<alpha> \<open>\<KK> \<^sub>C\<^sub>F\<down> c\<close> \<AA> \<open>\<TT> \<circ>\<^sub>C\<^sub>F \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c\<close> \<open>lim_Obj c\<lparr>UObj\<rparr>\<close> \<open>lim_Obj c\<lparr>UArr\<rparr>\<close>
[PROOF STATE]
proof (prove)
using this:
lim_Obj c\<lparr>UArr\<rparr> : \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. lim_Obj c\<lparr>UArr\<rparr> : \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<^sub>C\<^sub>F\<Sqinter>\<^sub>O c >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m lim_Obj c\<lparr>UObj\<rparr> : \<KK> \<^sub>C\<^sub>F\<down> c \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
note op_ua_UArr_is_cat_limit'[
      where lim_Obj=lim_Obj, OF assms(1,2) prems lim_Obj_UArr
      ]
[PROOF STATE]
proof (state)
this:
op_ua lim_Obj \<KK> c\<lparr>UArr\<rparr> : lim_Obj c\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M c \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : c \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>

goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?c2 \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> op_ua lim_Obj \<KK> ?c2\<lparr>UArr\<rparr> : lim_Obj ?c2\<lparr>UObj\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m op_cf \<TT> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?c2 \<^sub>O\<Sqinter>\<^sub>C\<^sub>F (op_cf \<KK>) : ?c2 \<down>\<^sub>C\<^sub>F (op_cf \<KK>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>

goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
note the_ntcf_rKe_is_cat_rKe = the_ntcf_rKe_is_cat_rKe
    [
      OF \<KK>.is_functor_op \<TT>.is_functor_op,
      unfolded cat_op_simps,
      where lim_Obj=\<open>op_ua lim_Obj \<KK>\<close>,
      unfolded cat_op_simps,
      OF this,
      simplified,
      folded the_cf_lKe_def the_ntcf_lKe_def
    ]
[PROOF STATE]
proof (state)
this:
the_ntcf_rKe \<alpha> (op_cf \<TT>) (op_cf \<KK>) (op_ua lim_Obj \<KK>) : the_cf_rKe \<alpha> (op_cf \<TT>) (op_cf \<KK>) (op_ua lim_Obj \<KK>) \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>

goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
by
      (
        rule is_cat_rKe.is_cat_lKe_op
          [
            OF the_ntcf_rKe_is_cat_rKe,
            unfolded cat_op_simps,
            folded the_cf_lKe_def the_ntcf_lKe_def
          ]
      )
[PROOF STATE]
proof (state)
this:
the_ntcf_lKe \<alpha> \<TT> \<KK> lim_Obj : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> the_cf_lKe \<alpha> \<TT> \<KK> lim_Obj \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_cat_rKe_preserves) is_cat_rKe_preserves_axioms':
  assumes "\<alpha>' = \<alpha>"
    and "\<GG>' = \<GG>"
    and "\<KK>' = \<KK>"
    and "\<TT>' = \<TT>"
    and "\<HH>' = \<HH>"
    and "\<BB>' = \<BB>"
    and "\<AA>' = \<AA>"
    and "\<CC>' = \<CC>"
    and "\<DD>' = \<DD>"
  shows "\<epsilon> : \<GG>' \<circ>\<^sub>C\<^sub>F \<KK>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>'\<^esub> \<TT>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C (\<HH>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C \<DD>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG>' \<circ>\<^sub>C\<^sub>F \<KK>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>'\<^esub> \<TT>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<HH>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C \<DD>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>C \<DD>
[PROOF STEP]
by (rule is_cat_rKe_preserves_axioms)


[STATEMENT]
lemma (in is_cat_lKe_preserves) is_cat_lKe_preserves_axioms':
  assumes "\<alpha>' = \<alpha>"
    and "\<FF>' = \<FF>"
    and "\<KK>' = \<KK>"
    and "\<TT>' = \<TT>"
    and "\<HH>' = \<HH>"
    and "\<BB>' = \<BB>"
    and "\<AA>' = \<AA>"
    and "\<CC>' = \<CC>"
    and "\<DD>' = \<DD>"
  shows "\<eta> : \<TT>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF>' \<circ>\<^sub>C\<^sub>F \<KK>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C (\<HH>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C \<DD>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF>' \<circ>\<^sub>C\<^sub>F \<KK>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<HH>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C \<DD>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>C \<DD>
[PROOF STEP]
by (rule is_cat_lKe_preserves_axioms)


[STATEMENT]
lemma (in is_cat_rKe_preserves) is_cat_rKe_preserves_op:
  "op_ntcf \<epsilon> :
    op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> :
    op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C (op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C op_cat \
)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<epsilon> : op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C op_cat \

[PROOF STEP]
proof(intro is_cat_lKe_preservesI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. op_ntcf \<epsilon> : op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>
 2. op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \

 3. op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_ntcf \<epsilon> : op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \

[PROOF STEP]
from cat_rKe_preserves
[PROOF STATE]
proof (chain)
picking this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
show "op_cf \<HH> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F op_ntcf \<epsilon> :
    op_cf \<HH> \<circ>\<^sub>C\<^sub>F op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> (op_cf \<HH> \<circ>\<^sub>C\<^sub>F op_cf \<GG>) \<circ>\<^sub>C\<^sub>F op_cf \<KK> :
    op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \
"
[PROOF STATE]
proof (prove)
using this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<epsilon> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<TT> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

goal (1 subgoal):
 1. op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_ntcf \<epsilon> : op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \

[PROOF STEP]
by (cs_concl_step op_ntcf_cf_ntcf_comp[symmetric])
      (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
[PROOF STATE]
proof (state)
this:
op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_ntcf \<epsilon> : op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \

goal (2 subgoals):
 1. op_ntcf \<epsilon> : op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>
 2. op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \

[PROOF STEP]
qed (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+


[STATEMENT]
lemma (in is_cat_rKe_preserves) is_cat_lKe_preserves_op'[cat_op_intros]:
  assumes "\<TT>' = op_cf \<TT>"
    and "\<GG>' = op_cf \<GG>"
    and "\<KK>' = op_cf \<KK>"
    and "\<BB>' = op_cat \<BB>"
    and "\<AA>' = op_cat \<AA>"
    and "\<CC>' = op_cat \<CC>"
    and "\<DD>' = op_cat \<DD>"
    and "\<HH>' = op_cf \<HH>"
  shows "op_ntcf \<epsilon> :
    \<TT>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<GG>' \<circ>\<^sub>C\<^sub>F \<KK>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C (\<HH>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C \<DD>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<epsilon> : \<TT>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<GG>' \<circ>\<^sub>C\<^sub>F \<KK>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<HH>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C \<DD>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<epsilon> : op_cf \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<GG> \<circ>\<^sub>C\<^sub>F op_cf \<KK> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C op_cat \<DD>
[PROOF STEP]
by (rule is_cat_rKe_preserves_op)


[STATEMENT]
lemma (in is_cat_lKe_preserves) is_cat_rKe_preserves_op:
  "op_ntcf \<eta> :
    op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<TT> :
    op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C (op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C op_cat \
)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<eta> : op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C op_cat \

[PROOF STEP]
proof(intro is_cat_rKe_preservesI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. op_ntcf \<eta> : op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>
 2. op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \

 3. op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_ntcf \<eta> : op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \

[PROOF STEP]
from cat_lKe_preserves
[PROOF STATE]
proof (chain)
picking this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

[PROOF STEP]
show "op_cf \<HH> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F op_ntcf \<eta> :
    (op_cf \<HH> \<circ>\<^sub>C\<^sub>F op_cf \<FF>) \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<HH> \<circ>\<^sub>C\<^sub>F op_cf \<TT> :
    op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \
"
[PROOF STATE]
proof (prove)
using this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<eta> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C \<CC> \<mapsto>\<^sub>C \

goal (1 subgoal):
 1. op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_ntcf \<eta> : op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \

[PROOF STEP]
by (cs_concl_step op_ntcf_cf_ntcf_comp[symmetric])
      (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
[PROOF STATE]
proof (state)
this:
op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_ntcf \<eta> : op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \

goal (2 subgoals):
 1. op_ntcf \<eta> : op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cat \<AA>
 2. op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \

[PROOF STEP]
qed (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)+


[STATEMENT]
lemma (in is_cat_lKe_preserves) is_cat_rKe_preserves_op'[cat_op_intros]:
  assumes "\<TT>' = op_cf \<TT>"
    and "\<FF>' = op_cf \<FF>"
    and "\<KK>' = op_cf \<KK>"
    and "\<HH>' = op_cf \<HH>"
    and "\<BB>' = op_cat \<BB>"
    and "\<AA>' = op_cat \<AA>"
    and "\<CC>' = op_cat \<CC>"
    and "\<DD>' = op_cat \<DD>"
  shows "op_ntcf \<eta> :
    \<FF>' \<circ>\<^sub>C\<^sub>F \<KK>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C (\<HH>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C \<DD>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<eta> : \<FF>' \<circ>\<^sub>C\<^sub>F \<KK>' \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT>' : \<BB>' \<mapsto>\<^sub>C \<CC>' \<mapsto>\<^sub>C \<HH>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C \<DD>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<eta> : op_cf \<FF> \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> op_cf \<TT> : op_cat \<BB> \<mapsto>\<^sub>C op_cat \<CC> \<mapsto>\<^sub>C op_cf \<HH> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C op_cat \<DD>
[PROOF STEP]
by (rule is_cat_rKe_preserves_op)


[STATEMENT]
lemma cat_rKe_is_cat_limit:
  \<comment>\<open>The statement of the theorem is similar to the statement of a part of
    Theorem 1 in Chapter X-7 in \cite{mac_lane_categories_2010}
    or Proposition 6.5.1 in \cite{riehl_category_2016}.\<close>
  assumes "\<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "\<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret \<epsilon>: is_cat_rKe \<alpha> \<BB> \<open>cat_1 \<aa> \<ff>\<close> \<AA> \<KK> \<TT> \<GG> \<epsilon>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>r\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<TT> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret \<TT>: is_functor \<alpha> \<BB> \<AA> \<TT>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
from cat_1_components(1)
[PROOF STATE]
proof (chain)
picking this:
cat_1 ?\<aa> ?\<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {?\<aa>}
[PROOF STEP]
have \<aa>: "\<aa> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
cat_1 ?\<aa> ?\<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {?\<aa>}

goal (1 subgoal):
 1. \<aa> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: \<epsilon>.AG.HomCod.cat_in_Obj_in_Vset)
[PROOF STATE]
proof (state)
this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
from cat_1_components(2)
[PROOF STATE]
proof (chain)
picking this:
cat_1 ?\<aa> ?\<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {?\<ff>}
[PROOF STEP]
have \<ff>: "\<ff> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
cat_1 ?\<aa> ?\<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {?\<ff>}

goal (1 subgoal):
 1. \<ff> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: \<epsilon>.AG.HomCod.cat_in_Arr_in_Vset)
[PROOF STATE]
proof (state)
this:
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have \<KK>_def: "\<KK> = cf_const \<BB> (cat_1 \<aa> \<ff>) \<aa>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)
[PROOF STEP]
by (rule cf_const_if_HomCod_is_cat_1)
      (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<KK> = dghm_const \<BB> (cat_1 \<aa> \<ff>) \<aa> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr>)

goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have \<GG>\<KK>_def: "\<GG> \<circ>\<^sub>C\<^sub>F \<KK> = cf_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = dghm_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: cat_1_components(1) \<KK>_def cat_cs_simps
          cs_intro: V_cs_intros cat_cs_intros
      )
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = dghm_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)

goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret \<epsilon>: is_ntcf \<alpha> \<BB> \<AA> \<open>\<GG> \<circ>\<^sub>C\<^sub>F \<KK>\<close> \<TT> \<epsilon>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show "\<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof(intro is_cat_limitI is_cat_coneI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<epsilon> : dghm_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 2. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 3. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
show "\<epsilon> : cf_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<epsilon> : dghm_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule \<epsilon>.ntcf_rKe.is_ntcf_axioms[unfolded \<GG>\<KK>_def])
[PROOF STATE]
proof (state)
this:
\<epsilon> : dghm_const \<BB> \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (2 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 2. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
fix u' r'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 2. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
assume prems: "u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (state)
this:
u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (2 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 2. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
interpret u': is_cat_cone \<alpha> r' \<BB> \<AA> \<TT> u'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule prems)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 2. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
have \<GG>_def: "\<GG> = cf_const (cat_1 \<aa> \<ff>) \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> = dghm_const (cat_1 \<aa> \<ff>) \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)
[PROOF STEP]
by (rule cf_const_if_HomDom_is_cat_1[OF \<epsilon>.Ran.is_functor_axioms])
[PROOF STATE]
proof (state)
this:
\<GG> = dghm_const (cat_1 \<aa> \<ff>) \<AA> (\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>) (\<AA>\<lparr>CId\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>\<rparr>)

goal (2 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 2. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have const_r': "cf_const (cat_1 \<aa> \<ff>) \<AA> r' : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps cs_intro: cat_lim_cs_intros cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (2 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 2. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
have cf_comp_cf_const_r_\<KK>_def:
      "cf_const (cat_1 \<aa> \<ff>) \<AA> r' \<circ>\<^sub>C\<^sub>F \<KK> = cf_const \<BB> \<AA> r'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = dghm_const \<BB> \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>)
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: cat_cs_simps \<KK>_def
            cs_intro: cat_cs_intros cat_lim_cs_intros
        )
[PROOF STATE]
proof (state)
this:
dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = dghm_const \<BB> \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>)

goal (2 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 2. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
from \<epsilon>.cat_rKe_unique[
        OF const_r', unfolded cf_comp_cf_const_r_\<KK>_def, OF u'.is_ntcf_axioms
        ]
[PROOF STATE]
proof (chain)
picking this:
\<exists>!\<sigma>. \<sigma> : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
obtain \<sigma>
      where \<sigma>: "\<sigma> : cf_const (cat_1 \<aa> \<ff>) \<AA> r' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
        and u'_def: "u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)"
        and unique_\<sigma>: "\<And>\<sigma>'.
          \<lbrakk>
            \<sigma>' : cf_const (cat_1 \<aa> \<ff>) \<AA> r' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>;
            u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)
          \<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<exists>!\<sigma>. \<sigma> : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (1 subgoal):
 1. (\<And>\<sigma>. \<lbrakk>\<sigma> : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>); \<And>\<sigma>'. \<lbrakk>\<sigma>' : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
\<lbrakk>?\<sigma>' : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (?\<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)\<rbrakk> \<Longrightarrow> ?\<sigma>' = \<sigma>

goal (2 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 2. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
interpret \<sigma>: is_ntcf \<alpha> \<open>cat_1 \<aa> \<ff>\<close> \<AA> \<open>cf_const (cat_1 \<aa> \<ff>) \<AA> r'\<close> \<GG> \<sigma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule \<sigma>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 2. \<And>u' r'. u' : r' <\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>n\<^sub>e \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<Longrightarrow> \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
show "\<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'
[PROOF STEP]
proof(intro ex1I conjI; (elim conjE)?)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?a1 : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
 2. u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> ?a1
 3. \<And>f'. \<lbrakk>f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'\<rbrakk> \<Longrightarrow> f' = ?a1
[PROOF STEP]
fix f'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?a1 : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
 2. u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> ?a1
 3. \<And>f'. \<lbrakk>f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'\<rbrakk> \<Longrightarrow> f' = ?a1
[PROOF STEP]
assume prems':
        "f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>" "u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'"
[PROOF STATE]
proof (state)
this:
f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'

goal (3 subgoals):
 1. ?a1 : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
 2. u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> ?a1
 3. \<And>f'. \<lbrakk>f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'\<rbrakk> \<Longrightarrow> f' = ?a1
[PROOF STEP]
from prems'(1)
[PROOF STATE]
proof (chain)
picking this:
f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
[PROOF STEP]
have "ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' :
        cf_const (cat_1 \<aa> \<ff>) \<AA> r' \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>

goal (1 subgoal):
 1. ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (subst \<GG>_def)
          (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (3 subgoals):
 1. ?a1 : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
 2. u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> ?a1
 3. \<And>f'. \<lbrakk>f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'\<rbrakk> \<Longrightarrow> f' = ?a1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (3 subgoals):
 1. ?a1 : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
 2. u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> ?a1
 3. \<And>f'. \<lbrakk>f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'\<rbrakk> \<Longrightarrow> f' = ?a1
[PROOF STEP]
with prems'(1)
[PROOF STATE]
proof (chain)
picking this:
f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have "u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)"
[PROOF STATE]
proof (prove)
using this:
f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
by
          (
            cs_concl
              cs_simp: cat_cs_simps prems'(2) \<KK>_def cs_intro: cat_cs_intros
          )
[PROOF STATE]
proof (state)
this:
u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (3 subgoals):
 1. ?a1 : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
 2. u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> ?a1
 3. \<And>f'. \<lbrakk>f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'\<rbrakk> \<Longrightarrow> f' = ?a1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
have \<sigma>_def: "\<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'"
[PROOF STATE]
proof (prove)
using this:
ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' : dghm_const (cat_1 \<aa> \<ff>) \<AA> r' (\<AA>\<lparr>CId\<rparr>\<lparr>r'\<rparr>) \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_1 \<aa> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_const (cat_1 \<aa> \<ff>) \<AA> f' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (1 subgoal):
 1. \<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'
[PROOF STEP]
by (auto simp: unique_\<sigma>[symmetric])
[PROOF STATE]
proof (state)
this:
\<sigma> = ntcf_const (cat_1 \<aa> \<ff>) \<AA> f'

goal (3 subgoals):
 1. ?a1 : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
 2. u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> ?a1
 3. \<And>f'. \<lbrakk>f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>; u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'\<rbrakk> \<Longrightarrow> f' = ?a1
[PROOF STEP]
show "f' = \<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' = \<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps \<sigma>_def cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
f' = \<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>

goal (2 subgoals):
 1. \<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr> : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr>
 2. u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> (\<sigma>\<lparr>NTMap\<rparr>\<lparr>\<aa>\<rparr>)
[PROOF STEP]
qed (cs_concl cs_simp: cat_cs_simps u'_def \<KK>_def cs_intro: cat_cs_intros)+
[PROOF STATE]
proof (state)
this:
\<exists>!f'. f' : r' \<mapsto>\<^bsub>\<AA>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<and> u' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_const \<BB> \<AA> f'

goal (1 subgoal):
 1. \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (cs_concl cs_simp: \<KK>_def cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<epsilon> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> <\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>i\<^sub>m \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cat_lKe_is_cat_colimit:
  assumes "\<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>"
    and "\<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "\<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret \<eta>: is_cat_lKe \<alpha> \<BB> \<open>cat_1 \<aa> \<ff>\<close> \<AA> \<KK> \<TT> \<FF> \<eta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>l\<^sub>K\<^sub>e\<^bsub>\<alpha>\<^esub> \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<^sub>C cat_1 \<aa> \<ff> \<mapsto>\<^sub>C \<AA>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
from cat_1_components(1)
[PROOF STATE]
proof (chain)
picking this:
cat_1 ?\<aa> ?\<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {?\<aa>}
[PROOF STEP]
have \<aa>: "\<aa> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
cat_1 ?\<aa> ?\<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {?\<aa>}

goal (1 subgoal):
 1. \<aa> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: \<eta>.AG.HomCod.cat_in_Obj_in_Vset)
[PROOF STATE]
proof (state)
this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
from cat_1_components(2)
[PROOF STATE]
proof (chain)
picking this:
cat_1 ?\<aa> ?\<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {?\<ff>}
[PROOF STEP]
have \<ff>: "\<ff> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
cat_1 ?\<aa> ?\<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {?\<ff>}

goal (1 subgoal):
 1. \<ff> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: \<eta>.AG.HomCod.cat_in_Arr_in_Vset)
[PROOF STATE]
proof (state)
this:
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
      (
        rule is_cat_limit.is_cat_colimit_op
          [
            OF cat_rKe_is_cat_limit[
              OF
                \<eta>.is_cat_rKe_op[unfolded \<eta>.AG.cat_1_op[OF \<aa> \<ff>]]
                \<eta>.ntcf_lKe.NTDom.is_functor_op
              ],
            unfolded cat_op_simps
          ]
      )
[PROOF STATE]
proof (state)
this:
\<eta> : \<TT> >\<^sub>C\<^sub>F\<^sub>.\<^sub>c\<^sub>o\<^sub>l\<^sub>i\<^sub>m \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<aa>\<rparr> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed