[STATEMENT]
lemma is_cat_lKeI':
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<And>\<FF>' \<eta>'.
      \<lbrakk> \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' : \<TT> \<mapsto>\<^sub>C\<^sub>F \<FF>' \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<rbrakk> \<Longrightarrow>
        \<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
  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 \<AA>"
[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 \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
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 \<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. \<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 \<AA>
[PROOF STEP]
interpret \<FF>: is_functor \<alpha> \<CC> \<AA> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
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 \<AA>
[PROOF STEP]
interpret \<eta>: is_ntcf \<alpha> \<BB> \<AA> \<TT> \<open>\<FF> \<circ>\<^sub>C\<^sub>F \<KK>\<close> \<eta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
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 \<AA>
[PROOF STEP]
have
    "\<exists>!\<sigma>.
      \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and>
      \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F op_cf \<KK>)"
    if "\<GG>' : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>"
      and "\<eta>' : \<GG>' \<circ>\<^sub>C\<^sub>F op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>"
    for \<GG>' \<eta>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
interpret \<GG>': is_functor \<alpha> \<open>op_cat \<CC>\<close> \<open>op_cat \<AA>\<close> \<GG>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG>' : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
by (rule that(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
interpret \<eta>':
      is_ntcf \<alpha> \<open>op_cat \<BB>\<close> \<open>op_cat \<AA>\<close> \<open>\<GG>' \<circ>\<^sub>C\<^sub>F op_cf \<KK>\<close> \<open>op_cf \<TT>\<close> \<eta>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
by (rule that(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
from assms(4)[
        OF is_functor.is_functor_op[OF that(1), unfolded cat_op_simps],
        OF is_ntcf.is_ntcf_op[OF that(2), unfolded cat_op_simps]
        ]
[PROOF STATE]
proof (chain)
picking this:
\<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> op_ntcf \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
obtain \<sigma> where \<sigma>: "\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
      and op_\<eta>'_def: "op_ntcf \<eta>' = \<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
      and unique_\<sigma>':
        "\<lbrakk>
          \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>;
          op_ntcf \<eta>' = \<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>
         \<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>"
      for \<sigma>'
[PROOF STATE]
proof (prove)
using this:
\<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> op_ntcf \<eta>' = \<sigma> \<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 \<eta>

goal (1 subgoal):
 1. (\<And>\<sigma>. \<lbrakk>\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; op_ntcf \<eta>' = \<sigma> \<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 \<eta>; \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; op_ntcf \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
op_ntcf \<eta>' = \<sigma> \<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 \<eta>
\<lbrakk>?\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; op_ntcf \<eta>' = ?\<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> ?\<sigma>' = \<sigma>

goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
interpret \<sigma>: is_ntcf \<alpha> \<CC> \<AA> \<FF> \<open>op_cf \<GG>'\<close> \<sigma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule \<sigma>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
proof(intro ex1I conjI; (elim conjE)?)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?a1 : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
 2. \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (?a1 \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)
 3. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma> = ?a1
[PROOF STEP]
show "op_ntcf \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
by (rule \<sigma>.is_ntcf_op[unfolded cat_op_simps])
[PROOF STATE]
proof (state)
this:
op_ntcf \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>

goal (2 subgoals):
 1. \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)
 2. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
from op_\<eta>'_def
[PROOF STATE]
proof (chain)
picking this:
op_ntcf \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
have "op_ntcf (op_ntcf \<eta>') = op_ntcf (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>)"
[PROOF STATE]
proof (prove)
using this:
op_ntcf \<eta>' = \<sigma> \<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 \<eta>

goal (1 subgoal):
 1. op_ntcf (op_ntcf \<eta>') = op_ntcf (\<sigma> \<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 \<eta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
op_ntcf (op_ntcf \<eta>') = op_ntcf (\<sigma> \<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 \<eta>)

goal (2 subgoals):
 1. \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)
 2. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
from this \<sigma> assms(1-3)
[PROOF STATE]
proof (chain)
picking this:
op_ntcf (op_ntcf \<eta>') = op_ntcf (\<sigma> \<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 \<eta>)
\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show \<eta>'_def:
        "\<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (op_ntcf \<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F op_cf \<KK>)"
[PROOF STATE]
proof (prove)
using this:
op_ntcf (op_ntcf \<eta>') = op_ntcf (\<sigma> \<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 \<eta>)
\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F op_cf \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<eta> : \<TT> \<mapsto>\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)
[PROOF STEP]
by (cs_prems cs_shallow cs_simp: cat_op_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
fix \<sigma>'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
assume prems:
        "\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>"
        "\<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F op_cf \<KK>)"
[PROOF STATE]
proof (state)
this:
\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
\<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
interpret \<sigma>': is_ntcf \<alpha> \<open>op_cat \<CC>\<close> \<open>op_cat \<AA>\<close> \<GG>' \<open>op_cf \<FF>\<close> \<sigma>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
from prems(2)
[PROOF STATE]
proof (chain)
picking this:
\<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
have
        "op_ntcf \<eta>' = op_ntcf (op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F op_cf \<KK>))"
[PROOF STATE]
proof (prove)
using this:
\<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)

goal (1 subgoal):
 1. op_ntcf \<eta>' = op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
op_ntcf \<eta>' = op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>))

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
op_ntcf \<eta>' = op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>))

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
have "\<dots> = op_ntcf \<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>)) = op_ntcf \<sigma>' \<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 \<eta>
[PROOF STEP]
by
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_op_simps
              cs_intro: cat_cs_intros cat_op_intros
          )
[PROOF STATE]
proof (state)
this:
op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>)) = op_ntcf \<sigma>' \<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 \<eta>

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
op_ntcf \<eta>' = op_ntcf \<sigma>' \<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 \<eta>
[PROOF STEP]
have "op_ntcf \<eta>' = op_ntcf \<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (prove)
using this:
op_ntcf \<eta>' = op_ntcf \<sigma>' \<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 \<eta>

goal (1 subgoal):
 1. op_ntcf \<eta>' = op_ntcf \<sigma>' \<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 \<eta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
op_ntcf \<eta>' = op_ntcf \<sigma>' \<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 \<eta>

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
from unique_\<sigma>'[OF \<sigma>'.is_ntcf_op[unfolded cat_op_simps] this]
[PROOF STATE]
proof (chain)
picking this:
op_ntcf \<sigma>' = \<sigma>
[PROOF STEP]
show
        "\<sigma>' = op_ntcf \<sigma>"
[PROOF STATE]
proof (prove)
using this:
op_ntcf \<sigma>' = \<sigma>

goal (1 subgoal):
 1. \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
by (auto simp: cat_op_simps)
[PROOF STATE]
proof (state)
this:
\<sigma>' = op_ntcf \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?\<GG>' : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; ?\<eta>' : ?\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>\<rbrakk> \<Longrightarrow> \<exists>!\<sigma>. \<sigma> : ?\<GG>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> ?\<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)

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 \<AA>
[PROOF STEP]
from
    is_cat_rKeI'
      [
        OF \<KK>.is_functor_op \<FF>.is_functor_op \<eta>.is_ntcf_op[unfolded cat_op_simps],
        unfolded cat_op_simps,
        OF this
      ]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>\<rbrakk> \<Longrightarrow> \<GG>' : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>\<rbrakk> \<Longrightarrow> \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>\<rbrakk> \<Longrightarrow> 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>
[PROOF STEP]
interpret \<eta>: is_cat_rKe
    \<alpha>
    \<open>op_cat \<BB>\<close>
    \<open>op_cat \<CC>\<close>
    \<open>op_cat \<AA>\<close>
    \<open>op_cf \<KK>\<close>
    \<open>op_cf \<TT>\<close>
    \<open>op_cf \<FF>\<close>
    \<open>op_ntcf \<eta>\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>\<rbrakk> \<Longrightarrow> \<GG>' : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<And>\<GG>' \<epsilon>'. \<lbrakk>\<GG>' : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>\<rbrakk> \<Longrightarrow> \<epsilon>' : \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK> \<mapsto>\<^sub>C\<^sub>F op_cf \<TT> : op_cat \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>\<rbrakk> \<Longrightarrow> 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>

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_cat \<AA>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
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 \<AA>
[PROOF STEP]
show "\<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 \<AA>"
[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 \<AA>
[PROOF STEP]
by (rule \<eta>.is_cat_lKe_op[unfolded cat_op_simps])
[PROOF STATE]
proof (state)
this:
\<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 \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_cat_rKe) cat_rKe_unique:
  assumes "\<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>" and "\<epsilon>' : \<GG>' \<circ>\<^sub>C\<^sub>F \<KK> \<mapsto>\<^sub>C\<^sub>F \<TT> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "\<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
interpret \<GG>': is_functor \<alpha> \<CC> \<AA> \<GG>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
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 (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
let ?\<TT> = \<open>cf_map \<TT>\<close>
    and ?\<GG> = \<open>cf_map \<GG>\<close>
    and ?\<GG>' = \<open>cf_map \<GG>'\<close>
    and ?\<epsilon> = \<open>ntcf_arrow \<epsilon>\<close>
    and ?\<epsilon>' = \<open>ntcf_arrow \<epsilon>'\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
define \<beta> where "\<beta> = \<alpha> + \<omega>"
[PROOF STATE]
proof (state)
this:
\<beta> = \<alpha> + \<omega>

goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
have "\<Z> \<beta>" and \<alpha>\<beta>: "\<alpha> \<in>\<^sub>\<circ> \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta> &&& \<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
by (simp_all add: \<beta>_def AG.\<Z>_Limit_\<alpha>\<omega> AG.\<Z>_\<omega>_\<alpha>\<omega> \<Z>_def AG.\<Z>_\<alpha>_\<alpha>\<omega>)
[PROOF STATE]
proof (state)
this:
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
then
[PROOF STATE]
proof (chain)
picking this:
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
using this:
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
interpret \<AA>\<KK>: is_tiny_functor
    \<beta> \<open>cat_FUNCT \<alpha> \<CC> \<AA>\<close> \<open>cat_FUNCT \<alpha> \<BB> \<AA>\<close> \<open>exp_cat_cf \<alpha> \<AA> \<KK>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp_cat_cf \<alpha> \<AA> \<KK> : cat_FUNCT \<alpha> \<CC> \<AA> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \<BB> \<AA>
[PROOF STEP]
by (rule cat_rKe_exp_cat_cf_cat_FUNCT_is_arr[OF \<beta>.\<Z>_axioms \<alpha>\<beta>])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
\<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have \<GG>': "?\<GG>' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<GG>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. cf_map \<GG>' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: cat_FUNCT_components(1) cs_intro: cat_FUNCT_cs_intros
      )
[PROOF STATE]
proof (state)
this:
cf_map \<GG>' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<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>
cf_map \<GG>' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
have
    "?\<epsilon>' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>?\<GG>'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> ?\<TT>"
[PROOF STATE]
proof (prove)
using this:
\<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>
cf_map \<GG>' \<in>\<^sub>\<circ> cat_FUNCT \<alpha> \<CC> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. ntcf_arrow \<epsilon>' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: cat_Kan_cs_simps cat_FUNCT_cs_simps
          cs_intro: cat_cs_intros cat_FUNCT_cs_intros
      )
[PROOF STATE]
proof (state)
this:
ntcf_arrow \<epsilon>' : exp_cat_cf \<alpha> \<AA> \<KK>\<lparr>ObjMap\<rparr>\<lparr>cf_map \<GG>'\<rparr> \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<BB> \<AA>\<^esub> cf_map \<TT>

goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
from
    is_functor.universal_arrow_foD(3)[
      OF \<AA>\<KK>.is_functor_axioms cat_rKe_ua_fo \<GG>' this
      ]
[PROOF STATE]
proof (chain)
picking this:
\<exists>!f'. f' : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
[PROOF STEP]
obtain f' where f': "f' : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>"
    and \<epsilon>'_def: "?\<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) ?\<TT> ?\<GG> ?\<epsilon> ?\<GG>'\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>"
    and f'_unique:
      "\<lbrakk>
        f'' : ?\<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> ?\<GG>;
        ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) ?\<TT> ?\<GG> ?\<epsilon> ?\<GG>'\<lparr>ArrVal\<rparr>\<lparr>f''\<rparr>
       \<rbrakk> \<Longrightarrow> f'' = f'"
    for f''
