Let x0 of type ο be given.

Assume H0: ∀ x1 : ι → ι . (∃ x2 : ι → ι → ι → ι . ∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) struct_u UnaryFuncHom struct_id struct_comp x1 x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) ⟶ x0.

Apply H0 with λ x1 . pack_u (setprod omega x1) (λ x2 . lam 2 (λ x3 . If_i (x3 = 0) (ordsucc (ap x2 0)) (ap x2 1))).

Let x1 of type ο be given.

Assume H1: ∀ x2 : ι → ι → ι → ι . (∃ x3 x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) struct_u UnaryFuncHom struct_id struct_comp (λ x5 . pack_u (setprod omega x5) (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (ordsucc (ap x6 0)) (ap x6 1)))) x2 (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) ⟶ x1.

Apply H1 with λ x2 x3 x4 . lam (setprod omega x2) (λ x5 . lam 2 (λ x6 . If_i (x6 = 0) (ap x5 0) (ap x4 (ap x5 1)))).

Let x2 of type ο be given.

Assume H2: ∀ x3 : ι → ι . (∃ x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) struct_u UnaryFuncHom struct_id struct_comp (λ x5 . pack_u (setprod omega x5) (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (ordsucc (ap x6 0)) (ap x6 1)))) (λ x5 x6 x7 . lam (setprod omega x5) (λ x8 . lam 2 (λ x9 . If_i (x9 = 0) (ap x8 0) (ap x7 (ap x8 1))))) (λ x5 . ap x5 0) (λ x5 x6 x7 . x7) x3 x4) ⟶ x2.

Apply H2 with λ x3 . lam x3 (λ x4 . lam 2 (λ x5 . If_i (x5 = 0) 0 x4)).

Let x3 of type ο be given.

Assume H3: ∀ x4 : ι → ι . MetaAdjunction_strict (λ x5 . True) HomSet (λ x5 . lam_id x5) (λ x5 x6 x7 x8 x9 . lam_comp x5 x8 x9) struct_u UnaryFuncHom struct_id struct_comp (λ x5 . pack_u (setprod omega x5) (λ x6 . lam 2 (λ x7 . If_i (x7 = 0) (ordsucc (ap x6 0)) (ap x6 1)))) (λ x5 x6 x7 . lam (setprod omega x5) (λ x8 . lam 2 (λ x9 . If_i (x9 = 0) (ap ... 0) ...))) ... ... ... ... ⟶ x3.

...

■

Proofgold Proof