[STATEMENT]
lemma Ya_ide:
    assumes a': "C.ide a'"
    shows "Y a a' = S.mkIde (Hom.set (a', a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Y a a' = S.mkIde (Hom.set (a', a))
[PROOF STEP]
using assms ide_apex Y.Y_simp Hom.map_ide
[PROOF STATE]
proof (prove)
using this:
C.ide a'
C.ide a
C.arr ?f \<Longrightarrow> Y ?f = (\<lambda>g. Hom.map (g, ?f))
\<lbrakk>C.ide ?b; C.ide ?a\<rbrakk> \<Longrightarrow> Hom.map (?b, ?a) = S.mkIde (Hom.set (?b, ?a))

goal (1 subgoal):
 1. Y a a' = S.mkIde (Hom.set (a', a))
[PROOF STEP]
by simp