Assume HA.
Apply MetaAdjunction_strict_E HA to the current goal.
Assume HA1 HG Heta Heps HA5.
Apply MetaFunctor_strict_E Obj Hom id comp Obj' Hom' id' comp' F0 F1 HA1 to the current goal.
Assume HC HC' HF.
Set T0 to be the term λX ⇒ G0 (F0 X) of type set → set.
Set T1 to be the term λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f) of type set → set → set → set.
Set mu to be the term λX ⇒ G1 (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)) of type set → set.
We prove the intermediate claim LT: MetaFunctor Obj Hom id comp Obj Hom id comp T0 T1.
An exact proof term for the current goal is MetaCat_CompFunctors Obj Hom id comp Obj' Hom' id' comp' Obj Hom id comp F0 F1 G0 G1 HF HG.
We prove the intermediate claim LTT: MetaFunctor Obj Hom id comp Obj Hom id comp (λX ⇒ T0 (T0 X)) (λX Y f ⇒ T1 (T0 X) (T0 Y) (T1 X Y f)).
An exact proof term for the current goal is MetaCat_CompFunctors Obj Hom id comp Obj Hom id comp Obj Hom id comp T0 T1 T0 T1 LT LT.
We prove the intermediate claim LFT: MetaFunctor Obj Hom id comp Obj' Hom' id' comp' (λX ⇒ F0 (T0 X)) (λX Y f ⇒ F1 (T0 X) (T0 Y) (T1 X Y f)).
An exact proof term for the current goal is MetaCat_CompFunctors Obj Hom id comp Obj Hom id comp Obj' Hom' id' comp' T0 T1 F0 F1 LT HF.
We prove the intermediate claim LepsF: MetaNatTrans Obj Hom id comp Obj' Hom' id' comp' (λX ⇒ F0 (G0 (F0 X))) (λX Y f ⇒ F1 (G0 (F0 X)) (G0 (F0 Y)) (G1 (F0 X) (F0 Y) (F1 X Y f))) F0 F1 (λX ⇒ eps (F0 X)).
An exact proof term for the current goal is MetaCat_CompNatTransFunctor Obj Hom id comp Obj' Hom' id' comp' Obj' Hom' id' comp' (λX ⇒ F0 (G0 X)) (λX Y f ⇒ F1 (G0 X) (G0 Y) (G1 X Y f)) (λX ⇒ X) (λX Y f ⇒ f) F0 F1 eps Heps HF.
We prove the intermediate claim Lmu: MetaNatTrans Obj Hom id comp Obj Hom id comp (λY ⇒ T0 (T0 Y)) (λX Y g ⇒ T1 (T0 X) (T0 Y) (T1 X Y g)) T0 T1 mu.
An exact proof term for the current goal is MetaCat_CompFunctorNatTrans Obj Hom id comp Obj' Hom' id' comp' Obj Hom id comp (λX ⇒ F0 (G0 (F0 X))) (λX Y f ⇒ F1 (G0 (F0 X)) (G0 (F0 Y)) (G1 (F0 X) (F0 Y) (F1 X Y f))) F0 F1 G0 G1 (λX ⇒ eps (F0 X)) LFT HF LepsF HG.
Apply MetaMonad_strict_I to the current goal.
Apply MetaNatTrans_strict_I to the current goal.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is MetaCat_IdFunctor Obj Hom id comp.
An exact proof term for the current goal is LT.
We will prove MetaNatTrans Obj Hom id comp Obj Hom id comp (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ G0 (F0 X)) (λX Y f ⇒ G1 (F0 X) (F0 Y) (F1 X Y f)) eta.
An exact proof term for the current goal is Heta.
Apply MetaNatTrans_strict_I to the current goal.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is HC.
An exact proof term for the current goal is LTT.
An exact proof term for the current goal is LT.
We will prove MetaNatTrans Obj Hom id comp Obj Hom id comp (λY ⇒ T0 (T0 Y)) (λX Y g ⇒ T1 (T0 X) (T0 Y) (T1 X Y g)) T0 T1 mu.
An exact proof term for the current goal is Lmu.
An exact proof term for the current goal is MetaAdjunctionMonad HF HG Heta Heps HA5.
∎