[PROOF STATE]
proof (prove)
using this:
\<exists>!f'. f' : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG> \<and> ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>; \<And>f''. \<lbrakk>f'' : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>f''\<rparr>\<rbrakk> \<Longrightarrow> f'' = f'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f' : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>
ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
\<lbrakk>?f'' : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>; ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>?f''\<rparr>\<rbrakk> \<Longrightarrow> ?f'' = f'

goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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]
proof(intro ex1I conjI; (elim conjE)?)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?a1 : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 2. \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (?a1 \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
 3. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<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> = ?a1
[PROOF STEP]
from \<epsilon>'_def cat_FUNCT_is_arrD(1)[OF f']
[PROOF STATE]
proof (chain)
picking this:
ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
ntcf_of_ntcf_arrow \<CC> \<AA> f' : cf_of_cf_map \<CC> \<AA> (cf_map \<GG>') \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<CC> \<AA> (cf_map \<GG>) : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show
      "\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (ntcf_of_ntcf_arrow \<CC> \<AA> f' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>)"
[PROOF STATE]
proof (prove)
using this:
ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>f'\<rparr>
ntcf_of_ntcf_arrow \<CC> \<AA> f' : cf_of_cf_map \<CC> \<AA> (cf_map \<GG>') \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<CC> \<AA> (cf_map \<GG>) : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_of_ntcf_arrow \<CC> \<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 (subst (asm) cat_FUNCT_is_arrD(2)[OF f']) (*slow*)
        (
          cs_prems cs_shallow
            cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_Kan_cs_simps
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<epsilon>' = \<epsilon> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (ntcf_of_ntcf_arrow \<CC> \<AA> f' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal (2 subgoals):
 1. ntcf_of_ntcf_arrow \<CC> \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 2. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<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> = ntcf_of_ntcf_arrow \<CC> \<AA> f'
[PROOF STEP]
from cat_FUNCT_is_arrD(1)[OF f']
[PROOF STATE]
proof (chain)
picking this:
ntcf_of_ntcf_arrow \<CC> \<AA> f' : cf_of_cf_map \<CC> \<AA> (cf_map \<GG>') \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<CC> \<AA> (cf_map \<GG>) : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show f'_is_arr:
      "ntcf_of_ntcf_arrow \<CC> \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
ntcf_of_ntcf_arrow \<CC> \<AA> f' : cf_of_cf_map \<CC> \<AA> (cf_map \<GG>') \<mapsto>\<^sub>C\<^sub>F cf_of_cf_map \<CC> \<AA> (cf_map \<GG>) : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. ntcf_of_ntcf_arrow \<CC> \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by
        (
          cs_prems cs_shallow
            cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
ntcf_of_ntcf_arrow \<CC> \<AA> f' : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<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> = ntcf_of_ntcf_arrow \<CC> \<AA> f'
[PROOF STEP]
fix \<sigma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<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> = ntcf_of_ntcf_arrow \<CC> \<AA> f'
[PROOF STEP]
assume prems:
      "\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>" "\<epsilon>' = \<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>)"
[PROOF STATE]
proof (state)
this:
\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon>' = \<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> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<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> = ntcf_of_ntcf_arrow \<CC> \<AA> f'
[PROOF STEP]
interpret \<sigma>: is_ntcf \<alpha> \<CC> \<AA> \<GG>' \<GG> \<sigma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<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> = ntcf_of_ntcf_arrow \<CC> \<AA> f'
[PROOF STEP]
from prems(1)
[PROOF STATE]
proof (chain)
picking this:
\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have \<sigma>:
      "ntcf_arrow \<sigma> : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. ntcf_arrow \<sigma> : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_FUNCT_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_arrow \<sigma> : cf_map \<GG>' \<mapsto>\<^bsub>cat_FUNCT \<alpha> \<CC> \<AA>\<^esub> cf_map \<GG>

goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<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> = ntcf_of_ntcf_arrow \<CC> \<AA> f'
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon>' = \<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]
have \<epsilon>'_def: "ntcf_arrow \<epsilon>' =
      umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) ?\<TT> ?\<GG> ?\<epsilon> ?\<GG>'\<lparr>ArrVal\<rparr>\<lparr>ntcf_arrow \<sigma>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<epsilon>' = \<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. ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>ntcf_arrow \<sigma>\<rparr>
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: prems(2) cat_Kan_cs_simps cat_cs_simps cat_FUNCT_cs_simps
            cs_intro: cat_cs_intros cat_FUNCT_cs_intros
        )
[PROOF STATE]
proof (state)
this:
ntcf_arrow \<epsilon>' = umap_fo (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) (cf_map \<GG>')\<lparr>ArrVal\<rparr>\<lparr>ntcf_arrow \<sigma>\<rparr>

goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>\<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<epsilon>' = \<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> = ntcf_of_ntcf_arrow \<CC> \<AA> f'
[PROOF STEP]
show "\<sigma> = ntcf_of_ntcf_arrow \<CC> \<AA> f'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> = ntcf_of_ntcf_arrow \<CC> \<AA> f'
[PROOF STEP]
unfolding f'_unique[OF \<sigma> \<epsilon>'_def, symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> = ntcf_of_ntcf_arrow \<CC> \<AA> (ntcf_arrow \<sigma>)
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros
        )
[PROOF STATE]
proof (state)
this:
\<sigma> = ntcf_of_ntcf_arrow \<CC> \<AA> f'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!\<sigma>. \<sigma> : \<GG>' \<mapsto>\<^sub>C\<^sub>F \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<epsilon>' = \<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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_cat_lKe) cat_lKe_unique:
  assumes "\<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>" and "\<eta>' : \<TT> \<mapsto>\<^sub>C\<^sub>F \<FF>' \<circ>\<^sub>C\<^sub>F \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
  shows "\<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK>) \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
interpret \<FF>': is_functor \<alpha> \<CC> \<AA> \<FF>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
interpret \<eta>': is_ntcf \<alpha> \<BB> \<AA> \<TT> \<open>\<FF>' \<circ>\<^sub>C\<^sub>F \<KK>\<close> \<eta>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta>' : \<TT> \<mapsto>\<^sub>C\<^sub>F \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
interpret \<eta>: is_cat_rKe
    \<alpha> \<open>op_cat \<BB>\<close> \<open>op_cat \<CC>\<close> \<open>op_cat \<AA>\<close> \<open>op_cf \<KK>\<close> \<open>op_cf \<TT>\<close> \<open>op_cf \<FF>\<close> \<open>op_ntcf \<eta>\<close>
