Assume H.
Apply H to the current goal.
Let F0 be given.
Assume H.
Apply H to the current goal.
Let F1 be given.
Assume H.
Apply H to the current goal.
Let eta be given.
Assume H.
Apply H to the current goal.
Let eps be given.
Assume H1: MetaAdjunction_strict (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_b_monoid Hom_struct_b struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps.
Apply MetaCatSet_initial to the current goal.
Let Init be given.
Assume H.
Apply H to the current goal.
Let uniq be given.
Assume H2: initial_p (λ_ ⇒ True) HomSet (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) Init uniq.
Apply MetaCat_struct_b_monoid_initial_neg to the current goal.
We use F0 Init to witness the existential quantifier.
An exact proof term for the current goal is LeftAdjointsPreserveInitial (λ_ ⇒ True) HomSet (λX ⇒ (λx ∈ X ⇒ x)) (λX Y Z f g ⇒ (λx ∈ X ⇒ f (g x))) struct_b_monoid Hom_struct_b struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps H1 Init uniq H2.
∎