Require Import basic ZF ZFpairs ZFsum ZFrelations.
Require Import ZFcont.
Require Import ZFord ZFfix ZFfunext ZFfixrec.
Require Import ZFfixfun.

Record iso_fun X Y f : Prop := {
  iso_funm : ext_fun X f;
  iso_typ : typ_fun f X Y;
  iso_inj : ∀ x x', x ∈ X -> x' ∈ X -> f x == f x' -> x == x';
  iso_surj : ∀ y, y ∈ Y -> exists2 x, x ∈ X & f x == y
}.

Lemma iso_fun_morph : ∀ X X' Y Y' f f',
  X == X' ->
  Y == Y' ->
  eq_fun X f f' ->
  iso_fun X Y f -> iso_fun X' Y' f'.

Lemma iso_change_rhs : ∀ X Y Y' f,
  Y == Y' ->
  iso_fun X Y f ->
  iso_fun X Y' f.

Lemma eq_iso_fun : ∀ X Y f, X == Y -> (∀ x, x ∈ X -> f x == x) ->
  iso_fun X Y f.

Lemma id_iso_fun : ∀ X, iso_fun X X (fun x => x).

Definition iso_inv X f y := union (subset X (fun x => f x == y)).

Instance iso_inv_morph0 : ∀ A f, morph1 (iso_inv A f).


Qed.

Lemma iso_inv_ext A A' f f' x x' :
  A == A' ->
  eq_fun A f f' ->
  x == x' ->
  iso_inv A f x == iso_inv A' f' x'.

Instance iso_inv_morph : Proper (eq_set ==> (eq_set ==> eq_set) ==> eq_set ==> eq_set) iso_inv.
Qed.

Lemma iso_inv_eq : ∀ X Y f y,
   iso_fun X Y f -> y ∈ Y -> f (iso_inv X f y) == y.

Lemma iso_inv_eq2 : ∀ X Y f x,
   iso_fun X Y f -> x ∈ X -> iso_inv X f (f x) == x.

Lemma iso_inv_typ : ∀ X Y f y,
   iso_fun X Y f -> y ∈ Y -> iso_inv X f y ∈ X.

Lemma iso_fun_sym : ∀ X Y f, iso_fun X Y f -> iso_fun Y X (iso_inv X f).

Lemma iso_fun_trans_eq : ∀ X Y Z f g h,
  (∀ x, x ∈ X -> g (f x) == h x) ->
  iso_fun X Y f ->
  iso_fun Y Z g ->
  iso_fun X Z h.

Definition comp_iso (f:set->set) (g:set->set) := fun x => g (f x).

Lemma iso_fun_trans : ∀ X Y Z f g, iso_fun X Y f -> iso_fun Y Z g ->
  iso_fun X Z (comp_iso f g).

Lemma comp_iso_morph : Proper ((eq_set ==> eq_set) ==> (eq_set ==> eq_set) ==> eq_set ==> eq_set) comp_iso.

Lemma comp_iso_eq_fun : ∀ A B f f' g g',
  (∀ x, x ∈ A -> f x ∈ B) ->
  eq_fun A f f' ->
  eq_fun B g g' ->
  eq_fun A (comp_iso f g) (comp_iso f' g').

Lemma comp_iso_typ X Y Z f g :
  typ_fun f X Y ->
  typ_fun g Y Z ->
  typ_fun (comp_iso f g) X Z.