[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_cat \<AA>
[PROOF STEP]
by (rule is_cat_rKe_op)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
from \<eta>.cat_rKe_unique[OF \<FF>'.is_functor_op \<eta>'.is_ntcf_op[unfolded cat_op_simps]]
[PROOF STATE]
proof (chain)
picking this:
\<exists>!\<sigma>. \<sigma> : op_cf \<FF>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> op_ntcf \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
obtain \<sigma> where \<sigma>: "\<sigma> : op_cf \<FF>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>"
    and \<eta>'_def: "op_ntcf \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F op_cf \<KK>)"
    and unique_\<sigma>': "\<And>\<sigma>'.
      \<lbrakk>
        \<sigma>' : op_cf \<FF>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>;
        op_ntcf \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F op_cf \<KK>)
      \<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>"
[PROOF STATE]
proof (prove)
using this:
\<exists>!\<sigma>. \<sigma> : op_cf \<FF>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA> \<and> op_ntcf \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)

goal (1 subgoal):
 1. (\<And>\<sigma>. \<lbrakk>\<sigma> : op_cf \<FF>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; op_ntcf \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>); \<And>\<sigma>'. \<lbrakk>\<sigma>' : op_cf \<FF>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; op_ntcf \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> \<sigma>' = \<sigma>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<sigma> : op_cf \<FF>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
