Assume HF.
Apply MetaFunctorE Obj Hom id comp Obj' Hom' id' comp' F0 F1 HF to the current goal.
Assume HF1 HF2 HF3 HF4.
Assume HG.
Apply MetaFunctorE Obj' Hom' id' comp' Obj Hom id comp G0 G1 HG to the current goal.
Assume HG1 HG2 HG3 HG4.
Assume Heta.
Apply MetaNatTransE 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 Heta to the current goal.
Assume Heta1 Heta2.
Assume Heps.
Apply MetaNatTransE Obj' Hom' id' comp' Obj' Hom' id' comp' (λY ⇒ F0 (G0 Y)) (λX Y g ⇒ F1 (G0 X) (G0 Y) (G1 X Y g)) (λY ⇒ Y) (λX Y g ⇒ g) eps Heps to the current goal.
Assume Heps1: ∀X, Obj' X → Hom' (F0 (G0 X)) X (eps X).
Assume Heps2: ∀X Y f, Obj' X → Obj' Y → Hom' X Y f → comp' (F0 (G0 X)) X Y f (eps X) = comp' (F0 (G0 X)) (F0 (G0 Y)) Y (eps Y) (F1 (G0 X) (G0 Y) (G1 X Y f)).
Assume HA.
Apply MetaAdjunctionE HA to the current goal.
Assume HA1 HA2.
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.
Apply MetaFunctorE Obj Hom id comp Obj Hom id comp T0 T1 LT to the current goal.
Assume HT01 HT02 HT03 HT04.
Apply MetaMonadI to the current goal.
We will prove ∀X, Obj X → comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X)).
Let X be given.
Assume HX.
We prove the intermediate claim LFX: Obj' (F0 X).
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
We prove the intermediate claim LTX: Obj (T0 X).
An exact proof term for the current goal is HT01 X HX.
We prove the intermediate claim LFTX: Obj' (F0 (T0 X)).
Apply HF1 to the current goal.
An exact proof term for the current goal is LTX.
We prove the intermediate claim LTTX: Obj (T0 (T0 X)).
An exact proof term for the current goal is HT01 (T0 X) LTX.
We prove the intermediate claim LFTTX: Obj' (F0 (T0 (T0 X))).
Apply HF1 to the current goal.
An exact proof term for the current goal is LTTX.
We prove the intermediate claim LepsFX: Hom' (F0 (T0 X)) (F0 X) (eps (F0 X)).
An exact proof term for the current goal is Heps1 (F0 X) LFX.
We prove the intermediate claim LmuX: Hom (T0 (T0 X)) (T0 X) (mu X).
An exact proof term for the current goal is HG2 (F0 (T0 X)) (F0 X) (eps (F0 X)) LFTX LFX LepsFX.
We prove the intermediate claim LFmuX: Hom' (F0 (T0 (T0 X))) (F0 (T0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X)).
An exact proof term for the current goal is HF2 (T0 (T0 X)) (T0 X) (mu X) LTTX LTX LmuX.
We will prove comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X)).
Use transitivity with G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X))), and G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (eps (F0 (T0 X)))).
We will prove comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (T1 (T0 (T0 X)) (T0 X) (mu X)) = G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X))).
Use symmetry.
An exact proof term for the current goal is HG4 (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (F1 (T0 (T0 X)) (T0 X) (mu X)) (eps (F0 X)) LFTTX LFTX LFX LFmuX LepsFX.
We will prove G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X))) = G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (eps (F0 (T0 X)))).
Use f_equal.
Use symmetry.
We will prove comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (eps (F0 (T0 X))) = comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 (T0 (T0 X)) (T0 X) (mu X)).
An exact proof term for the current goal is Heps2 (F0 (T0 X)) (F0 X) (eps (F0 X)) LFTX LFX LepsFX.
We will prove G1 (F0 (T0 (T0 X))) (F0 X) (comp' (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 X)) (eps (F0 (T0 X)))) = comp (T0 (T0 (T0 X))) (T0 (T0 X)) (T0 X) (mu X) (mu (T0 X)).
An exact proof term for the current goal is HG4 (F0 (T0 (T0 X))) (F0 (T0 X)) (F0 X) (eps (F0 (T0 X))) (eps (F0 X)) LFTTX LFTX LFX (Heps1 (F0 (T0 X)) LFTX) LepsFX.
We will prove ∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (eta (T0 X)) = id (T0 X).
Let X be given.
Assume HX.
We will prove comp (G0 (F0 X)) (G0 (F0 (G0 (F0 X)))) (G0 (F0 X)) (G1 (F0 (G0 (F0 X))) (F0 X) (eps (F0 X))) (eta (G0 (F0 X))) = id (G0 (F0 X)).
An exact proof term for the current goal is HA2 (F0 X) (HF1 X HX).
We will prove ∀X, Obj X → comp (T0 X) (T0 (T0 X)) (T0 X) (mu X) (T1 X (T0 X) (eta X)) = id (T0 X).
Let X be given.
Assume HX.
We will prove comp (G0 (F0 X)) (G0 (F0 (T0 X))) (G0 (F0 X)) (G1 (F0 (T0 X)) (F0 X) (eps (F0 X))) (G1 (F0 X) (F0 (T0 X)) (F1 X (T0 X) (eta X))) = id (T0 X).
We prove the intermediate claim LFX: Obj' (F0 X).
Apply HF1 to the current goal.
An exact proof term for the current goal is HX.
We prove the intermediate claim LTX: Obj (T0 X).
An exact proof term for the current goal is HT01 X HX.
We prove the intermediate claim LFTX: Obj' (F0 (T0 X)).
Apply HF1 to the current goal.
An exact proof term for the current goal is LTX.
Use transitivity with G1 (F0 X) (F0 X) (comp' (F0 X) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 X (T0 X) (eta X))), and G1 (F0 X) (F0 X) (id' (F0 X)).
We will prove comp (G0 (F0 X)) (G0 (F0 (T0 X))) (G0 (F0 X)) (G1 (F0 (T0 X)) (F0 X) (eps (F0 X))) (G1 (F0 X) (F0 (T0 X)) (F1 X (T0 X) (eta X))) = G1 (F0 X) (F0 X) (comp' (F0 X) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 X (T0 X) (eta X))).
Use symmetry.
Apply HG4 (F0 X) (F0 (T0 X)) (F0 X) (F1 X (T0 X) (eta X)) (eps (F0 X)) to the current goal.
An exact proof term for the current goal is LFX.
An exact proof term for the current goal is LFTX.
An exact proof term for the current goal is LFX.
We will prove Hom' (F0 X) (F0 (T0 X)) (F1 X (T0 X) (eta X)).
An exact proof term for the current goal is HF2 X (T0 X) (eta X) HX LTX (Heta1 X HX).
We will prove Hom' (F0 (G0 (F0 X))) (F0 X) (eps (F0 X)).
An exact proof term for the current goal is Heps1 (F0 X) (HF1 X HX).
We will prove G1 (F0 X) (F0 X) (comp' (F0 X) (F0 (T0 X)) (F0 X) (eps (F0 X)) (F1 X (T0 X) (eta X))) = G1 (F0 X) (F0 X) (id' (F0 X)).
Use f_equal.
An exact proof term for the current goal is HA1 X HX.
We will prove G1 (F0 X) (F0 X) (id' (F0 X)) = id (T0 X).
An exact proof term for the current goal is HG3 (F0 X) LFX.
∎