Lemma iso_intro : ∀ X Y f g,
  ext_fun X f ->
  (∀ x, x ∈ X -> f x ∈ Y /\ g (f x) == x) ->
  (∀ y y', y ∈ Y -> y == y' -> g y == g y' /\ g y ∈ X /\ f (g y) == y) ->
  iso_fun X Y f.

Lemma iso_fun_inj X1 X2 Y f :
  iso_fun X1 Y f ->
  iso_fun X2 Y f ->
  X1 ⊆ X2 ->
  X1 == X2.

Lemma iso_fun_narrow X1 X2 Y1 Y2 f x :
  iso_fun X1 Y1 f ->
  iso_fun X2 Y2 f ->
  X1 ⊆ X2 ->
  x ∈ X2 ->
  f x ∈ Y1 ->
  x ∈ X1.

Definition sum_isomap f g :=
  sum_case (fun x => inl (f x)) (fun y => inr (g y)).

Lemma sum_isomap_morph : Proper ((eq_set ==> eq_set) ==> (eq_set ==> eq_set) ==> eq_set ==> eq_set) sum_isomap.

Lemma sum_isomap_ext : ∀ A B f f' g g',
  eq_fun A f f' ->
  eq_fun B g g' ->
  eq_fun (sum A B) (sum_isomap f g) (sum_isomap f' g').

Lemma sum_isomap_typ X X' Y Y' f g :
  typ_fun f X X' ->
  typ_fun g Y Y' ->
  typ_fun (sum_isomap f g) (sum X Y) (sum X' Y').

Lemma sum_iso_fun_morph : ∀ X X' Y Y' f g,
  iso_fun X X' f -> iso_fun Y Y' g ->
  iso_fun (sum X Y) (sum X' Y') (sum_isomap f g).

Definition sum_isocomm := sum_case inr inl.

Instance sum_isocomm_morph : morph1 sum_isocomm.
Qed.

Lemma sum_isocomm_typ X Y:
  typ_fun sum_isocomm (sum X Y) (sum Y X).

Lemma sum_isocomm_invol : ∀ X Y x,
  x ∈ sum X Y -> sum_isocomm (sum_isocomm x) == x.

Lemma sum_comm_iso_fun :
  ∀ X Y, iso_fun (sum X Y) (sum Y X) sum_isocomm.

Definition sum_isoassoc :=
  sum_case (sum_case inl (fun y => inr (inl y))) (fun z => inr (inr z)).

Instance sum_isoassoc_morph : morph1 sum_isoassoc.


Qed.

Instance inlr_morph : morph1 (fun y => inr (inl y)).
Qed.

Instance inrr_morph : morph1 (fun y => inr (inr y)).
Qed.

Instance sclr_morph : morph1 (sum_case inl (fun y => inr (inl y))).
Qed.

Lemma sum_isoassoc_typ : ∀ X Y Z,
  typ_fun sum_isoassoc (sum (sum X Y) Z) (sum X (sum Y Z)).

Lemma sum_assoc_iso_fun :
  ∀ X Y Z, iso_fun (sum (sum X Y) Z) (sum X (sum Y Z)) sum_isoassoc.

Definition sigma_isomap f g :=
  fun p => couple (f (fst p)) (g (fst p) (snd p)).

Instance sigma_isomap_morph :
  Proper ((eq_set ==> eq_set) ==> (eq_set ==> eq_set ==> eq_set) ==> eq_set ==> eq_set) sigma_isomap.

Qed.

Lemma sigma_isomap_ext A B f f' g g' :
  ext_fun A B ->
  eq_fun A f f' ->
  (∀ x x' y y', x ∈ A -> x == x' -> y ∈ B x -> y == y' -> g x y == g' x' y') ->
  eq_fun (sigma A B) (sigma_isomap f g) (sigma_isomap f' g').

Lemma sigma_isomap_typ A A' B B' f g :
  ext_fun A B ->
  ext_fun A' B' ->
  typ_fun f A A' ->
  (∀ x, x ∈ A -> typ_fun (g x) (B x) (B' (f x))) ->
  typ_fun (sigma_isomap f g) (sigma A B) (sigma A' B').

Lemma sigma_iso_fun_morph : ∀ A A' B B' f g,
  ext_fun A B ->
  ext_fun A' B' ->
  ext_fun2 A B g ->
  iso_fun A A' f ->
  (∀ x x', x ∈ A -> f x == x' -> iso_fun (B x) (B' x') (g x)) ->
  iso_fun (sigma A B) (sigma A' B') (sigma_isomap f g).

Lemma sigma_iso_fun_1_l : ∀ x F,
  ext_fun (singl x) F ->
  iso_fun (sigma (singl x) F) (F x) snd.

Lemma sigma_iso_fun_1_l' : ∀ x F,
  ext_fun (singl x) F ->
  iso_fun (F x) (sigma (singl x) F) (couple x).

Lemma sigma_iso_fun_1_r : ∀ A B,
  ext_fun A B ->
  (∀ x, x ∈ A -> iso_fun (B x) (singl empty) (fun _ => empty)) ->
  iso_fun (sigma A B) A fst.

Definition sigma_1r_iso f x := couple x (f x).

Lemma sigma_1r_iso_typ A B f :
  ext_fun A B ->
  (∀ x, x ∈ A -> f x ∈ B x) ->
  typ_fun (sigma_1r_iso f) A (sigma A B).

Lemma sigma_iso_fun_1_r' : ∀ A B f,
  ext_fun A B ->
  ext_fun A f ->
  (∀ x, x ∈ A -> iso_fun (singl empty) (B x) (fun _ => f x)) ->
  iso_fun A (sigma A B) (sigma_1r_iso f).

Definition sigma_isoassoc :=
  fun t => couple (couple (fst t) (fst (snd t))) (snd (snd t)).

Instance sigma_isoassoc_morph : morph1 sigma_isoassoc.
Qed.

Lemma sigma_isoassoc_typ A B C :
  ext_fun A B ->
  ext_fun2 A B C ->
  typ_fun sigma_isoassoc
    (sigma A (fun x => sigma (B x) (fun y => C x y)))
    (sigma (sigma A B) (fun p => C (fst p) (snd p))).

Lemma iso_sigma_sigma : ∀ A B C,
  ext_fun A B ->
  ext_fun2 A B C ->
  iso_fun (sigma A (fun x => sigma (B x) (fun y => C x y)))
          (sigma (sigma A B) (fun p => C (fst p) (snd p)))
          sigma_isoassoc.

Definition sum_sigma_iso :=
  sum_case (fun p1 => couple (inl (fst p1)) (snd p1))
           (fun p2 => couple (inr (fst p2)) (snd p2)).

Instance sum_sigma_iso_morph : morph1 sum_sigma_iso.

Qed.

Instance cpl_inl_morph : morph1 (fun p1 => couple (inl (fst p1)) (snd p1)).
Qed.
Instance cpl_inr_morph : morph1 (fun p2 => couple (inr (fst p2)) (snd p2)).
Qed.

Lemma sum_sigma_iso_typ A1 A2 B1 B2 :
  ext_fun A1 B1 ->
  ext_fun A2 B2 ->
  typ_fun sum_sigma_iso
    (sum (sigma A1 B1) (sigma A2 B2))
    (sigma (sum A1 A2) (sum_case B1 B2)).

Lemma iso_fun_sum_sigma : ∀ A1 A2 B1 B2,
  ext_fun A1 B1 ->
  ext_fun A2 B2 ->
  iso_fun (sum (sigma A1 B1) (sigma A2 B2))
          (sigma (sum A1 A2) (sum_case B1 B2))
          sum_sigma_iso.

Lemma prodcart_iso_fun_morph : ∀ X X' Y Y' f g,
  iso_fun X X' f -> iso_fun Y Y' g ->
  iso_fun (prodcart X Y) (prodcart X' Y') (sigma_isomap f (fun _ => g)).

Lemma sigma_isomap_typ_prod A A' B B' f g :
  typ_fun f A A' ->
  typ_fun g B B' ->
  typ_fun (sigma_isomap f (fun _ => g)) (prodcart A B) (prodcart A' B').

Lemma prodcart_comm_iso_fun :
  ∀ X Y, iso_fun (prodcart X Y) (prodcart Y X) (fun p => couple (snd p) (fst p)).


Definition prodcart_sigma_iso q :=
  couple (couple (fst (fst q)) (fst (snd q)))
         (couple (snd (fst q)) (snd (snd q))).

Lemma prodcart_sigma_iso_typ A1 A2 B1 B2 :
  ext_fun A1 B1 ->
  ext_fun A2 B2 ->
  typ_fun prodcart_sigma_iso
    (prodcart (sigma A1 B1) (sigma A2 B2))
    (sigma (prodcart A1 A2) (fun p => prodcart (B1 (fst p)) (B2 (snd p)))).

Lemma iso_fun_prodcart_sigma : ∀ A1 A2 B1 B2,
  ext_fun A1 B1 ->
  ext_fun A2 B2 ->
  iso_fun (prodcart (sigma A1 B1) (sigma A2 B2))
    (sigma (prodcart A1 A2) (fun p => prodcart (B1 (fst p)) (B2 (snd p))))
    prodcart_sigma_iso.

Definition cc_prod_isomap A' f g :=
  fun fct => cc_lam A' (fun x' => g (f x') (cc_app fct (f x'))).

Instance cc_prod_isomap_morph :
  Proper (eq_set ==> (eq_set ==> eq_set) ==> (eq_set ==> eq_set ==> eq_set) ==> eq_set ==> eq_set) cc_prod_isomap.
Qed.

Lemma cc_prod_isomap_ext A B A' A'' f f' g g' :
  A' == A'' ->
  ext_fun A B ->
  eq_fun A' f f' ->
  typ_fun f A' A ->
  (∀ x x' y y', x ∈ A' -> x == x' -> y ∈ B (f x) -> y == y' ->
   g (f x) y == g' (f' x') y') ->
  eq_fun (cc_prod A B) (cc_prod_isomap A' f g) (cc_prod_isomap A'' f' g').

Lemma cc_prod_isomap_typ A A' B B' f g :
  ext_fun A' B' ->
  ext_fun A' f ->
  ext_fun2 A B g ->
  typ_fun f A' A ->
  (∀ x, x ∈ A' -> typ_fun (g (f x)) (B (f x)) (B' x)) ->
  typ_fun (cc_prod_isomap A' f g) (cc_prod A B) (cc_prod A' B').

Lemma cc_prod_iso_fun_morph : ∀ A A' B B' f g,
  ext_fun A B ->
  ext_fun A' B' ->
  ext_fun2 A B g ->
  iso_fun A' A f ->
  (∀ x, x ∈ A' -> iso_fun (B (f x)) (B' x) (g (f x))) ->
  iso_fun (cc_prod A B) (cc_prod A' B') (cc_prod_isomap A' f g).

Lemma cc_prod_iso_fun_0_l : ∀ a F,
  iso_fun (cc_prod empty F) (singl a) (fun _ => a).

Lemma cc_prod_iso_fun_0_l' : ∀ a F,
  iso_fun (singl a) (cc_prod empty F) (fun _ => cc_lam empty (fun _ => empty)).

Definition cc_prod_iso1l x := fun f => cc_app f x.

Lemma cc_prod_iso_fun_1_l : ∀ x F,
  (∀ x', x == x' -> F x == F x') ->
  iso_fun (cc_prod (singl x) F) (F x) (cc_prod_iso1l x).

Lemma cc_prod_iso_fun_1_l' : ∀ x F,
  (∀ x', x == x' -> F x == F x') ->
  iso_fun (F x) (cc_prod (singl x) F) (fun y => cc_lam (singl x) (fun _ => y)).

Lemma cc_prod_iso_fun_1_r : ∀ A F,
  ext_fun A F ->
  (∀ x, x ∈ A -> iso_fun (F x) (singl empty) (fun _ => empty)) ->
  iso_fun (cc_prod A F) (singl empty) (fun _ => empty).

Definition cc_prod_isocurry A B :=
  fun f2 => cc_lam (sigma A B) (fun p => cc_app (cc_app f2 (fst p)) (snd p)).

Lemma cc_prod_isocurry_typ A B C :
  ext_fun A B ->
  ext_fun2 A B C ->
  typ_fun (cc_prod_isocurry A B)
    (cc_prod A (fun x => cc_prod (B x) (fun y => C x y)))
    (cc_prod (sigma A B) (fun p => C (fst p) (snd p))).

Lemma cc_prod_curry_iso_fun : ∀ A B C,
  ext_fun A B ->
  ext_fun2 A B C ->
  iso_fun (cc_prod A (fun x => cc_prod (B x) (fun y => C x y)))
    (cc_prod (sigma A B) (fun p => C (fst p) (snd p)))
    (cc_prod_isocurry A B).

Definition cc_prod_sigma_iso A :=
  fun fct => couple (cc_lam A (fun x => fst (cc_app fct x)))
                    (cc_lam A (fun x => snd (cc_app fct x))).

Lemma cc_prod_sigma_iso_typ A B C :
  ext_fun A B ->
  ext_fun2 A B C ->
  typ_fun (cc_prod_sigma_iso A)
    (cc_prod A (fun x => sigma (B x) (fun y => C x y)))
    (sigma (cc_prod A B) (fun f => cc_prod A (fun x => C x (cc_app f x)))).

Instance cc_prod_sigma_iso_morph : morph2 cc_prod_sigma_iso.

Qed.

Lemma iso_fun_cc_prod_sigma : ∀ A B C,
  ext_fun A B ->
  ext_fun2 A B C ->
  iso_fun (cc_prod A (fun x => sigma (B x) (fun y => C x y)))
    (sigma (cc_prod A B) (fun f => cc_prod A (fun x => C x (cc_app f x))))
    (cc_prod_sigma_iso A).

Definition prodcart_cc_prod_iso D :=
  fun p => cc_lam D (sum_case (cc_app (fst p)) (cc_app (snd p))).

Instance prodcart_cc_prod_iso_morph : morph2 prodcart_cc_prod_iso.

Qed.

Lemma prodcart_cc_prod_iso_typ A1 A2 F1 F2 :
  ext_fun A1 F1 ->
  ext_fun A2 F2 ->
  typ_fun (prodcart_cc_prod_iso (sum A1 A2))
    (prodcart (cc_prod A1 F1) (cc_prod A2 F2))
    (cc_prod (sum A1 A2) (sum_case F1 F2)).

Lemma iso_fun_prodcart_cc_prod : ∀ A1 A2 F1 F2,
  ext_fun A1 F1 ->
  ext_fun A2 F2 ->
  iso_fun (prodcart (cc_prod A1 F1) (cc_prod A2 F2))
    (cc_prod (sum A1 A2) (sum_case F1 F2))
    (prodcart_cc_prod_iso (sum A1 A2)).

Section TI_iso.

  Definition TI_iso F g o :=
    cc_app (REC (fun o f => cc_lam (F (TI F o)) (g (cc_app f))) o).

Lemma iso_cont : ∀ F G o f,
  Proper (incl_set ==> incl_set) F ->
  Proper (incl_set ==> incl_set) G ->
  isOrd o ->
  (∀ o', o' ∈ o -> iso_fun (TI F (osucc o')) (TI G (osucc o')) f) ->
  iso_fun (TI F o) (TI G o) f.

  Variable F G : set -> set.
  Variable g : (set -> set) -> set -> set.
  Variable o : set.
  Hypothesis Fmono : Proper (incl_set ==> incl_set) F.
  Hypothesis Gmono : Proper (incl_set ==> incl_set) G.
  Hypothesis gext : ∀ X f f', eq_fun X f f' -> eq_fun (F X) (g f) (g f').
  Hypothesis isog' : ∀ o f, isOrd o ->
    iso_fun (TI F o) (TI G o) f -> iso_fun (F (TI F o)) (G (TI G o)) (g f).
  Hypothesis oord : isOrd o.

  Let Fm := Fmono_morph _ Fmono.
  Let Gm := Fmono_morph _ Gmono.
  Let egf : ∀ o' f, isOrd o' -> ext_fun (F (TI F o')) (g (cc_app f)).
Qed.

  Lemma TI_iso_recursor :
    recursor o (TI F)
      (fun o f => iso_fun (TI F o) (TI G o) (cc_app f))
      (fun o f => cc_lam (F (TI F o)) (g (cc_app f))).

  Lemma TI_iso_fun :
    iso_fun (TI F o) (TI G o) (TI_iso F g o) /\
    (∀ x, x ∈ TI F o -> TI_iso F g o x == g (TI_iso F g o) x).

  Lemma TI_iso_irrel o' o'' :
    isOrd o' ->
    isOrd o'' ->
    o' ⊆ o'' ->
    o'' ⊆ o ->
    eq_fun (TI F o') (TI_iso F g o') (TI_iso F g o'').

  Lemma TI_iso_fixpoint :
    TI F o == F (TI F o) <-> TI G o == G (TI G o).

End TI_iso.

Section TIF_iso.

  Variable A : set.
  Variable F G : (set -> set) -> set -> set.
  Hypothesis Fm : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) F.
  Hypothesis Gm : Proper ((eq_set==>eq_set)==>eq_set==>eq_set) G.
  Hypothesis Fmono : mono_fam A F.
  Hypothesis Gmono : mono_fam A G.

Lemma TIF_iso_cont : ∀ o f,
  isOrd o ->
  (∀ a o', a ∈ A -> o' ∈ o ->
   iso_fun (TIF A F (osucc o') a) (TIF A G (osucc o') a) (f a)) ->
  ∀ a, a ∈ A -> iso_fun (TIF A F o a) (TIF A G o a) (f a).

  Let fmrph g f o :
    isOrd o ->
    Proper ((eq_set==>eq_set==>eq_set)==>eq_set==>eq_set==>eq_set) g ->
    ext_fun (sigma A (fun a' => TIF A F (osucc o) a'))
     (fun p => g (fun x y => cc_app f (couple x y)) (fst p) (snd p)).
Qed.

  Definition TIF_iso g o a x :=
    cc_app (REC (fun o f =>
         cc_lam (sigma A (fun a' => TIF A F (osucc o) a'))
              (fun p => g (fun x y => cc_app f (couple x y)) (fst p) (snd p))) o)
      (couple a x).

  Variable g : (set -> set -> set) -> set -> set -> set.
  Hypothesis gm : Proper ((eq_set==>eq_set==>eq_set)==>eq_set==>eq_set==>eq_set) g.
  Hypothesis gext :
     ∀ X f f', morph1 X -> morph2 f -> morph2 f' ->
     (∀ a, a ∈ A -> eq_fun (X a) (f a) (f' a)) ->
     ∀ a, a ∈ A -> eq_fun (F X a) (g f a) (g f' a).
  Hypothesis isog :
     ∀ X Y f, morph1 X -> morph1 Y -> morph2 f ->
     (∀ a, a ∈ A -> iso_fun (X a) (Y a) (f a)) ->
      ∀ a, a ∈ A -> iso_fun (F X a) (G Y a) (g f a).

  Variable o : set.
  Variable oo : isOrd o.

  Lemma TIF_iso_recursor :
    recursor o (fun o => sigma A (fun a' => TIF A F o a'))
      (fun o f => ∀ a, a ∈ A -> iso_fun (TIF A F o a) (TIF A G o a) (fun x => cc_app f (couple a x)))
      (fun o f => cc_lam (sigma A (fun a' => TIF A F (osucc o) a'))
            (fun p => g (fun x y => cc_app f (couple x y)) (fst p) (snd p))).

  Lemma TIF_iso_fun :
    ∀ a, a ∈ A ->
    iso_fun (TIF A F o a) (TIF A G o a) (TIF_iso g o a) /\
    (∀ x, x ∈ TIF A F o a -> TIF_iso g o a x == g (TIF_iso g o) a x).

End TIF_iso.