op_ntcf \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
\<lbrakk>?\<sigma>' : op_cf \<FF>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>; op_ntcf \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)\<rbrakk> \<Longrightarrow> ?\<sigma>' = \<sigma>

goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
interpret \<sigma>: is_ntcf \<alpha> \<open>op_cat \<CC>\<close> \<open>op_cat \<AA>\<close> \<open>op_cf \<FF>'\<close> \<open>op_cf \<FF>\<close> \<sigma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma> : op_cf \<FF>' \<mapsto>\<^sub>C\<^sub>F op_cf \<FF> : op_cat \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> op_cat \<AA>
[PROOF STEP]
by (rule \<sigma>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = \<sigma> \<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 \<eta>
[PROOF STEP]
proof(intro ex1I conjI; (elim conjE)?)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?a1 : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 2. \<eta>' = ?a1 \<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 \<eta>
 3. \<And>\<sigma>. \<lbrakk>\<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma> \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma> = ?a1
[PROOF STEP]
show "op_ntcf \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule \<sigma>.is_ntcf_op[unfolded cat_op_simps])
[PROOF STATE]
proof (state)
this:
op_ntcf \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (2 subgoals):
 1. \<eta>' = op_ntcf \<sigma> \<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 \<eta>
 2. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
have "\<eta>' = op_ntcf (op_ntcf \<eta>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<eta>' = op_ntcf (op_ntcf \<eta>')
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_op_simps)
[PROOF STATE]
proof (state)
this:
\<eta>' = op_ntcf (op_ntcf \<eta>')

goal (2 subgoals):
 1. \<eta>' = op_ntcf \<sigma> \<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 \<eta>
 2. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<eta>' = op_ntcf (op_ntcf \<eta>')

goal (2 subgoals):
 1. \<eta>' = op_ntcf \<sigma> \<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 \<eta>
 2. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
from \<eta>'_def
[PROOF STATE]
proof (chain)
picking this:
op_ntcf \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)
[PROOF STEP]
have "\<dots> = op_ntcf (op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (\<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F op_cf \<KK>))"
[PROOF STATE]
proof (prove)
using this:
op_ntcf \<eta>' = op_ntcf \<eta> \<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 op_cf \<KK>)

