Set F0 to be the term λX ⇒ pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) of type set → set.
Set F1 to be the term λX Y h ⇒ λu ∈ int ⨯ X ⇒ (u 0,h (u 1)) of type set → set → set → set.
Set eta to be the term λX ⇒ λx ∈ X ⇒ (0,x) of type set → set.
Set epsPhi to be the term λX h ⇒ λu ∈ int ⨯ X ⇒ if u 0 < 0 then omega_iterate (- (u 0)) (inv X h) (u 1) else omega_iterate (u 0) h (u 1) of type set → (set → set) → set.
Set eps to be the term λA ⇒ unpack_u_i A epsPhi of type set → set.
We will prove MetaAdjunction_strict (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_u_bij Hom_struct_u struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps.
We prove the intermediate claim L1: ∀X, ∀u ∈ int ⨯ X, (u 0 + 1,u 1) ∈ int ⨯ X.
Let X and u be given.
Assume Hu.
Apply tuple_2_setprod int X to the current goal.
We will prove u 0 + 1 ∈ int.
Apply int_add_SNo to the current goal.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
An exact proof term for the current goal is nat_p_int 1 nat_1.
We will prove u 1 ∈ X.
An exact proof term for the current goal is ap1_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim L1b: ∀X, bij (int ⨯ X) (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)).
Let X be given.
Apply bijI to the current goal.
An exact proof term for the current goal is L1 X.
Let u be given.
Assume Hu.
Let v be given.
Assume Hv.
Assume H1: (u 0 + 1,u 1) = (v 0 + 1,v 1).
We will prove u = v.
Apply tuple_2_inj (u 0 + 1) (u 1) (v 0 + 1) (v 1) H1 to the current goal.
Assume H2: u 0 + 1 = v 0 + 1.
Assume H3: u 1 = v 1.
rewrite the current goal using tuple_lam_eta int (λ_ ⇒ X) u Hu (from right to left).
rewrite the current goal using tuple_lam_eta int (λ_ ⇒ X) v Hv (from right to left).
We will prove (u 0,u 1) = (v 0,v 1).
We prove the intermediate claim Lu0: u 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim Lv0: v 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) v Hv.
rewrite the current goal using add_SNo_cancel_R (u 0) 1 (v 0) (int_SNo (u 0) Lu0) SNo_1 (int_SNo (v 0) Lv0) H2 (from left to right).
rewrite the current goal using H3 (from left to right).
Use reflexivity.
Let w be given.
Assume Hw: w ∈ int ⨯ X.
We will prove ∃u ∈ int ⨯ X, (u 0 + 1,u 1) = w.
We prove the intermediate claim Lw0: w 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) w Hw.
We prove the intermediate claim Lw1: w 1 ∈ X.
An exact proof term for the current goal is ap1_lam int (λ_ ⇒ X) w Hw.
We use (w 0 + - 1,w 1) to witness the existential quantifier.
Apply andI to the current goal.
We will prove (w 0 + - 1,w 1) ∈ int ⨯ X.
Apply tuple_2_setprod int X to the current goal.
We will prove w 0 + - 1 ∈ int.
Apply int_add_SNo to the current goal.
An exact proof term for the current goal is Lw0.
Apply int_minus_SNo to the current goal.
Apply nat_p_int to the current goal.
An exact proof term for the current goal is nat_1.
We will prove w 1 ∈ X.
An exact proof term for the current goal is Lw1.
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove ((w 0 + - 1) + 1,w 1) = w.
rewrite the current goal using add_SNo_minus_R2' (w 0) 1 (int_SNo (w 0) Lw0) SNo_1 (from left to right).
We will prove (w 0,w 1) = w.
An exact proof term for the current goal is tuple_lam_eta int (λ_ ⇒ X) w Hw.
We prove the intermediate claim Letabeta: ∀X, ∀x ∈ X, eta X x = (0,x).
Let X and x be given.
Assume Hx.
An exact proof term for the current goal is beta X (λx ⇒ (0,x)) x Hx.
Set Phi to be the term λX' h ⇒ bij X' X' (λx ⇒ h x) of type set → (set → set) → prop.
We prove the intermediate claim LPhi1: ∀X, ∀h : set → set, ∀h' : set → set, (∀x ∈ X, h x = h' x) → Phi X h → Phi X h'.
Let X, h and h' be given.
Assume Hhh'.
Assume Hh: bij X X h.
Apply bijE X X h Hh to the current goal.
Assume Hh1 Hh2 Hh3.
We will prove bij X X h'.
Apply bijI to the current goal.
Let x be given.
Assume Hx.
We will prove h' x ∈ X.
rewrite the current goal using Hhh' x Hx (from right to left).
An exact proof term for the current goal is Hh1 x Hx.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy.
We will prove h' x = h' y → x = y.
rewrite the current goal using Hhh' x Hx (from right to left).
rewrite the current goal using Hhh' y Hy (from right to left).
An exact proof term for the current goal is Hh2 x Hx y Hy.
Let z be given.
Assume Hz: z ∈ X.
We will prove ∃x ∈ X, h' x = z.
Apply Hh3 z Hz to the current goal.
Let x be given.
Assume H.
Apply H to the current goal.
Assume Hx: x ∈ X.
Assume Hxz: h x = z.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx.
We will prove h' x = z.
rewrite the current goal using Hhh' x Hx (from right to left).
An exact proof term for the current goal is Hxz.
We prove the intermediate claim L2: ∀X, ∀h : set → set, ∀h' : set → set, (∀x ∈ X, h x = h' x) → (Phi X h') = (Phi X h).
Let X and h be given.
Let h' be given.
Assume Hhh'.
Apply prop_ext_2 to the current goal.
Assume H1: Phi X h'.
Apply LPhi1 X h' h to the current goal.
Let x be given.
Assume Hx.
Use symmetry.
An exact proof term for the current goal is Hhh' x Hx.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is LPhi1 X h h' Hhh'.
We prove the intermediate claim L3: ∀X, ∀h : set → set, (∀x ∈ X, h x ∈ X) → ∀u ∈ omega ⨯ X, omega_iterate (u 0) h (u 1) ∈ X.
Let X and h be given.
Assume Hh.
Let u be given.
Assume Hu.
An exact proof term for the current goal is omega_iterate_In X (u 1) (ap1_lam omega (λ_ ⇒ X) u Hu) h Hh (u 0) (omega_nat_p (u 0) (ap0_lam omega (λ_ ⇒ X) u Hu)).
We prove the intermediate claim L4: ∀X, ∀h : set → set, bij X X h → ∀h' : set → set, (∀x ∈ X, h x = h' x) → (epsPhi X h') = (epsPhi X h).
Let X and h be given.
Assume Hh.
Let h' be given.
Assume Hhh'.
We prove the intermediate claim Lih: bij X X (inv X h).
An exact proof term for the current goal is bij_inv X X h Hh.
Apply bijE X X h Hh to the current goal.
Assume Hh1 Hh2 Hh3.
Apply bijE X X (inv X h) Lih to the current goal.
Assume Hih1 Hih2 Hih3.
We prove the intermediate claim Lh': bij X X h'.
An exact proof term for the current goal is LPhi1 X h h' Hhh' Hh.
Apply bijE X X h' Lh' to the current goal.
Assume Hh'1 Hh'2 Hh'3.
We prove the intermediate claim Lih': bij X X (inv X h').
An exact proof term for the current goal is bij_inv X X h' Lh'.
Apply bijE X X (inv X h') Lih' to the current goal.
Assume Hih'1 Hih'2 Hih'3.
We will prove (λu ∈ int ⨯ X ⇒ if u 0 < 0 then omega_iterate (- (u 0)) (inv X h') (u 1) else omega_iterate (u 0) h' (u 1)) = (λu ∈ int ⨯ X ⇒ if u 0 < 0 then omega_iterate (- (u 0)) (inv X h) (u 1) else omega_iterate (u 0) h (u 1)).
Apply lam_ext to the current goal.
Let u be given.
Assume Hu.
Use symmetry.
We will prove (if u 0 < 0 then omega_iterate (- (u 0)) (inv X h) (u 1) else omega_iterate (u 0) h (u 1)) = (if u 0 < 0 then omega_iterate (- (u 0)) (inv X h') (u 1) else omega_iterate (u 0) h' (u 1)).
We prove the intermediate claim Lu0: u 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
Apply int_neg_or_nonneg (u 0) Lu0 to the current goal.
Assume H1: u 0 < 0.
Assume H2: - u 0 ∈ omega.
rewrite the current goal using If_i_1 (u 0 < 0) (omega_iterate (- (u 0)) (inv X h) (u 1)) (omega_iterate (u 0) h (u 1)) H1 (from left to right).
rewrite the current goal using If_i_1 (u 0 < 0) (omega_iterate (- (u 0)) (inv X h') (u 1)) (omega_iterate (u 0) h' (u 1)) H1 (from left to right).
We will prove omega_iterate (- (u 0)) (inv X h) (u 1) = omega_iterate (- (u 0)) (inv X h') (u 1).
We prove the intermediate claim Lihih': ∀x ∈ X, inv X h x = inv X h' x.
Let x be given.
Assume Hx.
We will prove inv X h x = inv X h' x.
Apply Hh2 to the current goal.
We will prove inv X h x ∈ X.
An exact proof term for the current goal is Hih1 x Hx.
We will prove inv X h' x ∈ X.
An exact proof term for the current goal is Hih'1 x Hx.
We will prove h (inv X h x) = h (inv X h' x).
Use transitivity with x, and h' (inv X h' x).
We will prove h (inv X h x) = x.
Apply surj_rinv X X h Hh3 x Hx to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We will prove x = h' (inv X h' x).
Use symmetry.
Apply surj_rinv X X h' Hh'3 x Hx to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We will prove h' (inv X h' x) = h (inv X h' x).
Use symmetry.
Apply Hhh' to the current goal.
We will prove inv X h' x ∈ X.
An exact proof term for the current goal is Hih'1 x Hx.
An exact proof term for the current goal is omega_iterate_ext X (u 1) (ap1_lam int (λ_ ⇒ X) u Hu) (inv X h) (inv X h') Hih1 Lihih' (- u 0) (omega_nat_p (- u 0) H2).
Assume H1: 0 <= u 0.
Assume H2: ¬ (u 0 < 0).
Assume H3: u 0 ∈ omega.
rewrite the current goal using If_i_0 (u 0 < 0) (omega_iterate (- (u 0)) (inv X h) (u 1)) (omega_iterate (u 0) h (u 1)) H2 (from left to right).
rewrite the current goal using If_i_0 (u 0 < 0) (omega_iterate (- (u 0)) (inv X h') (u 1)) (omega_iterate (u 0) h' (u 1)) H2 (from left to right).
We will prove omega_iterate (u 0) h (u 1) = omega_iterate (u 0) h' (u 1).
An exact proof term for the current goal is omega_iterate_ext X (u 1) (ap1_lam int (λ_ ⇒ X) u Hu) h h' Hh1 Hhh' (u 0) (omega_nat_p (u 0) H3).
We prove the intermediate claim Lepseq: ∀X, ∀h : set → set, bij X X h → eps (pack_u X h) = epsPhi X h.
Let X and h be given.
Assume Hh.
An exact proof term for the current goal is unpack_u_i_eq epsPhi X h (L4 X h Hh).
We prove the intermediate claim Lepsbetaint: ∀X, ∀h : set → set, bij X X h → ∀n ∈ int, ∀x ∈ X, eps (pack_u X h) (n,x) = if n < 0 then omega_iterate (- n) (inv X h) x else omega_iterate n h x.
Let X and h be given.
Assume Hh.
Let n be given.
Assume Hn.
Let x be given.
Assume Hx.
We will prove eps (pack_u X h) (n,x) = if n < 0 then omega_iterate (- n) (inv X h) x else omega_iterate n h x.
Use transitivity with epsPhi X h (n,x), and if (n,x) 0 < 0 then omega_iterate (- ((n,x) 0)) (inv X h) ((n,x) 1) else omega_iterate ((n,x) 0) h ((n,x) 1).
Use f_equal.
An exact proof term for the current goal is Lepseq X h Hh.
An exact proof term for the current goal is beta (int ⨯ X) (λu ⇒ if u 0 < 0 then omega_iterate (- (u 0)) (inv X h) (u 1) else omega_iterate (u 0) h (u 1)) (n,x) (tuple_2_setprod int X n Hn x Hx).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Use reflexivity.
We prove the intermediate claim Lepsbetanonneg: ∀X, ∀h : set → set, bij X X h → ∀n ∈ omega, ∀x ∈ X, eps (pack_u X h) (n,x) = omega_iterate n h x.
Let X and h be given.
Assume Hh.
Let n be given.
Assume Hn.
Let x be given.
Assume Hx.
We will prove eps (pack_u X h) (n,x) = omega_iterate n h x.
Use transitivity with and if n < 0 then omega_iterate (- n) (inv X h) x else omega_iterate n h x.
An exact proof term for the current goal is Lepsbetaint X h Hh n (Subq_omega_int n Hn) x Hx.
Apply If_i_0 to the current goal.
We will prove ¬ (n < 0).
Assume H1: n < 0.
Apply EmptyE n to the current goal.
We will prove n ∈ 0.
An exact proof term for the current goal is ordinal_SNoLt_In n 0 (nat_p_ordinal n (omega_nat_p n Hn)) ordinal_Empty H1.
We prove the intermediate claim Lepsbetaneg: ∀X, ∀h : set → set, bij X X h → ∀n ∈ int, n < 0 → ∀x ∈ X, eps (pack_u X h) (n,x) = omega_iterate (- n) (inv X h) x.
Let X and h be given.
Assume Hh.
Let n be given.
Assume Hn Hnneg.
Let x be given.
Assume Hx.
We will prove eps (pack_u X h) (n,x) = omega_iterate (- n) (inv X h) x.
Use transitivity with and if n < 0 then omega_iterate (- n) (inv X h) x else omega_iterate n h x.
An exact proof term for the current goal is Lepsbetaint X h Hh n Hn x Hx.
Apply If_i_1 to the current goal.
An exact proof term for the current goal is Hnneg.
We prove the intermediate claim LepsIn: ∀X, ∀h : set → set, bij X X h → ∀n ∈ int, ∀x ∈ X, eps (pack_u X h) (n,x) ∈ X.
Let X and h be given.
Assume Hh.
Let n be given.
Assume Hn.
Let x be given.
Assume Hx.
Apply bijE X X h Hh to the current goal.
Assume Hh1 Hh2 Hh3.
We prove the intermediate claim Lih: bij X X (inv X h).
An exact proof term for the current goal is bij_inv X X h Hh.
Apply bijE X X (inv X h) Lih to the current goal.
Assume Hih1 Hih2 Hih3.
Apply int_neg_or_nonneg n Hn to the current goal.
Assume H1: n < 0.
Assume H2: - n ∈ omega.
We will prove eps (pack_u X h) (n,x) ∈ X.
We prove the intermediate claim LepsIn1: omega_iterate (- n) (inv X h) x ∈ X.
An exact proof term for the current goal is omega_iterate_In X x Hx (inv X h) Hih1 (- n) (omega_nat_p (- n) H2).
An exact proof term for the current goal is Lepsbetaneg X h Hh n Hn H1 x Hx (λ_ v ⇒ v ∈ X) LepsIn1.
Assume H1: 0 <= n.
Assume H2: ¬ (n < 0).
Assume H3: n ∈ omega.
We prove the intermediate claim LepsIn2: omega_iterate n h x ∈ X.
An exact proof term for the current goal is omega_iterate_In X x Hx h Hh1 n (omega_nat_p n H3).
An exact proof term for the current goal is Lepsbetanonneg X h Hh n H3 x Hx (λ_ v ⇒ v ∈ X) LepsIn2.
We prove the intermediate claim LepsInP: ∀X, ∀h : set → set, bij X X h → ∀u ∈ int ⨯ X, eps (pack_u X h) u ∈ X.
Let X and h be given.
Assume Hh.
Let u be given.
Assume Hu.
rewrite the current goal using tuple_lam_eta int (λ_ ⇒ X) u Hu (from right to left).
An exact proof term for the current goal is LepsIn X h Hh (u 0) (ap0_lam int (λ_ ⇒ X) u Hu) (u 1) (ap1_lam int (λ_ ⇒ X) u Hu).
Apply MetaAdjunction_strict_I to the current goal.
We will prove MetaFunctor_strict (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_u_bij Hom_struct_u struct_id struct_comp F0 F1.
Apply MetaFunctor_strict_I to the current goal.
We will prove MetaCat (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)).
An exact proof term for the current goal is MetaCatSet.
We will prove MetaCat struct_u_bij Hom_struct_u struct_id struct_comp.
An exact proof term for the current goal is MetaCat_struct_u_bij.
We will prove MetaFunctor (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_u_bij Hom_struct_u struct_id struct_comp F0 F1.
Apply MetaFunctor_I to the current goal.
Let X be given.
Assume HX.
We will prove struct_u_bij (F0 X).
We will prove struct_u (F0 X) ∧ unpack_u_o (F0 X) (λX' h ⇒ bij X' X' h).
Apply andI to the current goal.
We will prove struct_u (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))).
Apply pack_struct_u_I to the current goal.
We will prove ∀u ∈ int ⨯ X, (u 0 + 1,u 1) ∈ int ⨯ X.
An exact proof term for the current goal is L1 X.
We will prove unpack_u_o (F0 X) (λX' h ⇒ bij X' X' h).
We prove the intermediate claim L5: ∀G : set → set, (∀u ∈ int ⨯ X, (u 0 + 1,u 1) = G u) → (Phi (int ⨯ X) G) = (Phi (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))).
An exact proof term for the current goal is L2 (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)).
We will prove unpack_u_o (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (λX' h ⇒ bij X' X' h).
rewrite the current goal using unpack_u_o_eq Phi (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) L5 (from left to right).
We will prove bij (int ⨯ X) (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)).
An exact proof term for the current goal is L1b X.
Let X, Y and f be given.
Assume HX HY Hf.
We will prove Hom_struct_u (F0 X) (F0 Y) (F1 X Y f).
We will prove Hom_struct_u (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (pack_u (int ⨯ Y) (λu ⇒ (u 0 + 1,u 1))) (λu ∈ int ⨯ X ⇒ (u 0,f (u 1))).
rewrite the current goal using Hom_struct_u_pack (from left to right).
Apply andI to the current goal.
We will prove (λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) ∈ (int ⨯ Y)(int ⨯ X).
We will prove (λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) ∈ ∏x ∈ int ⨯ X, int ⨯ Y.
Apply lam_Pi to the current goal.
Let u be given.
Assume Hu: u ∈ int ⨯ X.
We will prove (u 0,f (u 1)) ∈ int ⨯ Y.
We will prove (u 0,f (u 1)) ∈ int ⨯ Y.
Apply tuple_2_setprod int Y (u 0) (ap0_lam int (λ_ ⇒ X) u Hu) (f (u 1)) to the current goal.
We will prove f (u 1) ∈ Y.
Apply ap_Pi X (λ_ ⇒ Y) f (u 1) Hf to the current goal.
We will prove u 1 ∈ X.
An exact proof term for the current goal is ap1_lam int (λ_ ⇒ X) u Hu.
Let u be given.
Assume Hu: u ∈ int ⨯ X.
We will prove (λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) (u 0 + 1,u 1) = (((λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) u 0 + 1),((λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) u 1)).
rewrite the current goal using beta (int ⨯ X) (λu ⇒ (u 0,f (u 1))) (u 0 + 1,u 1) (L1 X u Hu) (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove (u 0 + 1,f (u 1)) = ((λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) u 0 + 1,((λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) u 1)).
rewrite the current goal using beta (int ⨯ X) (λu ⇒ (u 0,f (u 1))) u Hu (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Use reflexivity.
Let X be given.
Assume HX.
We will prove F1 X X (lam_id X) = struct_id (F0 X).
We will prove F1 X X (lam_id X) = (λu ∈ pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) 0 ⇒ u).
We will prove (λu ∈ int ⨯ X ⇒ (u 0,lam_id X (u 1))) = (λu ∈ pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) 0 ⇒ u).
rewrite the current goal using pack_u_0_eq2 (from right to left).
Apply lam_ext to the current goal.
Let u be given.
Assume Hu: u ∈ int ⨯ X.
We will prove (u 0,lam_id X (u 1)) = u.
We will prove (u 0,(λx ∈ X ⇒ x) (u 1)) = u.
rewrite the current goal using beta X (λx ⇒ x) (u 1) (ap1_lam int (λ_ ⇒ X) u Hu) (from left to right).
We will prove (u 0,u 1) = u.
An exact proof term for the current goal is tuple_lam_eta int (λ_ ⇒ X) u Hu.
Let X, Y, Z, f and g be given.
Assume HX HY HZ Hf Hg.
We will prove F1 X Z (lam_comp X g f) = struct_comp (F0 X) (F0 Y) (F0 Z) (F1 Y Z g) (F1 X Y f).
We will prove (λu ∈ int ⨯ X ⇒ (u 0,lam_comp X g f (u 1))) = lam_comp (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) 0) (F1 Y Z g) (F1 X Y f).
rewrite the current goal using pack_u_0_eq2 (from right to left).
We will prove (λu ∈ int ⨯ X ⇒ (u 0,lam_comp X g f (u 1))) = (λu ∈ int ⨯ X ⇒ (F1 Y Z g (F1 X Y f u))).
Apply lam_ext to the current goal.
Let u be given.
Assume Hu.
We will prove (u 0,lam_comp X g f (u 1)) = F1 Y Z g (F1 X Y f u).
We will prove (u 0,lam_comp X g f (u 1)) = F1 Y Z g ((λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) u).
rewrite the current goal using beta (int ⨯ X) (λu ⇒ (u 0,f (u 1))) u Hu (from left to right).
We will prove (u 0,lam_comp X g f (u 1)) = F1 Y Z g (u 0,f (u 1)).
We prove the intermediate claim LufY: (u 0,f (u 1)) ∈ int ⨯ Y.
Apply tuple_2_setprod int Y to the current goal.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f (u 1) Hf (ap1_lam int (λ_ ⇒ X) u Hu).
We will prove (u 0,lam_comp X g f (u 1)) = (λv ∈ int ⨯ Y ⇒ (v 0,g (v 1))) (u 0,f (u 1)).
rewrite the current goal using beta (int ⨯ Y) (λv ⇒ (v 0,g (v 1))) (u 0,f (u 1)) LufY (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove (u 0,lam_comp X g f (u 1)) = (u 0,g (f (u 1))).
We will prove (u 0,((λx ∈ X ⇒ g (f x)) (u 1))) = (u 0,g (f (u 1))).
rewrite the current goal using beta X (λx ⇒ g (f x)) (u 1) (ap1_lam int (λ_ ⇒ X) u Hu) (from left to right).
Use reflexivity.
We will prove MetaFunctor struct_u_bij Hom_struct_u struct_id struct_comp (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X 0) (λX Y f ⇒ f).
An exact proof term for the current goal is MetaCat_struct_u_bij_Forgetful.
We will prove MetaNatTrans (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) (λX ⇒ X) (λX Y f ⇒ f) (λX ⇒ F0 X 0) (λX Y f ⇒ F1 X Y f) eta.
Apply MetaNatTrans_I to the current goal.
Let X be given.
Assume _.
We will prove HomSet X (F0 X 0) (eta X).
We will prove eta X ∈ pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) 0X.
rewrite the current goal using pack_u_0_eq2 (from right to left).
We will prove eta X ∈ (int ⨯ X)X.
We will prove (λx ∈ X ⇒ (0,x)) ∈ ∏x ∈ X, int ⨯ X.
Apply lam_Pi to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We will prove (0,x) ∈ int ⨯ X.
Apply tuple_2_setprod to the current goal.
An exact proof term for the current goal is nat_p_int 0 nat_0.
An exact proof term for the current goal is Hx.
Let X, Y and f be given.
Assume _ _.
Assume Hf: HomSet X Y f.
We will prove lam_comp X (F1 X Y f) (eta X) = lam_comp X (eta Y) f.
We will prove (λx ∈ X ⇒ F1 X Y f (eta X x)) = (λx ∈ X ⇒ eta Y (f x)).
Apply lam_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We will prove F1 X Y f (eta X x) = eta Y (f x).
Use transitivity with F1 X Y f (0,x), and (0,f x).
Use f_equal.
An exact proof term for the current goal is Letabeta X x Hx.
We will prove (λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) (0,x) = (0,f x).
rewrite the current goal using beta (int ⨯ X) (λu ⇒ (u 0,f (u 1))) (0,x) (tuple_2_setprod int X 0 (nat_p_int 0 nat_0) x Hx) (from left to right).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
Use reflexivity.
Use symmetry.
An exact proof term for the current goal is Letabeta Y (f x) (ap_Pi X (λ_ ⇒ Y) f x Hf Hx).
We will prove MetaNatTrans struct_u_bij Hom_struct_u struct_id struct_comp struct_u_bij Hom_struct_u struct_id struct_comp (λY ⇒ F0 (Y 0)) (λX Y g ⇒ F1 (X 0) (Y 0) g) (λY ⇒ Y) (λX Y g ⇒ g) eps.
Apply MetaNatTrans_I to the current goal.
Let A be given.
Assume HA.
We will prove Hom_struct_u (F0 (A 0)) A (eps A).
Apply HA to the current goal.
Assume HAs.
Apply HAs to the current goal.
Let X and h be given.
Assume Hh: ∀x ∈ X, h x ∈ X.
We will prove unpack_u_o (pack_u X h) Phi → Hom_struct_u (F0 (pack_u X h 0)) (pack_u X h) (eps (pack_u X h)).
rewrite the current goal using pack_u_0_eq2 (from right to left).
We will prove unpack_u_o (pack_u X h) Phi → Hom_struct_u (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (pack_u X h) (eps (pack_u X h)).
rewrite the current goal using unpack_u_o_eq Phi X h (L2 X h) (from left to right).
Assume Hh2: bij X X h.
Apply bijE X X h Hh2 to the current goal.
Assume Hh2a Hh2b Hh2c.
We prove the intermediate claim Lih: bij X X (inv X h).
An exact proof term for the current goal is bij_inv X X h Hh2.
Apply bijE X X (inv X h) Lih to the current goal.
Assume Hih1 Hih2 Hih3.
rewrite the current goal using Hom_struct_u_pack (from left to right).
Apply andI to the current goal.
We will prove eps (pack_u X h) ∈ X(int ⨯ X).
We prove the intermediate claim L6: (λu ∈ int ⨯ X ⇒ if u 0 < 0 then omega_iterate (- (u 0)) (inv X h) (u 1) else omega_iterate (u 0) h (u 1)) ∈ ∏u ∈ int ⨯ X, X.
Apply lam_Pi to the current goal.
Let u be given.
Assume Hu: u ∈ int ⨯ X.
We will prove (if u 0 < 0 then omega_iterate (- (u 0)) (inv X h) (u 1) else omega_iterate (u 0) h (u 1)) ∈ X.
We prove the intermediate claim Lu0: u 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim Lu1: u 1 ∈ X.
An exact proof term for the current goal is ap1_lam int (λ_ ⇒ X) u Hu.
Apply int_neg_or_nonneg (u 0) Lu0 to the current goal.
Assume H1: u 0 < 0.
Assume H2: - u 0 ∈ omega.
rewrite the current goal using If_i_1 (u 0 < 0) (omega_iterate (- (u 0)) (inv X h) (u 1)) (omega_iterate (u 0) h (u 1)) H1 (from left to right).
We will prove omega_iterate (- (u 0)) (inv X h) (u 1) ∈ X.
An exact proof term for the current goal is omega_iterate_In X (u 1) Lu1 (inv X h) Hih1 (- (u 0)) (omega_nat_p (- (u 0)) H2).
Assume H1: 0 <= u 0.
Assume H2: ¬ (u 0 < 0).
Assume H3: u 0 ∈ omega.
rewrite the current goal using If_i_0 (u 0 < 0) (omega_iterate (- (u 0)) (inv X h) (u 1)) (omega_iterate (u 0) h (u 1)) H2 (from left to right).
We will prove omega_iterate (u 0) h (u 1) ∈ X.
An exact proof term for the current goal is omega_iterate_In X (u 1) Lu1 h Hh2a (u 0) (omega_nat_p (u 0) H3).
An exact proof term for the current goal is Lepseq X h Hh2 (λ_ u ⇒ u ∈ X(int ⨯ X)) L6.
We will prove ∀u ∈ int ⨯ X, eps (pack_u X h) (u 0 + 1,u 1) = h (eps (pack_u X h) u).
Let u be given.
Assume Hu: u ∈ int ⨯ X.
We prove the intermediate claim Lu0: u 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim Lu1: u 1 ∈ X.
An exact proof term for the current goal is ap1_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim LSu0: u 0 + 1 ∈ int.
An exact proof term for the current goal is int_add_SNo (u 0) Lu0 1 (nat_p_int 1 nat_1).
We prove the intermediate claim Lu0S: SNo (u 0).
An exact proof term for the current goal is int_SNo (u 0) Lu0.
We will prove eps (pack_u X h) (u 0 + 1,u 1) = h (eps (pack_u X h) u).
Use transitivity with and if u 0 + 1 < 0 then omega_iterate (- (u 0 + 1)) (inv X h) (u 1) else omega_iterate (u 0 + 1) h (u 1).
An exact proof term for the current goal is Lepsbetaint X h Hh2 (u 0 + 1) LSu0 (u 1) Lu1.
We will prove (if u 0 + 1 < 0 then omega_iterate (- (u 0 + 1)) (inv X h) (u 1) else omega_iterate (u 0 + 1) h (u 1)) = h (eps (pack_u X h) u).
Apply int_neg_or_nonneg (u 0 + 1) LSu0 to the current goal.
Assume H1: u 0 + 1 < 0.
Assume H2: - (u 0 + 1) ∈ omega.
rewrite the current goal using If_i_1 (u 0 + 1 < 0) (omega_iterate (- (u 0 + 1)) (inv X h) (u 1)) (omega_iterate (u 0 + 1) h (u 1)) H1 (from left to right).
We will prove omega_iterate (- (u 0 + 1)) (inv X h) (u 1) = h (eps (pack_u X h) u).
Apply Hih2 to the current goal.
We will prove omega_iterate (- (u 0 + 1)) (inv X h) (u 1) ∈ X.
Apply omega_iterate_In X (u 1) Lu1 (inv X h) Hih1 (- (u 0 + 1)) to the current goal.
We will prove nat_p (- (u 0 + 1)).
An exact proof term for the current goal is omega_nat_p (- (u 0 + 1)) H2.
We will prove h (eps (pack_u X h) u) ∈ X.
Apply Hh to the current goal.
We will prove eps (pack_u X h) u ∈ X.
rewrite the current goal using tuple_lam_eta int (λ_ ⇒ X) u Hu (from right to left).
An exact proof term for the current goal is LepsIn X h Hh2 (u 0) Lu0 (u 1) Lu1.
We will prove inv X h (omega_iterate (- (u 0 + 1)) (inv X h) (u 1)) = inv X h (h (eps (pack_u X h) u)).
Use transitivity with omega_iterate (- u 0) (inv X h) (u 1), and eps (pack_u X h) u.
We will prove inv X h (omega_iterate (- (u 0 + 1)) (inv X h) (u 1)) = omega_iterate (- u 0) (inv X h) (u 1).
rewrite the current goal using omega_iterate_S_out (- (u 0 + 1)) H2 (from right to left).
We will prove omega_iterate (ordsucc (- (u 0 + 1))) (inv X h) (u 1) = omega_iterate (- u 0) (inv X h) (u 1).
rewrite the current goal using ordinal_ordsucc_SNo_eq (- (u 0 + 1)) (nat_p_ordinal (- (u 0 + 1)) (omega_nat_p (- (u 0 + 1)) H2)) (from left to right).
We will prove omega_iterate (1 + - (u 0 + 1)) (inv X h) (u 1) = omega_iterate (- u 0) (inv X h) (u 1).
rewrite the current goal using add_SNo_com (u 0) 1 (int_SNo (u 0) Lu0) SNo_1 (from left to right).
rewrite the current goal using minus_add_SNo_distr 1 (u 0) SNo_1 (int_SNo (u 0) Lu0) (from left to right).
We will prove omega_iterate (1 + - 1 + - u 0) (inv X h) (u 1) = omega_iterate (- u 0) (inv X h) (u 1).
rewrite the current goal using add_SNo_minus_SNo_prop2 1 (- u 0) SNo_1 (SNo_minus_SNo (u 0) (int_SNo (u 0) Lu0)) (from left to right).
Use reflexivity.
We will prove omega_iterate (- u 0) (inv X h) (u 1) = eps (pack_u X h) u.
Use symmetry.
rewrite the current goal using tuple_lam_eta int (λ_ ⇒ X) u Hu (from right to left) at position 1.
We will prove eps (pack_u X h) (u 0,u 1) = omega_iterate (- u 0) (inv X h) (u 1).
We prove the intermediate claim Lu0neg: u 0 < 0.
Apply SNoLt_tra (u 0) (u 0 + 1) 0 Lu0S (SNo_add_SNo (u 0) 1 Lu0S SNo_1) SNo_0 to the current goal.
We will prove u 0 < u 0 + 1.
rewrite the current goal using add_SNo_0R (u 0) Lu0S (from right to left) at position 1.
Apply add_SNo_Lt2 (u 0) 0 1 Lu0S SNo_0 SNo_1 to the current goal.
We will prove 0 < 1.
An exact proof term for the current goal is SNoLt_0_1.
We will prove u 0 + 1 < 0.
An exact proof term for the current goal is H1.
An exact proof term for the current goal is Lepsbetaneg X h Hh2 (u 0) Lu0 Lu0neg (u 1) Lu1.
We will prove eps (pack_u X h) u = inv X h (h (eps (pack_u X h) u)).
Use symmetry.
An exact proof term for the current goal is inj_linv X h Hh2b (eps (pack_u X h) u) (LepsInP X h Hh2 u Hu).
Assume H1: 0 <= u 0 + 1.
Assume H2: ¬ (u 0 + 1 < 0).
Assume H3: u 0 + 1 ∈ omega.
rewrite the current goal using If_i_0 (u 0 + 1 < 0) (omega_iterate (- (u 0 + 1)) (inv X h) (u 1)) (omega_iterate (u 0 + 1) h (u 1)) H2 (from left to right).
We will prove omega_iterate (u 0 + 1) h (u 1) = h (eps (pack_u X h) u).
Apply SNoLeE 0 (u 0 + 1) SNo_0 (int_SNo (u 0 + 1) LSu0) H1 to the current goal.
Assume H4: 0 < u 0 + 1.
We prove the intermediate claim Lu0n: u 0 ∈ omega.
Apply int_neg_or_nonneg (u 0) Lu0 to the current goal.
Assume H5: u 0 < 0.
Assume H6: - u 0 ∈ omega.
We will prove False.
We prove the intermediate claim Lmu0pos: 0 < - u 0.
rewrite the current goal using minus_SNo_0 (from right to left) at position 1.
Apply minus_SNo_Lt_contra (u 0) 0 Lu0S SNo_0 to the current goal.
We will prove u 0 < 0.
An exact proof term for the current goal is H5.
Apply nat_inv (- u 0) (omega_nat_p (- u 0) H6) to the current goal.
Assume H7: - u 0 = 0.
Apply SNoLt_irref 0 to the current goal.
We will prove 0 < 0.
rewrite the current goal using H7 (from right to left) at position 2.
An exact proof term for the current goal is Lmu0pos.
Assume H.
Apply H to the current goal.
Let n be given.
Assume H.
Apply H to the current goal.
Assume Hn: nat_p n.
Assume H7: - u 0 = ordsucc n.
Apply neq_ordsucc_0 n to the current goal.
We will prove ordsucc n = 0.
Apply SingE to the current goal.
We will prove ordsucc n ∈ {0}.
rewrite the current goal using eq_1_Sing0 (from right to left).
We will prove ordsucc n ∈ 1.
Apply ordinal_SNoLt_In (ordsucc n) 1 (ordinal_ordsucc n (nat_p_ordinal n Hn)) (nat_p_ordinal 1 nat_1) to the current goal.
We will prove ordsucc n < 1.
rewrite the current goal using H7 (from right to left).
We will prove - u 0 < 1.
Apply add_SNo_Lt2_cancel (u 0) (- u 0) 1 Lu0S (SNo_minus_SNo (u 0) Lu0S) SNo_1 to the current goal.
We will prove u 0 + - u 0 < u 0 + 1.
rewrite the current goal using add_SNo_minus_SNo_rinv (u 0) Lu0S (from left to right).
An exact proof term for the current goal is H4.
Assume _ _ H5.
An exact proof term for the current goal is H5.
We prove the intermediate claim Lu0o: ordinal (u 0).
An exact proof term for the current goal is nat_p_ordinal (u 0) (omega_nat_p (u 0) Lu0n).
We will prove omega_iterate (u 0 + 1) h (u 1) = h (eps (pack_u X h) u).
rewrite the current goal using add_SNo_com (u 0) 1 (int_SNo (u 0) Lu0) SNo_1 (from left to right).
We will prove omega_iterate (1 + u 0) h (u 1) = h (eps (pack_u X h) u).
rewrite the current goal using ordinal_ordsucc_SNo_eq (u 0) Lu0o (from right to left).
We will prove omega_iterate (ordsucc (u 0)) h (u 1) = h (eps (pack_u X h) u).
Use transitivity with and h (omega_iterate (u 0) h (u 1)).
An exact proof term for the current goal is omega_iterate_S_out (u 0) Lu0n h (u 1).
Use f_equal.
We will prove omega_iterate (u 0) h (u 1) = eps (pack_u X h) u.
Use symmetry.
rewrite the current goal using tuple_lam_eta int (λ_ ⇒ X) u Hu (from right to left) at position 1.
We will prove eps (pack_u X h) (u 0,u 1) = omega_iterate (u 0) h (u 1).
An exact proof term for the current goal is Lepsbetanonneg X h Hh2 (u 0) Lu0n (u 1) Lu1.
Assume H4: 0 = u 0 + 1.
We will prove omega_iterate (u 0 + 1) h (u 1) = h (eps (pack_u X h) u).
rewrite the current goal using H4 (from right to left).
rewrite the current goal using omega_iterate_0 (from left to right).
We will prove u 1 = h (eps (pack_u X h) u).
Apply surj_rinv X X h Hh2c (u 1) Lu1 to the current goal.
Assume _.
Assume H5: h (inv X h (u 1)) = u 1.
rewrite the current goal using H5 (from right to left).
We will prove h (inv X h (u 1)) = h (eps (pack_u X h) u).
Use f_equal.
We will prove inv X h (u 1) = eps (pack_u X h) u.
We prove the intermediate claim Lmu01: - u 0 = 1.
Apply add_SNo_cancel_L (u 0) (- u 0) 1 Lu0S (SNo_minus_SNo (u 0) Lu0S) SNo_1 to the current goal.
We will prove u 0 + - u 0 = u 0 + 1.
rewrite the current goal using add_SNo_minus_SNo_rinv (u 0) Lu0S (from left to right).
An exact proof term for the current goal is H4.
Use transitivity with and omega_iterate (- u 0) (inv X h) (u 1).
We will prove inv X h (u 1) = omega_iterate (- u 0) (inv X h) (u 1).
rewrite the current goal using Lmu01 (from left to right).
Use symmetry.
rewrite the current goal using omega_iterate_S_out 0 (nat_p_omega 0 nat_0) (from left to right).
Use f_equal.
Apply omega_iterate_0 to the current goal.
We will prove omega_iterate (- u 0) (inv X h) (u 1) = eps (pack_u X h) u.
We prove the intermediate claim Lu0neg: u 0 < 0.
Apply minus_SNo_Lt_contra3 0 (u 0) SNo_0 Lu0S to the current goal.
We will prove - 0 < - u 0.
rewrite the current goal using Lmu01 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
We will prove 0 < 1.
An exact proof term for the current goal is SNoLt_0_1.
Use symmetry.
rewrite the current goal using tuple_lam_eta int (λ_ ⇒ X) u Hu (from right to left) at position 1.
An exact proof term for the current goal is Lepsbetaneg X h Hh2 (u 0) Lu0 Lu0neg (u 1) Lu1.
Let A, B and f be given.
Assume HA HB.
We will prove Hom_struct_u A B f → lam_comp (F0 (A 0) 0) f (eps A) = lam_comp (F0 (A 0) 0) (eps B) (F1 (A 0) (B 0) f).
Apply HA to the current goal.
Assume HAs.
Apply HAs to the current goal.
Let X and h be given.
Assume Hh: ∀x ∈ X, h x ∈ X.
We will prove unpack_u_o (pack_u X h) Phi → Hom_struct_u (pack_u X h) B f → lam_comp (F0 (pack_u X h 0) 0) f (eps (pack_u X h)) = lam_comp (F0 (pack_u X h 0) 0) (eps B) (F1 (pack_u X h 0) (B 0) f).
rewrite the current goal using pack_u_0_eq2 (from right to left).
rewrite the current goal using unpack_u_o_eq Phi X h (L2 X h) (from left to right).
Assume Hh2: bij X X h.
Apply bijE X X h Hh2 to the current goal.
Assume Hh2a Hh2b Hh2c.
We will prove Hom_struct_u (pack_u X h) B f → lam_comp (F0 X 0) f (eps (pack_u X h)) = lam_comp (F0 X 0) (eps B) (F1 X (B 0) f).
Apply HB to the current goal.
Assume HBs.
Apply HBs to the current goal.
Let Y and k be given.
Assume Hk: ∀y ∈ Y, k y ∈ Y.
We will prove unpack_u_o (pack_u Y k) Phi → Hom_struct_u (pack_u X h) (pack_u Y k) f → lam_comp (F0 X 0) f (eps (pack_u X h)) = lam_comp (F0 X 0) (eps (pack_u Y k)) (F1 X (pack_u Y k 0) f).
rewrite the current goal using unpack_u_o_eq Phi Y k (L2 Y k) (from left to right).
Assume Hk2: bij Y Y k.
Apply bijE Y Y k Hk2 to the current goal.
Assume Hk2a Hk2b Hk2c.
rewrite the current goal using Hom_struct_u_pack X Y h k f (from left to right).
Assume Hf.
Apply Hf to the current goal.
Assume Hf1: f ∈ YX.
Assume Hf2: ∀x ∈ X, f (h x) = k (f x).
rewrite the current goal using pack_u_0_eq2 (from right to left).
We will prove lam_comp (F0 X 0) f (eps (pack_u X h)) = lam_comp (F0 X 0) (eps (pack_u Y k)) (F1 X Y f).
We will prove lam_comp (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) 0) f (eps (pack_u X h)) = lam_comp (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) 0) (eps (pack_u Y k)) (F1 X Y f).
rewrite the current goal using pack_u_0_eq2 (from right to left).
We will prove lam_comp (int ⨯ X) f (eps (pack_u X h)) = lam_comp (int ⨯ X) (eps (pack_u Y k)) (F1 X Y f).
We will prove (λu ∈ int ⨯ X ⇒ f (eps (pack_u X h) u)) = (λu ∈ int ⨯ X ⇒ eps (pack_u Y k) (F1 X Y f u)).
Apply lam_ext to the current goal.
Let u be given.
Assume Hu: u ∈ int ⨯ X.
We prove the intermediate claim Lu0: u 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim Lu1: u 1 ∈ X.
An exact proof term for the current goal is ap1_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim Lih: bij X X (inv X h).
An exact proof term for the current goal is bij_inv X X h Hh2.
Apply bijE X X (inv X h) Lih to the current goal.
Assume Hih1 Hih2 Hih3.
We prove the intermediate claim Lik: bij Y Y (inv Y k).
An exact proof term for the current goal is bij_inv Y Y k Hk2.
Apply bijE Y Y (inv Y k) Lik to the current goal.
Assume Hik1 Hik2 Hik3.
We will prove f (eps (pack_u X h) u) = eps (pack_u Y k) (F1 X Y f u).
We will prove f (eps (pack_u X h) u) = eps (pack_u Y k) ((λu ∈ int ⨯ X ⇒ (u 0,f (u 1))) u).
rewrite the current goal using beta (int ⨯ X) (λu ⇒ (u 0,f (u 1))) u Hu (from left to right).
We will prove f (eps (pack_u X h) u) = eps (pack_u Y k) (u 0,f (u 1)).
Use transitivity with f (if u 0 < 0 then omega_iterate (- u 0) (inv X h) (u 1) else omega_iterate (u 0) h (u 1)), and if u 0 < 0 then omega_iterate (- u 0) (inv Y k) (f (u 1)) else omega_iterate (u 0) k (f (u 1)).
Use f_equal.
We will prove eps (pack_u X h) u = if u 0 < 0 then omega_iterate (- u 0) (inv X h) (u 1) else omega_iterate (u 0) h (u 1).
rewrite the current goal using tuple_lam_eta int (λ_ ⇒ X) u Hu (from right to left) at position 1.
An exact proof term for the current goal is Lepsbetaint X h Hh2 (u 0) Lu0 (u 1) Lu1.
We will prove f (if u 0 < 0 then omega_iterate (- u 0) (inv X h) (u 1) else omega_iterate (u 0) h (u 1)) = (if u 0 < 0 then omega_iterate (- u 0) (inv Y k) (f (u 1)) else omega_iterate (u 0) k (f (u 1))).
Apply int_neg_or_nonneg (u 0) Lu0 to the current goal.
Assume H1: u 0 < 0.
Assume H2: - u 0 ∈ omega.
rewrite the current goal using If_i_1 (u 0 < 0) (omega_iterate (- u 0) (inv X h) (u 1)) (omega_iterate (u 0) h (u 1)) H1 (from left to right).
rewrite the current goal using If_i_1 (u 0 < 0) (omega_iterate (- u 0) (inv Y k) (f (u 1))) (omega_iterate (u 0) k (f (u 1))) H1 (from left to right).
We will prove f (omega_iterate (- u 0) (inv X h) (u 1)) = omega_iterate (- u 0) (inv Y k) (f (u 1)).
We prove the intermediate claim Lf: ∀x ∈ X, f (inv X h x) = inv Y k (f x).
Let x be given.
Assume Hx.
Apply Hk2b to the current goal.
We will prove f (inv X h x) ∈ Y.
Apply ap_Pi X (λ_ ⇒ Y) f (inv X h x) Hf1 to the current goal.
We will prove inv X h x ∈ X.
An exact proof term for the current goal is Hih1 x Hx.
We will prove inv Y k (f x) ∈ Y.
Apply Hik1 to the current goal.
We will prove f x ∈ Y.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x Hf1 Hx.
We will prove k (f (inv X h x)) = k (inv Y k (f x)).
Use transitivity with f (h (inv X h x)), and f x.
We will prove k (f (inv X h x)) = f (h (inv X h x)).
Use symmetry.
An exact proof term for the current goal is Hf2 (inv X h x) (Hih1 x Hx).
We will prove f (h (inv X h x)) = f x.
Use f_equal.
Apply surj_rinv X X h Hh2c x Hx to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We will prove f x = k (inv Y k (f x)).
Use symmetry.
Apply surj_rinv Y Y k Hk2c (f x) (ap_Pi X (λ_ ⇒ Y) f x Hf1 Hx) to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
An exact proof term for the current goal is omega_iterate_comm X (u 1) Lu1 (inv X h) (inv Y k) Hih1 (λx ⇒ f x) Lf (- u 0) (omega_nat_p (- u 0) H2).
Assume H1: 0 <= u 0.
Assume H2: ¬ (u 0 < 0).
Assume H3: u 0 ∈ omega.
rewrite the current goal using If_i_0 (u 0 < 0) (omega_iterate (- u 0) (inv X h) (u 1)) (omega_iterate (u 0) h (u 1)) H2 (from left to right).
rewrite the current goal using If_i_0 (u 0 < 0) (omega_iterate (- u 0) (inv Y k) (f (u 1))) (omega_iterate (u 0) k (f (u 1))) H2 (from left to right).
We will prove f (omega_iterate (u 0) h (u 1)) = omega_iterate (u 0) k (f (u 1)).
An exact proof term for the current goal is omega_iterate_comm X (u 1) Lu1 h k Hh (λx ⇒ f x) Hf2 (u 0) (omega_nat_p (u 0) H3).
Use symmetry.
An exact proof term for the current goal is Lepsbetaint Y k Hk2 (u 0) Lu0 (f (u 1)) (ap_Pi X (λ_ ⇒ Y) f (u 1) Hf1 Lu1).
We will prove MetaAdjunction (λ_ ⇒ True) HomSet (λX ⇒ (lam_id X)) (λX Y Z f g ⇒ (lam_comp X f g)) struct_u_bij Hom_struct_u struct_id struct_comp F0 F1 (λX ⇒ X 0) (λX Y f ⇒ f) eta eps.
Apply MetaAdjunction_I to the current goal.
Let X be given.
Assume _.
We will prove struct_comp (F0 X) (F0 (F0 X 0)) (F0 X) (eps (F0 X)) (F1 X (F0 X 0) (eta X)) = struct_id (F0 X).
We will prove lam_comp (F0 X 0) (eps (F0 X)) (F1 X (F0 X 0) (eta X)) = lam_id (F0 X 0).
We will prove lam_comp (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) 0) (eps (F0 X)) (F1 X (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) 0) (eta X)) = lam_id (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) 0).
rewrite the current goal using pack_u_0_eq2 (from right to left).
We will prove lam_comp (int ⨯ X) (eps (F0 X)) (F1 X (int ⨯ X) (eta X)) = lam_id (int ⨯ X).
We will prove (λu ∈ int ⨯ X ⇒ eps (F0 X) (F1 X (int ⨯ X) (eta X) u)) = (λu ∈ int ⨯ X ⇒ u).
Apply lam_ext to the current goal.
Let u be given.
Assume Hu: u ∈ int ⨯ X.
We prove the intermediate claim Lu0: u 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim Lu1: u 1 ∈ X.
An exact proof term for the current goal is ap1_lam int (λ_ ⇒ X) u Hu.
We will prove eps (F0 X) (F1 X (int ⨯ X) (eta X) u) = u.
We will prove eps (F0 X) ((λu ∈ int ⨯ X ⇒ (u 0,eta X (u 1))) u) = u.
Use transitivity with eps (F0 X) (u 0,(0,u 1)), if u 0 < 0 then omega_iterate (- u 0) (inv (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (0,u 1) else omega_iterate (u 0) (λu ⇒ (u 0 + 1,u 1)) (0,u 1), and (u 0,u 1).
Use f_equal.
Use transitivity with and (u 0,eta X (u 1)).
An exact proof term for the current goal is beta (int ⨯ X) (λu ⇒ (u 0,eta X (u 1))) u Hu.
We will prove (u 0,eta X (u 1)) = (u 0,(0,u 1)).
An exact proof term for the current goal is Letabeta X (u 1) Lu1 (λ_ v ⇒ (u 0,v) = (u 0,(0,u 1))) (λq H ⇒ H).
We will prove eps (F0 X) (u 0,(0,u 1)) = if u 0 < 0 then omega_iterate (- u 0) (inv (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (0,u 1) else omega_iterate (u 0) (λu ⇒ (u 0 + 1,u 1)) (0,u 1).
We will prove eps (pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (u 0,(0,u 1)) = if u 0 < 0 then omega_iterate (- u 0) (inv (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (0,u 1) else omega_iterate (u 0) (λu ⇒ (u 0 + 1,u 1)) (0,u 1).
Apply Lepsbetaint (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) (L1b X) (u 0) Lu0 (0,u 1) (tuple_2_setprod int X 0 (nat_p_int 0 nat_0) (u 1) Lu1) to the current goal.
We will prove (if u 0 < 0 then omega_iterate (- u 0) (inv (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (0,u 1) else omega_iterate (u 0) (λu ⇒ (u 0 + 1,u 1)) (0,u 1)) = (u 0,u 1).
Apply int_neg_or_nonneg (u 0) Lu0 to the current goal.
Assume H1: u 0 < 0.
Assume H2: - u 0 ∈ omega.
rewrite the current goal using If_i_1 (u 0 < 0) (omega_iterate (- u 0) (inv (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (0,u 1)) (omega_iterate (u 0) (λu ⇒ (u 0 + 1,u 1)) (0,u 1)) H1 (from left to right).
We will prove omega_iterate (- u 0) (inv (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (0,u 1) = (u 0,u 1).
Use transitivity with and omega_iterate (- u 0) (λu ⇒ (u 0 + - 1,u 1)) (0,u 1).
Use symmetry.
We prove the intermediate claim L7: ∀u ∈ int ⨯ X, (u 0 + - 1,u 1) ∈ int ⨯ X.
Let u be given.
Assume Hu.
We prove the intermediate claim Lu0: u 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim Lu1: u 1 ∈ X.
An exact proof term for the current goal is ap1_lam int (λ_ ⇒ X) u Hu.
Apply tuple_2_setprod to the current goal.
We will prove u 0 + - 1 ∈ int.
Apply int_add_SNo to the current goal.
An exact proof term for the current goal is Lu0.
We will prove - 1 ∈ int.
Apply int_minus_SNo to the current goal.
An exact proof term for the current goal is nat_p_int 1 nat_1.
We will prove u 1 ∈ X.
An exact proof term for the current goal is Lu1.
Apply omega_iterate_ext (int ⨯ X) (0,u 1) (tuple_2_setprod int X 0 (nat_p_int 0 nat_0) (u 1) Lu1) (λu ⇒ (u 0 + - 1,u 1)) (inv (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) to the current goal.
An exact proof term for the current goal is L7.
We will prove ∀u ∈ int ⨯ X, (u 0 + - 1,u 1) = inv (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) u.
Let u be given.
Assume Hu.
We prove the intermediate claim Lu0: u 0 ∈ int.
An exact proof term for the current goal is ap0_lam int (λ_ ⇒ X) u Hu.
We prove the intermediate claim Lu1: u 1 ∈ X.
An exact proof term for the current goal is ap1_lam int (λ_ ⇒ X) u Hu.
Set g to be the term λu ⇒ (u 0 + 1,u 1) of type set → set.
We will prove (u 0 + - 1,u 1) = inv (int ⨯ X) g u.
Apply bijE (int ⨯ X) (int ⨯ X) g (L1b X) to the current goal.
Assume _ H3 H4.
Apply H3 to the current goal.
We will prove (u 0 + - 1,u 1) ∈ int ⨯ X.
An exact proof term for the current goal is L7 u Hu.
We will prove inv (int ⨯ X) g u ∈ int ⨯ X.
Apply bijE (int ⨯ X) (int ⨯ X) (inv (int ⨯ X) g) (bij_inv (int ⨯ X) (int ⨯ X) g (L1b X)) to the current goal.
Assume H5 _ _.
An exact proof term for the current goal is H5 u Hu.
We will prove ((u 0 + - 1,u 1) 0 + 1,(u 0 + - 1,u 1) 1) = g (inv (int ⨯ X) g u).
rewrite the current goal using tuple_2_0_eq (from left to right).
rewrite the current goal using tuple_2_1_eq (from left to right).
We will prove ((u 0 + - 1) + 1,u 1) = g (inv (int ⨯ X) g u).
rewrite the current goal using add_SNo_minus_R2' (u 0) 1 (int_SNo (u 0) Lu0) SNo_1 (from left to right).
We will prove (u 0,u 1) = g (inv (int ⨯ X) g u).
rewrite the current goal using tuple_lam_eta int (λ_ ⇒ X) u Hu (from left to right).
We will prove u = g (inv (int ⨯ X) g u).
Use symmetry.
Apply surj_rinv (int ⨯ X) (int ⨯ X) g H4 u Hu to the current goal.
Assume _ H5.
An exact proof term for the current goal is H5.
We will prove nat_p (- u 0).
An exact proof term for the current goal is omega_nat_p (- u 0) H2.
We will prove omega_iterate (- u 0) (λu ⇒ (u 0 + - 1,u 1)) (0,u 1) = (u 0,u 1).
rewrite the current goal using omega_iterate_pair_countback1 (u 1) (- u 0) (omega_nat_p (- u 0) H2) (from left to right).
We will prove (- - u 0,u 1) = (u 0,u 1).
rewrite the current goal using minus_SNo_invol (u 0) (int_SNo (u 0) Lu0) (from left to right).
Use reflexivity.
Assume H1: 0 <= u 0.
Assume H2: ¬ (u 0 < 0).
Assume H3: u 0 ∈ omega.
rewrite the current goal using If_i_0 (u 0 < 0) (omega_iterate (- u 0) (inv (int ⨯ X) (λu ⇒ (u 0 + 1,u 1))) (0,u 1)) (omega_iterate (u 0) (λu ⇒ (u 0 + 1,u 1)) (0,u 1)) H2 (from left to right).
We will prove omega_iterate (u 0) (λu ⇒ (u 0 + 1,u 1)) (0,u 1) = (u 0,u 1).
Use transitivity with and omega_iterate (u 0) (λu ⇒ (ordsucc (u 0),u 1)) (0,u 1).
We will prove omega_iterate (u 0) (λu ⇒ (u 0 + 1,u 1)) (0,u 1) = omega_iterate (u 0) (λu ⇒ (ordsucc (u 0),u 1)) (0,u 1).
Use symmetry.
Apply omega_iterate_ext (omega ⨯ X) (0,u 1) (tuple_2_setprod omega X 0 (nat_p_omega 0 nat_0) (u 1) Lu1) (λu ⇒ (ordsucc (u 0),u 1)) (λu ⇒ (u 0 + 1,u 1)) to the current goal.
We will prove ∀u ∈ omega ⨯ X, (ordsucc (u 0),u 1) ∈ omega ⨯ X.
Let u be given.
Assume Hu.
Apply tuple_2_setprod omega X to the current goal.
We will prove ordsucc (u 0) ∈ omega.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is ap0_lam omega (λ_ ⇒ X) u Hu.
We will prove u 1 ∈ X.
An exact proof term for the current goal is ap1_lam omega (λ_ ⇒ X) u Hu.
We will prove ∀u ∈ omega ⨯ X, (ordsucc (u 0),u 1) = (u 0 + 1,u 1).
Let u be given.
Assume Hu.
We prove the intermediate claim Lu0o: ordinal (u 0).
An exact proof term for the current goal is nat_p_ordinal (u 0) (omega_nat_p (u 0) (ap0_lam omega (λ_ ⇒ X) u Hu)).
rewrite the current goal using ordinal_ordsucc_SNo_eq (u 0) Lu0o (from left to right).
We will prove (1 + u 0,u 1) = (u 0 + 1,u 1).
rewrite the current goal using add_SNo_com 1 (u 0) SNo_1 (ordinal_SNo (u 0) Lu0o) (from left to right).
Use reflexivity.
We will prove nat_p (u 0).
An exact proof term for the current goal is omega_nat_p (u 0) H3.
An exact proof term for the current goal is omega_iterate_pair_count1 (u 1) (u 0) (omega_nat_p (u 0) H3).
We will prove (u 0,u 1) = u.
An exact proof term for the current goal is tuple_lam_eta int (λ_ ⇒ X) u Hu.
Let A be given.
Assume HA.
Apply HA to the current goal.
Assume HAs.
Apply HAs to the current goal.
Let X and h be given.
Assume Hh: ∀x ∈ X, h x ∈ X.
We will prove unpack_u_o (pack_u X h) Phi → lam_comp (pack_u X h 0) (eps (pack_u X h)) (eta (pack_u X h 0)) = lam_id (pack_u X h 0).
rewrite the current goal using pack_u_0_eq2 (from right to left).
rewrite the current goal using unpack_u_o_eq Phi X h (L2 X h) (from left to right).
Assume Hh2: bij X X h.
We will prove (λx ∈ X ⇒ eps (pack_u X h) (eta X x)) = (λx ∈ X ⇒ x).
Apply lam_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We will prove eps (pack_u X h) (eta X x) = x.
Use transitivity with eps (pack_u X h) (0,x), and omega_iterate 0 h x.
Use f_equal.
An exact proof term for the current goal is Letabeta X x Hx.
We will prove eps (pack_u X h) (0,x) = omega_iterate 0 h x.
An exact proof term for the current goal is Lepsbetanonneg X h Hh2 0 (nat_p_omega 0 nat_0) x Hx.
We will prove omega_iterate 0 h x = x.
Apply omega_iterate_0 to the current goal.
∎