goal (1 subgoal):
 1. op_ntcf (op_ntcf \<eta>') = op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
op_ntcf (op_ntcf \<eta>') = op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>))

goal (2 subgoals):
 1. \<eta>' = op_ntcf \<sigma> \<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 \<eta>
 2. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
op_ntcf (op_ntcf \<eta>') = op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>))

goal (2 subgoals):
 1. \<eta>' = op_ntcf \<sigma> \<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 \<eta>
 2. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
have "\<dots> = op_ntcf \<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>)) = op_ntcf \<sigma> \<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 \<eta>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
op_ntcf (op_ntcf \<eta> \<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 op_cf \<KK>)) = op_ntcf \<sigma> \<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 \<eta>

goal (2 subgoals):
 1. \<eta>' = op_ntcf \<sigma> \<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 \<eta>
 2. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<eta>' = op_ntcf \<sigma> \<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 \<eta>
[PROOF STEP]
show "\<eta>' = op_ntcf \<sigma> \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (prove)
using this:
\<eta>' = op_ntcf \<sigma> \<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 \<eta>

goal (1 subgoal):
 1. \<eta>' = op_ntcf \<sigma> \<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 \<eta>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<eta>' = op_ntcf \<sigma> \<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 \<eta>

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
fix \<sigma>'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
assume prems:
      "\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
      "\<eta>' = \<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>"
[PROOF STATE]
proof (state)
this:
\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
\<eta>' = \<sigma>' \<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 \<eta>

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
interpret \<sigma>': is_ntcf \<alpha> \<CC> \<AA> \<FF> \<FF>' \<sigma>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
from prems(2)
[PROOF STATE]
proof (chain)
picking this:
\<eta>' = \<sigma>' \<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 \<eta>
[PROOF STEP]
have "op_ntcf \<eta>' = op_ntcf (\<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F \<KK> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<eta>)"
[PROOF STATE]
proof (prove)
using this:
\<eta>' = \<sigma>' \<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 \<eta>

goal (1 subgoal):
 1. op_ntcf \<eta>' = op_ntcf (\<sigma>' \<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 \<eta>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
op_ntcf \<eta>' = op_ntcf (\<sigma>' \<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 \<eta>)

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
op_ntcf \<eta>' = op_ntcf (\<sigma>' \<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 \<eta>)

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
have "\<dots> = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (op_ntcf \<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F op_cf \<KK>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf (\<sigma>' \<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 \<eta>) = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
op_ntcf (\<sigma>' \<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 \<eta>) = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
op_ntcf \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)
[PROOF STEP]
have "op_ntcf \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F (op_ntcf \<sigma>' \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F op_cf \<KK>)"
[PROOF STATE]
proof (prove)
using this:
op_ntcf \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)

goal (1 subgoal):
 1. op_ntcf \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
op_ntcf \<eta>' = op_ntcf \<eta> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (op_ntcf \<sigma>' \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<KK>)

goal (1 subgoal):
 1. \<And>\<sigma>'. \<lbrakk>\<sigma>' : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>; \<eta>' = \<sigma>' \<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 \<eta>\<rbrakk> \<Longrightarrow> \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
from unique_\<sigma>'[OF \<sigma>'.is_ntcf_op this]
[PROOF STATE]
proof (chain)
picking this:
op_ntcf \<sigma>' = \<sigma>
[PROOF STEP]
show "\<sigma>' = op_ntcf \<sigma>"
[PROOF STATE]
proof (prove)
using this:
op_ntcf \<sigma>' = \<sigma>

goal (1 subgoal):
 1. \<sigma>' = op_ntcf \<sigma>
[PROOF STEP]
by (auto simp: cat_op_simps)
[PROOF STATE]
proof (state)
this:
\<sigma>' = op_ntcf \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!\<sigma>. \<sigma> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<FF>' : \<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA> \<and> \<eta>' = \<sigma> \<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 \<eta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_cat_rKe) cat_rKe_ntcf_ua_fo_is_iso_ntcf_if_ge_Limit:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows
    "ntcf_ua_fo \<beta> (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) :
      Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<CC> \<AA>(-,cf_map \<GG>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o
      Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<BB> \<AA>(-,cf_map \<TT>) \<circ>\<^sub>C\<^sub>F op_cf (exp_cat_cf \<alpha> \<AA> \<KK>) :
      op_cat (cat_FUNCT \<alpha> \<CC> \<AA>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ua_fo \<beta> (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<CC> \<AA>(-,cf_map \<GG>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<BB> \<AA>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf (exp_cat_cf \<alpha> \<AA> \<KK>) : op_cat (cat_FUNCT \<alpha> \<CC> \<AA>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ntcf_ua_fo \<beta> (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<CC> \<AA>(-,cf_map \<GG>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<BB> \<AA>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf (exp_cat_cf \<alpha> \<AA> \<KK>) : op_cat (cat_FUNCT \<alpha> \<CC> \<AA>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
interpret \<AA>_\<KK>:
    is_tiny_functor \<beta> \<open>cat_FUNCT \<alpha> \<CC> \<AA>\<close> \<open>cat_FUNCT \<alpha> \<BB> \<AA>\<close> \<open>exp_cat_cf \<alpha> \<AA> \<KK>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp_cat_cf \<alpha> \<AA> \<KK> : cat_FUNCT \<alpha> \<CC> \<AA> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> \<BB> \<AA>
[PROOF STEP]
by
      (
        rule exp_cat_cf_is_tiny_functor[
          OF assms Ran.HomCod.category_axioms AG.is_functor_axioms
          ]
      )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ntcf_ua_fo \<beta> (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<CC> \<AA>(-,cf_map \<GG>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<BB> \<AA>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf (exp_cat_cf \<alpha> \<AA> \<KK>) : op_cat (cat_FUNCT \<alpha> \<CC> \<AA>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ua_fo \<beta> (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<CC> \<AA>(-,cf_map \<GG>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<BB> \<AA>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf (exp_cat_cf \<alpha> \<AA> \<KK>) : op_cat (cat_FUNCT \<alpha> \<CC> \<AA>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
by
      (
        rule is_functor.cf_ntcf_ua_fo_is_iso_ntcf[
          OF \<AA>_\<KK>.is_functor_axioms cat_rKe_ua_fo
          ]
      )
[PROOF STATE]
proof (state)
this:
ntcf_ua_fo \<beta> (exp_cat_cf \<alpha> \<AA> \<KK>) (cf_map \<TT>) (cf_map \<GG>) (ntcf_arrow \<epsilon>) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<CC> \<AA>(-,cf_map \<GG>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> \<BB> \<AA>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf (exp_cat_cf \<alpha> \<AA> \<KK>) : op_cat (cat_FUNCT \<alpha> \<CC> \<AA>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_cat_lKe) cat_lKe_ntcf_ua_fo_is_iso_ntcf_if_ge_Limit:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  defines "\<AA>\<KK> \<equiv> exp_cat_cf \<alpha> (op_cat \<AA>) (op_cf \<KK>)"
    and "\<AA>\<CC> \<equiv> cat_FUNCT \<alpha> (op_cat \<CC>) (op_cat \<AA>)"
    and "\<AA>\<BB> \<equiv> cat_FUNCT \<alpha> (op_cat \<BB>) (op_cat \<AA>)"
  shows
    "ntcf_ua_fo \<beta> \<AA>\<KK> (cf_map \<TT>) (cf_map \<FF>) (ntcf_arrow (op_ntcf \<eta>)) :
      Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<CC>(-,cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<BB>(-,cf_map \<TT>) \<circ>\<^sub>C\<^sub>F op_cf \<AA>\<KK> :
      op_cat \<AA>\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ua_fo \<beta> \<AA>\<KK> (cf_map \<TT>) (cf_map \<FF>) (ntcf_arrow (op_ntcf \<eta>)) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<CC>(-,cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<BB>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<AA>\<KK> : op_cat \<AA>\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ntcf_ua_fo \<beta> \<AA>\<KK> (cf_map \<TT>) (cf_map \<FF>) (ntcf_arrow (op_ntcf \<eta>)) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<CC>(-,cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<BB>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<AA>\<KK> : op_cat \<AA>\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
note simps = \<AA>\<CC>_def \<AA>\<BB>_def \<AA>\<KK>_def
[PROOF STATE]
proof (state)
this:
\<AA>\<CC> \<equiv> cat_FUNCT \<alpha> (op_cat \<CC>) (op_cat \<AA>)
\<AA>\<BB> \<equiv> cat_FUNCT \<alpha> (op_cat \<BB>) (op_cat \<AA>)
\<AA>\<KK> \<equiv> exp_cat_cf \<alpha> (op_cat \<AA>) (op_cf \<KK>)

goal (1 subgoal):
 1. ntcf_ua_fo \<beta> \<AA>\<KK> (cf_map \<TT>) (cf_map \<FF>) (ntcf_arrow (op_ntcf \<eta>)) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<CC>(-,cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<BB>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<AA>\<KK> : op_cat \<AA>\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
interpret \<AA>_\<KK>: is_tiny_functor \<beta> \<AA>\<CC> \<AA>\<BB> \<AA>\<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA>\<KK> : \<AA>\<CC> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<beta>\<^esub> \<AA>\<BB>
[PROOF STEP]
unfolding simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp_cat_cf \<alpha> (op_cat \<AA>) (op_cf \<KK>) : cat_FUNCT \<alpha> (op_cat \<CC>) (op_cat \<AA>) \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<beta>\<^esub> cat_FUNCT \<alpha> (op_cat \<BB>) (op_cat \<AA>)
[PROOF STEP]
by
      (
        rule exp_cat_cf_is_tiny_functor[
          OF assms(1,2) Lan.HomCod.category_op AG.is_functor_op
          ]
      )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ntcf_ua_fo \<beta> \<AA>\<KK> (cf_map \<TT>) (cf_map \<FF>) (ntcf_arrow (op_ntcf \<eta>)) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<CC>(-,cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<BB>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<AA>\<KK> : op_cat \<AA>\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ua_fo \<beta> \<AA>\<KK> (cf_map \<TT>) (cf_map \<FF>) (ntcf_arrow (op_ntcf \<eta>)) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<CC>(-,cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<BB>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<AA>\<KK> : op_cat \<AA>\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
unfolding simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ua_fo \<beta> (exp_cat_cf \<alpha> (op_cat \<AA>) (op_cf \<KK>)) (cf_map \<TT>) (cf_map \<FF>) (ntcf_arrow (op_ntcf \<eta>)) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> (op_cat \<CC>) (op_cat \<AA>)(-,cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>cat_FUNCT \<alpha> (op_cat \<BB>) (op_cat \<AA>)(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf (exp_cat_cf \<alpha> (op_cat \<AA>) (op_cf \<KK>)) : op_cat (cat_FUNCT \<alpha> (op_cat \<CC>) (op_cat \<AA>)) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>
[PROOF STEP]
by
      (
        rule is_functor.cf_ntcf_ua_fo_is_iso_ntcf[
          OF \<AA>_\<KK>.is_functor_axioms[unfolded simps] cat_lKe_ua_fo
          ]
      )
[PROOF STATE]
proof (state)
this:
ntcf_ua_fo \<beta> \<AA>\<KK> (cf_map \<TT>) (cf_map \<FF>) (ntcf_arrow (op_ntcf \<eta>)) : Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<CC>(-,cf_map \<FF>) \<mapsto>\<^sub>C\<^sub>F\<^sub>.\<^sub>i\<^sub>s\<^sub>o Hom\<^sub>O\<^sub>.\<^sub>C\<^bsub>\<beta>\<^esub>\<AA>\<BB>(-,cf_map \<TT>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_cf \<AA>\<KK> : op_cat \<AA>\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<beta>\<^esub> cat_Set \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma op_ua_components:
  shows [cat_op_simps]: "op_ua lim_Obj \<KK> c\<lparr>UObj\<rparr> = lim_Obj c\<lparr>UObj\<rparr>"
    and "op_ua lim_Obj \<KK> c\<lparr>UArr\<rparr> =
      op_ntcf (lim_Obj c\<lparr>UArr\<rparr>) \<circ>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^sub>-\<^sub>C\<^sub>F inv_cf (op_cf_obj_comma \<KK> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ua lim_Obj \<KK> c\<lparr>UObj\<rparr> = lim_Obj c\<lparr>UObj\<rparr> &&& op_ua lim_Obj \<KK> c\<lparr>UArr\<rparr> = op_ntcf (lim_Obj c\<lparr>UArr\<rparr>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c)
[PROOF STEP]
unfolding op_ua_def ua_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [lim_Obj c\<lparr>[]\<^sub>\<circ>\<rparr>, op_ntcf (lim_Obj c\<lparr>1\<^sub>\<nat>\<rparr>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = lim_Obj c\<lparr>[]\<^sub>\<circ>\<rparr> &&& [lim_Obj c\<lparr>[]\<^sub>\<circ>\<rparr>, op_ntcf (lim_Obj c\<lparr>1\<^sub>\<nat>\<rparr>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = op_ntcf (lim_Obj c\<lparr>1\<^sub>\<nat>\<rparr>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm (op_cf_obj_comma \<KK> c)
[PROOF STEP]
by (simp_all add: nat_omega_simps)