(*
 * Copyright (c) 2009-2010, Andrew Appel, Robert Dockins and Aquinas Hobor.
 *
 *)

Require Import VST.msl.base.
Require Import VST.msl.ageable.
Require Import VST.msl.knot.
Require Import VST.msl.knot_lemmas.
Require Import VST.msl.functors.

Import CovariantFunctor.
Import CovariantFunctorLemmas.
Import CovariantFunctorGenerator.

Local Open Scope nat_scope.

Definition map_pair {A B C D} (f:A -> B) (g:C -> D) (x:A * C) : B * D :=
  (f (fst x), g (snd x)).

Module Type ISOMORPHIC_KNOTS.
  Declare Module TF : TY_FUNCTOR.
  Declare Module K1 : KNOT with Module TF := TF.
  Declare Module K2 : KNOT with Module TF := TF.
  Import TF.

  Parameter f : K1.knot -> K2.knot.
  Parameter g : K2.knot -> K1.knot.

  Definition fF : F K1.predicate -> F K2.predicate :=
    fmap F (fun p : K1.knot * other -> K1.TF.T => p oo map_pair g (@id other)).

  Definition gF : F K2.predicate -> F K1.predicate :=
    fmap F (fun p : K2.knot * other -> K2.TF.T => p oo map_pair f (@id other)).

  Axiom iso1 : f oo g = id K2.knot.
  Axiom iso2 : g oo f = id K1.knot.

  Axiom f_squash : forall n F1,
    f (K1.squash (n, F1)) = K2.squash (n, fF F1).

  Axiom g_squash : forall n F2,
    g (K2.squash (n, F2)) = K1.squash (n, gF F2).

  Axiom f_unsquash : forall k1 U1,
    U1 = K1.unsquash k1 ->
    K2.unsquash (f k1) = (fst U1, fF (snd U1)).

  Axiom g_unsquash : forall k2 U2,
    U2 = K2.unsquash k2 ->
    K1.unsquash (g k2) = (fst U2, gF (snd U2)).

End ISOMORPHIC_KNOTS.

Module Unique_Knot (TF' : TY_FUNCTOR)
                                (K1' : KNOT with Module TF := TF')
                                (K2' : KNOT with Module TF := TF') :
                                  ISOMORPHIC_KNOTS
                                    with Module TF := TF'
                                    with Module K1 := K1'
                                    with Module K2 := K2'.
Module TF := TF'.
Import TF.
Module K1 := K1'.
Module K2 := K2'.
Module K1L := Knot_Lemmas K1.
Module K2L := Knot_Lemmas K2.

Section Common.
Variable f : K1.knot -> K2.knot.
Variable g : K2.knot -> K1.knot.

Definition f_pred' (p1 : K1.predicate) : K2.predicate :=
  p1 oo map_pair g (@id other).

Definition g_pred' (p2 : K2.predicate) : K1.predicate :=
  p2 oo map_pair f (@id other).

Variable f_level : forall k, level k = level (f k).
Variable g_level : forall k, level k = level (g k).

Lemma f_pred'_approx: forall n,
f_pred' oo K1.approx n = K2.approx n oo f_pred'.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: None *)
extensionality P1 k2.
(* Goal: @eq K2.TF.T (@compose K1.predicate K1.predicate K2.predicate f_pred' (K1.approx n) P1 k2) (@compose K1.predicate K2.predicate K2.predicate (K2.approx n) f_pred' P1 k2) *)
destruct k2; unfold f_pred', compose; simpl.
(* Goal: @eq K1.TF.T (K2.approx n P (@map_pair K1.knot K2.knot other other f (id other) (@pair K1.knot K1.TF.other k o))) (K1.approx n (fun x : prod K1.knot other => P (@map_pair K1.knot K2.knot other other f (id other) x)) (@pair K1.knot K1.TF.other k o)) *)
unfold K1'.approx, K2'.approx; simpl.
(* Goal: @eq K2.TF.T (if le_gt_dec n (@level K1.knot K1.ag_knot (g k)) then K1.TF.T_bot else P1 (@map_pair K2.knot K1.knot other other g (id other) (@pair K2.knot K2.TF.other k o))) (if le_gt_dec n (@level K2.knot K2.ag_knot k) then K2.TF.T_bot else P1 (@map_pair K2.knot K1.knot other other g (id other) (@pair K2.knot K2.TF.other k o))) *)
rewrite g_level; simpl; auto.
Qed.

Lemma g_pred'_approx : forall n,
g_pred' oo K2.approx n = K1.approx n oo g_pred'.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : K2.predicate, K1.predicate) (@compose K2.predicate K2.predicate K1.predicate g_pred' (K2.approx n)) (@compose K2.predicate K1.predicate K1.predicate (K1.approx n) g_pred') *)
extensionality P k1.
(* Goal: @eq K1.TF.T (@compose K2.predicate K2.predicate K1.predicate g_pred' (K2.approx n) P k1) (@compose K2.predicate K1.predicate K1.predicate (K1.approx n) g_pred' P k1) *)
destruct k1; unfold g_pred', compose; simpl.
(* Goal: @eq K1.TF.T (K2.approx n P (@map_pair K1.knot K2.knot other other f (id other) (@pair K1.knot K1.TF.other k o))) (K1.approx n (fun x : prod K1.knot other => P (@map_pair K1.knot K2.knot other other f (id other) x)) (@pair K1.knot K1.TF.other k o)) *)
unfold K1'.approx, K2'.approx; simpl.
(* Goal: @eq K1.TF.T (if le_gt_dec n (@level K2.knot K2.ag_knot (f k)) then K2.TF.T_bot else P (@map_pair K1.knot K2.knot other other f (id other) (@pair K1.knot K1.TF.other k o))) (if le_gt_dec n (@level K1.knot K1.ag_knot k) then K1.TF.T_bot else P (@map_pair K1.knot K2.knot other other f (id other) (@pair K1.knot K1.TF.other k o))) *)
rewrite f_level; simpl; auto.
Qed.

Definition f_F' : TF.F K1.predicate -> TF.F K2.predicate :=
  fmap F f_pred'.

Definition g_F' : TF.F K2.predicate -> TF.F K1.predicate :=
  fmap F g_pred'.

End Common.

Section Z.
(* The base case.  To keep things simple, we will put definitions first. *)

Definition fZ_pred (p2 : K2.predicate) : K1.predicate :=
fun k1 => T_bot.

Definition gZ_pred (p1 : K1.predicate) : K2.predicate :=
fun k2 => T_bot.

Definition fF_Z : TF.F K1.predicate -> TF.F K2.predicate :=
  fmap F gZ_pred.

Definition gF_Z : TF.F K2.predicate -> TF.F K1.predicate :=
  fmap F fZ_pred.

Definition f_Z (k1 : K1.knot) : K2.knot :=
  match K1.unsquash k1 with
    (n, F_p1) => K2.squash (n, fF_Z F_p1)
  end.

Definition g_Z (k2 : K2.knot) : K1.knot :=
  match K2.unsquash k2 with
    (n, F_p2) => K1.squash (n, gF_Z F_p2)
  end.

(* Now the lemmas *)
Lemma predZ_iso1: fZ_pred oo K2.approx 0 oo gZ_pred = K1.approx 0.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : K2.predicate, K2.predicate) (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx m) (g_pred' f))) (K2.approx m) *)
extensionality p k.
(* Goal: @eq K1.TF.T (@compose K1.predicate K2.predicate K1.predicate fZ_pred (@compose K1.predicate K2.predicate K2.predicate (K2.approx O) gZ_pred) p k) (K1.approx O p k) *)
unfold compose, gZ_pred, fZ_pred, K1'.approx in *.
(* Goal: @eq K2.TF.T T_bot (if le_gt_dec O (@level (prod K2.knot K2.TF.other) (ag_prod K2.knot K2.TF.other K2.ag_knot) k) then K2.TF.T_bot else p k) *)
destruct k; simpl; auto.
Qed.

Lemma predZ_iso2: gZ_pred oo K1.approx 0 oo fZ_pred = K2.approx 0.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : K2.predicate, K2.predicate) (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx m) (g_pred' f))) (K2.approx m) *)
extensionality p k.
(* Goal: @eq K2.TF.T (@compose K2.predicate K1.predicate K2.predicate gZ_pred (@compose K2.predicate K1.predicate K1.predicate (K1.approx O) fZ_pred) p k) (K2.approx O p k) *)
unfold compose, gZ_pred, fZ_pred, K2'.approx in *.
(* Goal: @eq K2.TF.T T_bot (if le_gt_dec O (@level (prod K2.knot K2.TF.other) (ag_prod K2.knot K2.TF.other K2.ag_knot) k) then K2.TF.T_bot else p k) *)
destruct k; simpl; auto.
Qed.

Lemma iso1_Z : forall k, level k <= 0 -> (g_Z oo f_Z) k = k.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K2.knot (@compose K2.knot K1.knot K2.knot f_Z g_Z k) k *)
unfold compose, g_Z, f_Z.
(* Goal: @eq K1.knot (let (n, F_p2) := K2.unsquash (let (n, F_p1) := K1.unsquash k in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))) in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) k *)
remember (K1.unsquash k) as unsq_k.
(* Goal: @eq K2.knot (let (n, F_p1) := K1.unsquash (let (n, F_p2) := unsq_k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))) k *)
destruct unsq_k as [n0 Fp].
(* Goal: None *)
rewrite K2.unsquash_squash.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate (@compose K1.predicate K2.predicate K2.predicate (K2.approx m) (f_pred' g)) F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Sn) F1) *)
rewrite K1.knot_level in H.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (f_F' g (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n0) (g_F' f Fp))))) k *)
rewrite <- Hequnsq_k in H.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
replace (fmap F (K2.approx n0) (fF_Z Fp)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (K2.approx n0) oo (fmap F gZ_pred)) Fp) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
replace (gF_Z (fmap F (K2.approx n0 oo gZ_pred) Fp)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F fZ_pred oo fmap F (K2.approx n0 oo gZ_pred)) Fp) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq K1.knot (K1.squash (@pair nat (_functor F K1.predicate) n0 (@fmap F K1.predicate K1.predicate (@compose K1.predicate K2.predicate K1.predicate fZ_pred (@compose K1.predicate K2.predicate K2.predicate (K2.approx n0) gZ_pred)) Fp))) k *)
assert (n0 = 0) by omega.
(* Goal: @eq K1.knot (K1.squash (@pair nat (_functor F K1.predicate) n0 (@fmap F K1.predicate K1.predicate (@compose K1.predicate K2.predicate K1.predicate fZ_pred (@compose K1.predicate K2.predicate K2.predicate (K2.approx n0) gZ_pred)) Fp))) k *)
clear H; subst n0.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (@fmap F K2.predicate K2.predicate (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx n0) (g_pred' f))) Fp))) k *)
symmetry in Hequnsq_k.
(* Goal: @eq K1.knot (K1.squash (@pair nat (_functor F K1.predicate) O (@fmap F K1.predicate K1.predicate (@compose K1.predicate K2.predicate K1.predicate fZ_pred (@compose K1.predicate K2.predicate K2.predicate (K2.approx O) gZ_pred)) Fp))) k *)
rewrite predZ_iso1; trivial.
(* Goal: @eq K1.knot (K1.squash (@pair nat (_functor F K1.predicate) n0 (@fmap F K1.predicate K1.predicate (K1.approx n0) Fp))) k *)
rewrite <- (K1L.unsquash_approx Hequnsq_k).
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 Fp)) k *)
rewrite <- Hequnsq_k.
(* Goal: @eq K1.knot (K1.squash (K1.unsquash k)) k *)
rewrite K1.squash_unsquash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma iso2_Z : forall k, level k <= 0 -> (f_Z oo g_Z) k = k.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K2.knot (@compose K2.knot K1.knot K2.knot f_Z g_Z k) k *)
unfold compose, g_Z, f_Z.
(* Goal: @eq K2.knot (let (n, F_p1) := K1.unsquash (let (n, F_p2) := K2.unsquash k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))) k *)
remember (K2.unsquash k) as unsq_k.
(* Goal: @eq K2.knot (let (n, F_p1) := K1.unsquash (let (n, F_p2) := unsq_k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))) k *)
destruct unsq_k as [n0 Fp].
(* Goal: None *)
rewrite K1.unsquash_squash.
(* Goal: @eq K1.knot (g k) (K1.squash (@pair nat (_functor F K1.predicate) n0 (g_F' f _f))) *)
rewrite K2.knot_level in H.
replace (fmap F (K1.approx n0) (gF_Z Fp)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (K1.approx n0) oo (fmap F fZ_pred)) Fp) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
replace (fF_Z (fmap F (K1.approx n0 oo fZ_pred) Fp)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F gZ_pred oo fmap F (K1.approx n0 oo fZ_pred)) Fp) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (@fmap F K2.predicate K2.predicate (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx n0) (g_pred' f))) Fp))) k *)
symmetry in Hequnsq_k.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (@fmap F K2.predicate K2.predicate (@compose K2.predicate K1.predicate K2.predicate gZ_pred (@compose K2.predicate K1.predicate K1.predicate (K1.approx n0) fZ_pred)) Fp))) k *)
assert (n0 = 0).
(* Goal: @eq nat n0 O *)
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (@fmap F K2.predicate K2.predicate (@compose K2.predicate K1.predicate K2.predicate gZ_pred (@compose K2.predicate K1.predicate K1.predicate (K1.approx n0) fZ_pred)) Fp))) k *)
destruct (K2'.unsquash k); inv Hequnsq_k.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
omega.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (@fmap F K2.predicate K2.predicate (@compose K2.predicate K1.predicate K2.predicate gZ_pred (@compose K2.predicate K1.predicate K1.predicate (K1.approx n0) fZ_pred)) Fp))) k *)
subst n0.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite predZ_iso2; trivial.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (@fmap F K2.predicate K2.predicate (K2.approx n0) Fp))) k *)
rewrite <- (K2L.unsquash_approx Hequnsq_k).
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 Fp)) k *)
rewrite <- Hequnsq_k.
(* Goal: @eq K1.knot (g k) (g (K2.squash (K2.unsquash k))) *)
rewrite K2.squash_unsquash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

(* We must also prove that f_Sn and g_Sn preserve the level property. *)
Lemma f_level_Z: forall k, level k = level (f_Z k).
Proof.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
intro.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k) (@level K2.knot K2.ag_knot (f_Z k)) *)
unfold f_Z.
(* Goal: @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (let (n, F_p2) := K2.unsquash k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2)))) *)
rewrite K1.knot_level, K2.knot_level.
(* Goal: @eq nat (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash k)) (@fst nat (_functor K2.TF.F K2.predicate) (K2.unsquash (let (n, F_p1) := K1.unsquash k in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))))) *)
remember (K1.unsquash k) as uk.
(* Goal: @eq nat (@fst nat (_functor K2.TF.F K2.predicate) uk) (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash (let (n, F_p2) := uk in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))))) *)
destruct uk.
(* Goal: None *)
rewrite K2.unsquash_squash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma g_level_Z: forall k, level k = level (g_Z k).
Proof.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
intro.
(* Goal: @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Z k)) *)
unfold g_Z.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (let (n, F_p2) := K2.unsquash k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2)))) *)
rewrite K1.knot_level, K2.knot_level.
(* Goal: @eq nat (@fst nat (_functor K2.TF.F K2.predicate) (K2.unsquash k)) (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash (let (n, F_p2) := K2.unsquash k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))))) *)
remember (K2.unsquash k) as uk.
(* Goal: @eq nat (@fst nat (_functor K2.TF.F K2.predicate) uk) (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash (let (n, F_p2) := uk in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))))) *)
destruct uk.
(* Goal: None *)
rewrite K1.unsquash_squash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

(* Finally, we must show that fZ preserves unsquashing. *)
Lemma fZ_unsquash : forall k1,
  level k1 <= 0 ->
  forall U1,
  U1 = K1.unsquash k1 ->
  K2.unsquash (f_Z k1) = (fst U1, fF_Z (snd U1)).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f_Z k1)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (fF_Z (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold fF_Z, f_Z.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f k1)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (fF (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
destruct U1 as [n F1].
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S n)) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
rewrite <- H0.
(* Goal: None *)
rewrite K2.unsquash_squash.
replace (fmap F (K2.approx n) (fF_Z F1)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
 ((fmap F (K2.approx n) oo fmap F gZ_pred) F1) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap F K1.predicate K2.predicate (@compose K1.predicate K2.predicate K2.predicate (K2.approx n) gZ_pred) F1)) (@pair nat (_functor F K2.predicate) n (@fmap F K1.predicate K2.predicate gZ_pred F1)) *)
assert (K2'.approx n oo gZ_pred = gZ_pred).
(* Goal: None *)
extensionality P1 k2.
(* Goal: None *)
destruct k2.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
unfold gZ_pred, compose, K2'.approx; simpl.
(* Goal: None *)
destruct (le_gt_dec n (level k)); auto.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap F K1.predicate K2.predicate (@compose K1.predicate K2.predicate K2.predicate (K2.approx n) gZ_pred) F1)) (@pair nat (_functor F K2.predicate) n (@fmap F K1.predicate K2.predicate gZ_pred F1)) *)
congruence.
Qed.

End Z.

Section Sn.
(* The inductive step.  To keep things simple, we will put definitions first. *)
Variable f : K1.knot -> K2.knot.
Variable g : K2.knot -> K1.knot.


Definition f_Sn (k1 : K1.knot) : K2.knot :=
  match K1.unsquash k1 with
    (n, F_p1) => K2.squash (n, f_F' g F_p1)
  end.

Definition g_Sn (k2 : K2.knot) : K1.knot :=
  match K2.unsquash k2 with
    (n, F_p2) => K1.squash (n, g_F' f F_p2)
  end.


(* Now we include details relevant to the proof of the inductive step. *)

Variable n : nat.
Variable iso1 : forall k, level k <= n -> (g oo f) k = k.
Variable iso2 : forall k, level k <= n -> (f oo g) k = k.

(* These two properties are enough to prove a bijection up to level k *)

Lemma f_inj : forall ka kb,
  level ka <= n ->
  level kb <= n ->
  f ka = f kb ->
  ka = kb.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K1.knot ka kb *)
assert ((g oo f) ka = (g oo f) kb) by (unfold compose; rewrite H1; trivial).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
do 2 rewrite iso1 in H2; trivial.
Qed.

Lemma g_inj : forall ka kb,
  level ka <= n ->
  level kb <= n ->
  g ka = g kb ->
  ka = kb.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K2.knot ka kb *)
assert ((f oo g) ka = (f oo g) kb) by (unfold compose; rewrite H1; trivial).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
do 2 rewrite iso2 in H2; trivial.
Qed.

Lemma f_surj : forall k2,
  level k2 <= n ->
  exists k1,
  f k1 = k2.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @ex K1.knot (fun k1 : K1.knot => @eq K2.knot (f k1) k2) *)
exists (g k2).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite <- iso2; trivial.
Qed.

Lemma g_surj : forall k1,
  level k1 <= n ->
  exists k2,
  g k2 = k1.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @ex K2.knot (fun k2 : K2.knot => @eq K1.knot (g k2) k1) *)
exists (f k1).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite <- iso1; trivial.
Qed.

(* Now we show that k1_pred and k2_pred are the identity under approximation. *)
(* Not clear that we need this. *)
(*
Lemma k1_pred_iso: K1.approx (n+1) oo k1_pred = K1.approx (n+1).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : K2.predicate, K2.predicate) (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx m) (g_pred' f))) (K2.approx m) *)
extensionality p k.
unfold k1_pred, compose, g_pred, f_pred in *.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
apply prop_ext; split; do 2 intro; spec H H0; rewrite iso1 in *; trivial; omega.
Qed.

Lemma k2_pred_iso: K2.approx (n+1) oo k2_pred = K2.approx (n+1).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : K2.predicate, K2.predicate) (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx m) (g_pred' f))) (K2.approx m) *)
extensionality p k.
unfold k2_pred, compose, g_pred, f_pred in *.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
apply prop_ext; split; do 2 intro; spec H H0; rewrite iso2 in *; trivial; omega.
Qed.
*)

(*
What we would like to show next is that f and g preserve the level of the knot,
even in their (unfortunately non-unique over level n) inverses.
Unfortunately, this is not possible:

Lemma f_level: forall k, K1.level k = K2.level (f k).

This is clearly impossible since we don't know anything about the behavior of f
for knots above level n.

Actually, even this weaker version is not provable:

Lemma f_level: forall k,
(K1.level k <= n \/ K2.level (f k) <= n) ->
K1.level k = K2.level (f k).

Counterexample: K1.knot = K2.knot = nat;
                            K1.level = K2.level = id;
                            f = inc, g = dec;
*)

(* So we must assert them as axioms, which means a bigger induction *)
Variable f_level: forall k, level k = level (f k).
Variable g_level: forall k, level k = level (g k).

(* However, using them we can prove pred_iso1 and pred_iso2, which are vital. *)
Lemma predn_iso1: forall m,
  m <= (n+1) ->
  g_pred' f oo K2.approx m oo f_pred' g = K1.approx m.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : K2.predicate, K2.predicate) (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx m) (g_pred' f))) (K2.approx m) *)
extensionality p k.
(* Goal: @eq K2.TF.T (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx m) (g_pred' f)) p k) (K2.approx m p k) *)
unfold g_pred', f_pred', compose in *.
(* Goal: @eq K2.TF.T (K1.approx m (fun x : prod K1.knot other => p (@map_pair K1.knot K2.knot other other f (id other) x)) (@map_pair K2.knot K1.knot other other g (id other) k)) (K2.approx m p k) *)
destruct k.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
unfold K2'.approx, map_pair, id; simpl.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
unfold K1'.approx; simpl.
(* Goal: @eq K1.TF.T (if le_gt_dec m (@level K2.knot K2.ag_knot (f k)) then K2.TF.T_bot else p (@pair K1.knot other (g (f k)) o)) (if le_gt_dec m (@level K1.knot K1.ag_knot k) then K1.TF.T_bot else p (@pair K1.knot K1.TF.other k o)) *)
rewrite <- f_level.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: @eq K2.TF.T (if le_gt_dec m (@level K2.knot K2.ag_knot k) then K1.TF.T_bot else p (@pair K2.knot other (f (g k)) o)) (if le_gt_dec m (@level K2.knot K2.ag_knot k) then K2.TF.T_bot else p (@pair K2.knot K2.TF.other k o)) *)
destruct (le_gt_dec m (level k)); auto.
(* Goal: @eq K1.TF.T (p (@pair K1.knot other (g (f k)) o)) (p (@pair K1.knot K1.TF.other k o)) *)
rewrite iso1; auto.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
simpl; omega.
Qed.

Lemma predn_iso2: forall m,
  m <= (n+1) ->
  f_pred' g oo K1.approx m oo g_pred' f = K2.approx m.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : K2.predicate, K2.predicate) (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx m) (g_pred' f))) (K2.approx m) *)
extensionality p k.
(* Goal: @eq K2.TF.T (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx m) (g_pred' f)) p k) (K2.approx m p k) *)
unfold g_pred', f_pred', compose in *.
(* Goal: @eq K2.TF.T (K1.approx m (fun x : prod K1.knot other => p (@map_pair K1.knot K2.knot other other f (id other) x)) (@map_pair K2.knot K1.knot other other g (id other) k)) (K2.approx m p k) *)
destruct k.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
unfold K1'.approx, map_pair, id; simpl.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
unfold K2'.approx; simpl.
(* Goal: None *)
rewrite <- g_level.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: @eq K2.TF.T (if le_gt_dec m (@level K2.knot K2.ag_knot k) then K1.TF.T_bot else p (@pair K2.knot other (f (g k)) o)) (if le_gt_dec m (@level K2.knot K2.ag_knot k) then K2.TF.T_bot else p (@pair K2.knot K2.TF.other k o)) *)
destruct (le_gt_dec m (level k)); auto.
(* Goal: @eq K2.TF.T (p (@pair K2.knot other (f (g k)) o)) (p (@pair K2.knot K2.TF.other k o)) *)
rewrite iso2; auto.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
simpl; omega.
Qed.

(* Now we can prove that f_Sn and g_Sn preserve the isomorphism. *)
Lemma iso1_Sn : forall k, level k <= n + 1 -> (g_Sn oo f_Sn) k = k.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K2.knot (@compose K2.knot K1.knot K2.knot f_Sn g_Sn k) k *)
unfold compose, g_Sn, f_Sn.
(* Goal: @eq K1.knot (let (n, F_p2) := K2.unsquash (let (n, F_p1) := K1.unsquash k in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))) in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) k *)
remember (K1.unsquash k) as unsq_k.
(* Goal: @eq K2.knot (let (n, F_p1) := K1.unsquash (let (n, F_p2) := unsq_k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))) k *)
destruct unsq_k as [n0 Fp].
(* Goal: None *)
rewrite K2.unsquash_squash.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate (@compose K1.predicate K2.predicate K2.predicate (K2.approx m) (f_pred' g)) F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Sn) F1) *)
rewrite K1.knot_level in H.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (f_F' g (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n0) (g_F' f Fp))))) k *)
rewrite <- Hequnsq_k in H.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
replace (fmap F (K2.approx n0) (f_F' g Fp)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (K2.approx n0) oo (fmap F (f_pred' g))) Fp) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
replace (g_F' f (fmap F (K2.approx n0 oo f_pred' g) Fp)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (g_pred' f) oo fmap F (K2.approx n0 oo f_pred' g)) Fp) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (@fmap F K2.predicate K2.predicate (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx n0) (g_pred' f))) Fp))) k *)
symmetry in Hequnsq_k.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite predn_iso1; trivial.
(* Goal: @eq K1.knot (K1.squash (@pair nat (_functor F K1.predicate) n0 (@fmap F K1.predicate K1.predicate (K1.approx n0) Fp))) k *)
rewrite <- (K1L.unsquash_approx Hequnsq_k).
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 Fp)) k *)
rewrite <- Hequnsq_k.
(* Goal: @eq K1.knot (K1.squash (K1.unsquash k)) k *)
rewrite K1.squash_unsquash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma iso2_Sn : forall k, level k <= n + 1 -> (f_Sn oo g_Sn) k = k.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K2.knot (@compose K2.knot K1.knot K2.knot f_Sn g_Sn k) k *)
unfold compose, g_Sn, f_Sn.
(* Goal: @eq K2.knot (let (n, F_p1) := K1.unsquash (let (n, F_p2) := K2.unsquash k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))) k *)
remember (K2.unsquash k) as unsq_k.
(* Goal: @eq K2.knot (let (n, F_p1) := K1.unsquash (let (n, F_p2) := unsq_k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))) k *)
destruct unsq_k as [n0 Fp].
(* Goal: None *)
rewrite K1.unsquash_squash.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: @eq K1.knot (g k) (K1.squash (@pair nat (_functor F K1.predicate) n0 (g_F' f _f))) *)
rewrite K2.knot_level in H.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (f_F' g (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n0) (g_F' f Fp))))) k *)
rewrite <- Hequnsq_k in H.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
replace (fmap F (K1.approx n0) (g_F' f Fp)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (K1.approx n0) oo (fmap F (g_pred' f))) Fp) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
replace (f_F' g (fmap F (K1.approx n0 oo g_pred' f) Fp)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (f_pred' g) oo fmap F (K1.approx n0 oo g_pred' f)) Fp) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (@fmap F K2.predicate K2.predicate (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (@compose K2.predicate K1.predicate K1.predicate (K1.approx n0) (g_pred' f))) Fp))) k *)
symmetry in Hequnsq_k.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite predn_iso2; trivial.
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 (@fmap F K2.predicate K2.predicate (K2.approx n0) Fp))) k *)
rewrite <- (K2L.unsquash_approx Hequnsq_k).
(* Goal: @eq K2.knot (K2.squash (@pair nat (_functor F K2.predicate) n0 Fp)) k *)
rewrite <- Hequnsq_k.
(* Goal: @eq K1.knot (g k) (g (K2.squash (K2.unsquash k))) *)
rewrite K2.squash_unsquash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

(* We must also prove that f_Sn and g_Sn preserve the level property. *)
Lemma f_level_Sn: forall k, level k = level (f_Sn k).
Proof.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
intro.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f_Sn k1)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' g_Sn (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold f_Sn.
(* Goal: @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (let (n, F_p2) := K2.unsquash k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2)))) *)
rewrite K1.knot_level, K2.knot_level.
(* Goal: @eq nat (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash k)) (@fst nat (_functor K2.TF.F K2.predicate) (K2.unsquash (let (n, F_p1) := K1.unsquash k in K2.squash (@pair nat (_functor F K2.predicate) n (f_F' g F_p1))))) *)
remember (K1.unsquash k) as uk.
(* Goal: @eq nat (@fst nat (_functor K2.TF.F K2.predicate) uk) (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash (let (n, F_p2) := uk in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))))) *)
destruct uk.
(* Goal: None *)
rewrite K2.unsquash_squash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma g_level_Sn: forall k, level k = level (g_Sn k).
Proof.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
intro.
(* Goal: @eq K1.knot (g k) (g_Sn k) *)
unfold g_Sn.
(* Goal: @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (let (n, F_p2) := K2.unsquash k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2)))) *)
rewrite K1.knot_level, K2.knot_level.
(* Goal: @eq nat (@fst nat (_functor K2.TF.F K2.predicate) (K2.unsquash k)) (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash (let (n, F_p2) := K2.unsquash k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))))) *)
remember (K2.unsquash k) as uk.
(* Goal: @eq nat (@fst nat (_functor K2.TF.F K2.predicate) uk) (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash (let (n, F_p2) := uk in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))))) *)
destruct uk.
(* Goal: None *)
rewrite K1.unsquash_squash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

(* Finally, we must show that f_Sn preserves unsquashing. *)
Variable fn_unsquash : forall k1,
  level k1 <= n ->
  forall U1,
  U1 = K1.unsquash k1 ->
  K2.unsquash (f k1) = (fst U1, f_F' g (snd U1)).

Lemma Fn_iso2 : forall m,
  m <= n + 1 ->
  g_F' f oo f_F' g oo fmap F (K1.approx m) = fmap F (K1.approx m).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : _functor F K1.predicate, _functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (g_F' f) (@compose (_functor F K1.predicate) (_functor F K1.predicate) (_functor F K2.predicate) (f_F' g) (@fmap F K1.predicate K1.predicate (K1.approx m)))) (@fmap F K1.predicate K1.predicate (K1.approx m)) *)
unfold g_F', f_F'.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
do 2 rewrite fmap_comp.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (g_pred' f oo f_pred' g oo K1.approx m) with (K1.approx m); trivial.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite f_pred'_approx; trivial.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite predn_iso1; trivial.
Qed.

Lemma gn_unsquash : forall k2,
  level k2 <= n ->
  forall U2,
  U2 = K2.unsquash k2 ->
  K1.unsquash (g k2) = (fst U2, g_F' f (snd U2)).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash (g k2)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) U2) (g_F' f (@snd nat (_functor K2.TF.F K2.predicate) U2))) *)
destruct U2 as [m F2].
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
generalize (fn_unsquash (g k2)); intro.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash (g k2)) (@pair nat (_functor F K1.predicate) m (g_F' f F2)) *)
rewrite <- g_level in H1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash (g k2)) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
remember (g k2) as k1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) m (g_F' f F2)) *)
specialize ( H1 H (K1.unsquash k1)).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
firstorder.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
assert (f k1 = (f oo g) k2) by (unfold compose; congruence).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite iso2 in H2; trivial.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) m (g_F' f F2)) *)
rewrite H2 in H1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) m (g_F' f F2)) *)
rewrite <- H0 in H1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) m (g_F' f F2)) *)
inversion H1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
apply injective_projections; simpl; trivial.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash k1)) (gF (fF (@snd nat (_functor K1.TF.F K1.predicate) (K1.unsquash k1))))) *)
remember (K1.unsquash k1) as U1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (g_F' f (f_F' g (snd U1))) with ((g_F' f oo f_F' g) (snd U1)) by trivial.
(* Goal: @eq (_functor K1.TF.F K1.predicate) (@snd nat (_functor K1.TF.F K1.predicate) U1) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (g_F' f) (f_F' g) (@snd nat (_functor K1.TF.F K1.predicate) U1)) *)
destruct U1 as [m' F1].
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
simpl in *.
(* Goal: @eq (_functor K1.TF.F K1.predicate) F1 (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (g_F' f) (f_F' g) F1) *)
subst m'.
(* Goal: @eq (_functor K1.TF.F K1.predicate) F1 (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (g_F' f) (f_F' g) F1) *)
clear H1.
(* Goal: @eq (_functor K1.TF.F K1.predicate) F1 (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (g_F' f) (f_F' g) F1) *)
symmetry in HeqU1.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
generalize (K1L.unsquash_approx HeqU1); intro.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) F1) (f_F' g F1) *)
rewrite H1.
replace ((g_F' f oo f_F' g) (fmap F (K1'.approx m) F1)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((g_F' f oo f_F' g oo fmap F (K1.approx m)) F1) by trivial.
(* Goal: @eq (_functor K1.TF.F K1.predicate) (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx m) F1) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (g_F' f) (@compose (_functor F K1.predicate) (_functor F K1.predicate) (_functor F K2.predicate) (f_F' g) (@fmap F K1.predicate K1.predicate (K1.approx m))) F1) *)
rewrite Fn_iso2.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: @eq K1.knot (g k) (K1.squash (@pair nat (_functor F K1.predicate) n0 (g_F' f _f))) *)
rewrite K2.knot_level in H.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) F1) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
rewrite <- H0 in H.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
omega.
Qed.

Lemma gn_squash : forall m F2,
  m <= n ->
  g (K2.squash (m, F2)) = K1.squash (m, g_F' f F2).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
apply (K1L.unsquash_inj).
assert (level (K2.squash (m , F2)) <= n) by
  (simpl; rewrite K2.knot_level; rewrite K2.unsquash_squash; simpl; trivial).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite (gn_unsquash (K2'.squash (m, F2)) H0 (K2.unsquash (K2'.squash (m, F2)))); trivial.
(* Goal: None *)
rewrite K1.unsquash_squash.
(* Goal: None *)
rewrite K2.unsquash_squash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
replace (g_F' f (fmap F (K2'.approx m) F2)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (g_pred' f) oo (fmap F (K2.approx m))) F2) by trivial.
replace (m, fmap F (K1'.approx m) (g_F' f F2)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  (m, (fmap F (K1.approx m) oo fmap F (g_pred' f)) F2) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
do 2 rewrite fmap_comp.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
apply injective_projections; simpl; trivial.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite g_pred'_approx; trivial.
Qed.

Lemma fSn_unsquash : forall k1,
  level k1 <= n + 1 ->
  forall U1,
  U1 = K1.unsquash k1 ->
  K2.unsquash (f_Sn k1) = (fst U1, f_F' (g_Sn) (snd U1)).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f_Sn k1)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' g_Sn (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold f_Sn.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S n)) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
rewrite <- H0.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred (@snd nat (_functor K1.TF.F K1.predicate) U1)) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) (@snd nat (_functor K1.TF.F K1.predicate) U1)) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
destruct U1 as [m F1].
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: None *)
rewrite K2.unsquash_squash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
apply injective_projections; simpl; trivial.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) F1)) (f_F' g (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) F1)) *)
unfold f_F'.
replace (fmap F (K2'.approx m) (fmap F (f_pred' g) F1)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (K2.approx m) oo fmap F  (f_pred' g)) F1) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate (@compose K1.predicate K2.predicate K2.predicate (K2.approx m) (f_pred' g)) F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Sn) F1) *)
rewrite K1.knot_level in H.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) F1) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
rewrite <- H0 in H.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) F1) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
symmetry in H0.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
generalize (K1L.unsquash_approx H0); intro.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) F1) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
pattern F1 at 2.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) F1) (f_F' g F1) *)
rewrite H1.
replace (fmap F (f_pred' g_Sn) (fmap F (K1'.approx m) F1)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (f_pred' g_Sn) oo fmap F (K1.approx m)) F1) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap F K1.predicate K2.predicate (@compose K1.predicate K2.predicate K2.predicate (K2.approx n) gZ_pred) F1)) (@pair nat (_functor F K2.predicate) n (@fmap F K1.predicate K2.predicate gZ_pred F1)) *)
assert (K2'.approx m oo f_pred' g = f_pred' g_Sn oo K1.approx m); try congruence.
(* Goal: None *)
extensionality p1 k2.
(* Goal: None *)
destruct k2.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl; unfold f_pred', compose, K1.approx, K2.approx, g_Sn; simpl.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite K1.knot_level, K2'.knot_level; unfold g_Sn; simpl.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
unfold map_pair; simpl.
(* Goal: None *)
remember (K2.unsquash k) as uk2.
(* Goal: None *)
destruct uk2 as [m' F2].
(* Goal: None *)
rewrite K1.unsquash_squash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: None *)
destruct (le_gt_dec m m'); auto.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (id (_functor F K1.predicate) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold id.
(* Goal: None *)
rewrite <- gn_squash in *; [ | omega ].
(* Goal: None *)
rewrite Hequk2.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite K2.squash_unsquash; trivial.
Qed.

Lemma gn_gSn_eq_n : forall k,
level k <= n ->
g k = g_Sn k.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K1.knot (g k) (g_Sn k) *)
unfold g_Sn.
(* Goal: @eq K1.knot (g k) (let (n, F_p2) := K2.unsquash k in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) *)
remember (K2.unsquash k) as usqk.
(* Goal: @eq K1.knot (g k) (let (n, F_p2) := usqk in K1.squash (@pair nat (_functor F K1.predicate) n (g_F' f F_p2))) *)
destruct usqk.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: @eq K1.knot (g k) (K1.squash (@pair nat (_functor F K1.predicate) n0 (g_F' f _f))) *)
rewrite K2.knot_level in H.
(* Goal: @eq K1.knot (g k) (K1.squash (@pair nat (_functor F K1.predicate) n0 (g_F' f _f))) *)
rewrite <- Hequsqk in H.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
rewrite <- gn_squash; try omega.
(* Goal: @eq K1.knot (g k) (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n0 _f))) *)
rewrite Hequsqk.
(* Goal: @eq K1.knot (g k) (g (K2.squash (K2.unsquash k))) *)
rewrite K2.squash_unsquash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

End Sn.

Section FG.
(* We tie it together *)

Fixpoint fg (n : nat) {struct n} : ((K1.knot -> K2.knot) * (K2.knot -> K1.knot)) :=
  match n with
   | 0 => (f_Z, g_Z)
   | S n => match fg n with (fn, gn) => (f_Sn gn, g_Sn fn) end
  end.

Lemma fg_level_fst : forall n k, level k = level (fst (fg n) k).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
destruct n.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (f_Z k0)) *)
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
apply f_level_Z.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) k) k *)
unfold fg.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) k) k *)
fold fg.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
destruct (fg n).
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (f_Sn k2 k0)) *)
apply f_level_Sn.
Qed.

Lemma fg_level_snd : forall n k, level k = level (snd (fg n) k).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
destruct n.
(* Goal: @eq nat (@level K2.knot K2.ag_knot k0) (@level K1.knot K1.ag_knot (g_Z k0)) *)
(* Goal: @eq nat (@level K2.knot K2.ag_knot k0) (@level K1.knot K1.ag_knot (gn k0)) *)
apply g_level_Z.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) k) k *)
unfold fg.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) k) k *)
fold fg.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
destruct (fg n).
(* Goal: @eq nat (@level K2.knot K2.ag_knot k0) (@level K1.knot K1.ag_knot (g_Sn k1 k0)) *)
apply g_level_Sn.
Qed.

Lemma fg_id : forall n k, level k <= n -> (fst (fg n) oo snd (fg n)) k  = k.
Proof.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) n) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
induction n.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) k) k *)
unfold fg.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite iso2_Z; trivial.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) k) k *)
unfold fg.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) k) k *)
fold fg.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k2) *)
remember (fg n) as fgn.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) fgn k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fgn in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k2) *)
destruct fgn as [fn gn].
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
simpl in *.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
rewrite (iso2_Sn fn gn n); trivial; try omega.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
destruct n.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
unfold fg in Heqfgn.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
inversion Heqfgn.
(* Goal: @eq nat (@level K2.knot K2.ag_knot k0) (@level K1.knot K1.ag_knot (g_Z k0)) *)
(* Goal: @eq nat (@level K2.knot K2.ag_knot k0) (@level K1.knot K1.ag_knot (gn k0)) *)
apply g_level_Z.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
unfold fg in Heqfgn.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
fold fg in Heqfgn.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
destruct (fg n).
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
inversion Heqfgn.
(* Goal: @eq nat (@level K2.knot K2.ag_knot k0) (@level K1.knot K1.ag_knot (g_Sn k1 k0)) *)
apply g_level_Sn.
Qed.

Lemma gf_id : forall n k, level k <= n -> (snd (fg n) oo fst (fg n)) k  = k.
Proof.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) n) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
induction n.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) k) k *)
unfold fg.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite iso1_Z; trivial.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n))) k) k *)
unfold fg.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) k) k *)
fold fg.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k2) *)
remember (fg n) as fgn.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) fgn k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fgn in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k2) *)
destruct fgn as [fn gn].
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
simpl in *.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
rewrite (iso1_Sn fn gn n); trivial; try omega.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
destruct n.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
unfold fg in Heqfgn.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
inversion Heqfgn.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (f_Z k0)) *)
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
apply f_level_Z.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
unfold fg in Heqfgn.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
fold fg in Heqfgn.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
destruct (fg n).
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (fn k0)) *)
inversion Heqfgn.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k0) (@level K2.knot K2.ag_knot (f_Sn k2 k0)) *)
apply f_level_Sn.
Qed.

Lemma fg_fst_unsquash: forall n k, level k <= n ->
  forall U1,
  U1 = K1.unsquash k ->
  K2.unsquash (fst (fg n) k) = (fst U1, f_F' (snd (fg n)) (snd U1)).
Proof.
induction n;
unfold fg;
fold fg;
simpl;
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f_Z k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' g_Z (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
rewrite (fZ_unsquash k H U1 H0).
(* Move up? *)
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
apply injective_projections; simpl; trivial.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (fF_Z (@snd nat (_functor K1.TF.F K1.predicate) U1)) (f_F' g_Z (@snd nat (_functor K1.TF.F K1.predicate) U1)) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold f_F', fF_Z.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred (@snd nat (_functor K1.TF.F K1.predicate) U1)) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) (@snd nat (_functor K1.TF.F K1.predicate) U1)) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
destruct U1 as [m F1].
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate (@compose K1.predicate K2.predicate K2.predicate (K2.approx m) (f_pred' g)) F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Sn) F1) *)
simpl in H; rewrite K1.knot_level in H.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) F1) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
rewrite <- H0 in H.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
assert (m = 0) by omega.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) F1) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
subst m.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
clear H.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) F1) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
symmetry in H0.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
generalize (K1L.unsquash_approx H0); intro.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) F1) *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
pattern F1 at 2.
(* Goal: (fun _f : _functor K1.TF.F K1.predicate => @eq (_functor K2.TF.F K2.predicate) (@fmap F K1.predicate K2.predicate gZ_pred F1) (@fmap F K1.predicate K2.predicate (f_pred' g_Z) _f)) F1 *)
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
rewrite H.
replace (fmap F (f_pred' g_Z) (fmap F (K1'.approx 0) F1)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (f_pred' g_Z) oo fmap F (K1.approx 0)) F1) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (f_pred' g_Z oo K1'.approx 0) with gZ_pred; trivial.
(* End move up *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k2) *)
remember (fg n) as fgn.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) fgn k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fgn in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k2) *)
destruct fgn as [fn gn].
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
simpl in *.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f_Sn gn k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (g_Sn fn) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
replace gn with (snd (fg n)) by (rewrite <- Heqfgn; trivial).
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
generalize (fSn_unsquash (fst (fg n)) (snd (fg n)) n (gf_id n) (fg_id n) (fg_level_fst n) (fg_level_snd n)); intro.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f_Sn (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (g_Sn fn) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
rewrite <- Heqfgn in H1.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f_Sn (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (g_Sn fn) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
simpl in H1.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
replace (n + 1) with (S n) in H1 by omega.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f_Sn (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (g_Sn fn) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
specialize ( H1 IHn k H U1 H0).
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f_Sn (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) k)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (f_F' (g_Sn fn) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
rewrite <- Heqfgn.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) F1) (f_F' g F1) *)
rewrite H1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma fg_fg_eq: forall n k2,
level k2 < n ->
snd (fg (level k2)) k2 = snd (fg n) k2.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
assert (exists m, level k2 + m = n).
(* Goal: @ex nat (fun m : nat => @eq nat (Init.Nat.add (@level K2.knot K2.ag_knot k2) m) n) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
remember (level k2) as m.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) n) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
clear -H.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) n) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
induction n.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) O) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S n)) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
inversion H.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
assert (m = n \/ m < n) by omega.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
clear H.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S n)) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
destruct H0.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S n)) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S n)) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
subst n.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S m)) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S n)) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
exists 1.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
omega.
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S n)) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
destruct (IHn H) as [m0 ?].
(* Goal: @ex nat (fun m0 : nat => @eq nat (Init.Nat.add m m0) (S n)) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
rewrite <- H0.
(* Goal: @ex nat (fun m1 : nat => @eq nat (Init.Nat.add m m1) (S (Init.Nat.add m m0))) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
exists (m0 + 1).
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
omega.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
destruct H0 as [m ?].
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
clear H.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) *)
revert m H0.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
induction n; intros.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (level k2) with 0 by omega; trivial.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n)) k2) *)
destruct m.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (level k2 + 0) with (level k2) in H0 by trivial.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n)) k2) *)
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n)) k2) *)
rewrite H0.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k2)) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (S n)) k2) *)
specialize ( IHn m).
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
rewrite IHn; try omega.
(* Goal: forall (k : K1.knot) (_ : le (@level K1.knot K1.ag_knot k) (S n)), @eq K1.knot (@compose K1.knot K2.knot K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := (fix fg (n : nat) : prod (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) := match n with | O => @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) f_Z g_Z | S n0 => let (fn, gn) := fg n0 in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn) end) n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn))) k) k *)
unfold fg; fold fg.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fg n in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k2) *)
remember (fg n) as fgn.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) fgn k2) (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (let (fn, gn) := fgn in @pair (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (f_Sn gn) (g_Sn fn)) k2) *)
destruct fgn as [fn gn].
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
generalize (gn_gSn_eq_n (fst (fg n)) (snd (fg n)) n (gf_id n) (fg_id n) (fg_level_fst n) (fg_level_snd n) (fg_fst_unsquash n)); intro.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
rewrite <- Heqfgn in H.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
simpl in H.
(* Goal: @eq K1.knot (gn k2) (g_Sn fn k2) *)
apply H.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
simpl in *.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
omega.
Qed.

End FG.

(* Now for the main definitions and theorems *)

Definition f (k : K1.knot) : K2.knot := fst (fg (level k)) k.

Definition g (k : K2.knot) : K1.knot := snd (fg (level k)) k.

Definition fF : TF.F K1.predicate -> TF.F K2.predicate :=
  f_F' g.

Definition gF : TF.F K2.predicate -> TF.F K1.predicate :=
  g_F' f.

Lemma iso1 : f oo g = id K2.knot.
Proof.
(* Goal: @eq (forall _ : K1.knot, K1.knot) (@compose K1.knot K2.knot K1.knot g f) (id K1.knot) *)
extensionality k.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (id (_functor F K1.predicate) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold id.
(* Goal: @eq K1.knot (@compose K1.knot K2.knot K1.knot g f k) k *)
unfold compose, f, g.
(* Goal: None *)
rewrite <- fg_level_snd.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K1.knot K1.ag_knot k)) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K1.knot K1.ag_knot k)) k)) k *)
remember (level k) as n.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (fst (fg n) (snd (fg n) k)) with ((fst (fg n) oo snd (fg n)) k) by trivial.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
rewrite fg_id; trivial; omega.
Qed.

Lemma iso2 : g oo f = id K1.knot.
Proof.
(* Goal: @eq (forall _ : K1.knot, K1.knot) (@compose K1.knot K2.knot K1.knot g f) (id K1.knot) *)
extensionality k.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (id (_functor F K1.predicate) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold id.
(* Goal: @eq K1.knot (@compose K1.knot K2.knot K1.knot g f k) k *)
unfold compose, f, g.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K1.knot K1.ag_knot k)) k))) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K1.knot K1.ag_knot k)) k)) k *)
rewrite <- fg_level_fst.
(* Goal: @eq K1.knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K1.knot K1.ag_knot k)) (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K1.knot K1.ag_knot k)) k)) k *)
remember (level k) as n.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (snd (fg n) (fst (fg n) k)) with ((snd (fg n) oo fst (fg n)) k) by trivial.
(* Goal: le (@level K2.knot K2.ag_knot k2) n *)
rewrite gf_id; trivial; omega.
Qed.

Lemma fpred_gpred : f_pred' g oo g_pred' f = id (K2.predicate).
Proof.
(* Goal: @eq (forall _ : K2.predicate, K2.predicate) (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (g_pred' f)) (id K2.predicate) *)
extensionality P2 k2.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (id (_functor F K1.predicate) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold id.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
unfold g_pred', f_pred', map_pair, compose; simpl.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
destruct k2; simpl.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (f (g k)) with ((f oo g) k) by trivial.
(* Goal: @eq K2.TF.T (P2 (@pair K2.knot other (@compose K2.knot K1.knot K2.knot f g k) (id other (id other o)))) (P2 (@pair K2.knot K2.TF.other k o)) *)
rewrite iso1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma gpred_fpred : g_pred' f oo f_pred' g = id (K1.predicate).
Proof.
(* Goal: @eq (forall _ : K1.predicate, K1.predicate) (@compose K1.predicate K2.predicate K1.predicate (g_pred' f) (f_pred' g)) (id K1.predicate) *)
extensionality P1 k1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (id (_functor F K1.predicate) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold id.
(* Goal: @eq K1.TF.T (@compose K1.predicate K2.predicate K1.predicate (g_pred' f) (f_pred' g) P1 k1) (P1 k1) *)
unfold g_pred', f_pred', compose.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
unfold map_pair; simpl.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
destruct k1; simpl.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (g (f k)) with ((g oo f) k) by trivial.
(* Goal: @eq K1.TF.T (P1 (@pair K1.knot other (@compose K1.knot K2.knot K1.knot g f k) (id other (id other o)))) (P1 (@pair K1.knot K1.TF.other k o)) *)
rewrite iso2.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma Fiso1 : fF oo gF = id (F K2.predicate).
Proof.
(* Goal: @eq (forall _ : _functor F K2.predicate, _functor F K2.predicate) (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K2.predicate) fF gF) (id (_functor F K2.predicate)) *)
extensionality F2.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (id (_functor F K1.predicate) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold id.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) gF fF F1) F1 *)
unfold fF, gF, f_F', g_F'.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq (_functor F K2.predicate) (@fmap F K2.predicate K2.predicate (@compose K2.predicate K1.predicate K2.predicate (f_pred' g) (g_pred' f)) F2) F2 *)
rewrite fpred_gpred.
(* Goal: @eq (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (id K1.predicate) F1) F1 *)
rewrite fmap_id.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma Fiso2 : gF oo fF = id (F K1.predicate).
Proof.
(* Goal: @eq (forall _ : _functor F K1.predicate, _functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) gF fF) (id (_functor F K1.predicate)) *)
extensionality F1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (id (_functor F K1.predicate) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold id.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) gF fF F1) F1 *)
unfold fF, gF, f_F', g_F'.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
rewrite fmap_comp.
(* Goal: @eq (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (@compose K1.predicate K2.predicate K1.predicate (g_pred' f) (f_pred' g)) F1) F1 *)
rewrite gpred_fpred.
(* Goal: @eq (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (id K1.predicate) F1) F1 *)
rewrite fmap_id.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma f_level : forall k, level k = level (f k).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k) (@level K2.knot K2.ag_knot (f k)) *)
unfold f.
(* Goal: @eq nat (@level K1.knot K1.ag_knot k) (@level K2.knot K2.ag_knot (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K1.knot K1.ag_knot k)) k)) *)
rewrite <- (fg_level_fst (level k)).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma g_level : forall k, level k = level (g k).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K2.TF.T (P1 (@pair K1.knot other (g k) (id other o))) (P1 (@pair K1.knot other (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k) (id other o))) *)
unfold g.
(* Goal: @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k)) k)) *)
rewrite <- (fg_level_snd (level k)).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma f_unsquash : forall k1 U1,
  U1 = K1.unsquash k1 ->
  K2.unsquash (f k1) = (fst U1, fF (snd U1)).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f k1)) (@pair nat (_functor F K2.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (fF (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
destruct U1 as [n F1].
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (f k1)) (@pair nat (_functor F K2.predicate) n (fF F1)) *)
unfold f; simpl; rewrite K1.knot_level.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash k1))) k1)) (@pair nat (_functor F K2.predicate) n (fF F1)) *)
rewrite <- H.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (K2.unsquash (@fst (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k1)) (@pair nat (_functor F K2.predicate) n (fF F1)) *)
assert (level k1 <= n) by (rewrite K1.knot_level; rewrite <- H; trivial).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite (fg_fst_unsquash n k1 H0 (n, F1)); trivial.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
apply injective_projections; simpl; trivial.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) F1) (fF F1) *)
unfold fF.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) F1) (f_F' g F1) *)
symmetry in H.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
generalize (K1L.unsquash_approx H); intro.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) F1) (f_F' g F1) *)
rewrite H1.
(* Goal: @eq (_functor K2.TF.F K2.predicate) (f_F' (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n)) (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) F1)) (f_F' g (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) F1)) *)
unfold f_F'.
replace (fmap F (f_pred' (snd (fg n))) (fmap F (K1'.approx n) F1)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (f_pred' (snd (fg n))) oo fmap F (K1.approx n)) F1) by trivial.
replace (fmap F (f_pred' g) (fmap F (K1'.approx n) F1)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fmap F (f_pred' g) oo fmap F (K1.approx n)) F1) by trivial.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
do 2 rewrite fmap_comp.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (f_pred' (snd (fg n)) oo K1.approx n) with (f_pred' g oo K1'.approx n); trivial.
(* Goal: None *)
extensionality P1 k2.
(* Goal: None *)
unfold f_pred', compose.
(* Goal: None *)
unfold K1.approx.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
unfold map_pair; destruct k2; simpl.
(* Goal: None *)
rewrite <- fg_level_snd.
(* Goal: None *)
rewrite <- g_level.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: None *)
destruct (le_gt_dec n (level k)); auto.
(* Goal: @eq K2.TF.T (P1 (@pair K1.knot other (g k) (id other o))) (P1 (@pair K1.knot other (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k) (id other o))) *)
unfold g.
(* Goal: @eq K2.TF.T (P1 (@pair K1.knot other (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k)) k) (id other o))) (P1 (@pair K1.knot other (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k) (id other o))) *)
red in g0.
(* Goal: @eq K2.TF.T (P1 (@pair K1.knot other (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg (@level K2.knot K2.ag_knot k)) k) (id other o))) (P1 (@pair K1.knot other (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k) (id other o))) *)
rewrite (fg_fg_eq n k g0).
(* Goal: @eq K2.TF.T (P1 (@pair K1.knot other (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k) (id other o))) (P1 (@pair K1.knot other (@snd (forall _ : K1.knot, K2.knot) (forall _ : K2.knot, K1.knot) (fg n) k) (id other o))) *)
auto.
Qed.

Lemma g_unsquash : forall k2 U2,
  U2 = K2.unsquash k2 ->
  K1.unsquash (g k2) = (fst U2, gF (snd U2)).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash (g k2)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) U2) (gF (@snd nat (_functor K2.TF.F K2.predicate) U2))) *)
destruct U2 as [n F2].
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g_Sn k)) *)
generalize (f_unsquash (g k2)); intro.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash (g k2)) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
remember (g k2) as k1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
specialize ( H0 (K1.unsquash k1)).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
firstorder.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
assert (f k1 = (f oo g) k2) by (unfold compose; congruence).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
rewrite iso1 in H1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
unfold id in H1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
rewrite H1 in H0.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
rewrite <- H in H0.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) n (gF F2)) *)
inversion H0.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (K1.unsquash k1) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) (K1.unsquash k1)) (gF (fF (@snd nat (_functor K1.TF.F K1.predicate) (K1.unsquash k1))))) *)
remember (K1.unsquash k1) as U1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
replace (gF (fF (snd U1))) with ((gF oo fF) (snd U1)) by trivial.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) gF fF (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
rewrite Fiso2.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (id (_functor F K1.predicate) (@snd nat (_functor K1.TF.F K1.predicate) U1))) *)
unfold id.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) U1 (@pair nat (_functor F K1.predicate) (@fst nat (_functor K1.TF.F K1.predicate) U1) (@snd nat (_functor K1.TF.F K1.predicate) U1)) *)
destruct U1.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.


Lemma fF_approx : forall n,
fF oo (fmap F (K1.approx n)) = (fmap F (K2.approx n)) oo fF.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : _functor F K1.predicate, _functor F K2.predicate) (@compose (_functor F K1.predicate) (_functor F K1.predicate) (_functor F K2.predicate) fF (@fmap F K1.predicate K1.predicate (K1.approx n))) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K2.predicate) (@fmap F K2.predicate K2.predicate (K2.approx n)) fF) *)
unfold fF, f_F'.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
do 2 rewrite fmap_comp.
(* Goal: @eq (forall _ : _functor F K1.predicate, _functor F K2.predicate) (@fmap F K1.predicate K2.predicate (@compose K1.predicate K1.predicate K2.predicate (f_pred' g) (K1.approx n))) (@fmap F K1.predicate K2.predicate (@compose K1.predicate K2.predicate K2.predicate (K2.approx n) (f_pred' g))) *)
rewrite f_pred'_approx.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
(* Goal: forall k : K2.knot, @eq nat (@level K2.knot K2.ag_knot k) (@level K1.knot K1.ag_knot (g k)) *)
apply g_level.
Qed.

Lemma gF_approx : forall n,
gF oo (fmap F (K2.approx n)) = (fmap F (K1.approx n)) oo gF.
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq (forall _ : _functor F K2.predicate, _functor F K1.predicate) (@compose (_functor F K2.predicate) (_functor F K2.predicate) (_functor F K1.predicate) gF (@fmap F K2.predicate K2.predicate (K2.approx n))) (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF) *)
unfold gF, g_F'.
(* Goal: @eq (_functor F K1.predicate) (@compose (_functor F K1.predicate) (_functor F K2.predicate) (_functor F K1.predicate) (@fmap F K2.predicate K1.predicate (g_pred' f)) (@fmap F K1.predicate K2.predicate (f_pred' g)) F1) F1 *)
do 2 rewrite fmap_comp.
(* Goal: @eq (forall _ : _functor F K2.predicate, _functor F K1.predicate) (@fmap F K2.predicate K1.predicate (@compose K2.predicate K2.predicate K1.predicate (g_pred' f) (K2.approx n))) (@fmap F K2.predicate K1.predicate (@compose K2.predicate K1.predicate K1.predicate (K1.approx n) (g_pred' f))) *)
rewrite g_pred'_approx.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
(* Goal: forall k : K1.knot, @eq nat (@level K1.knot K1.ag_knot k) (@level K2.knot K2.ag_knot (f k)) *)
apply f_level.
Qed.

Lemma f_squash : forall n F1,
  f (K1.squash (n, F1)) = K2.squash (n, fF F1).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K2.knot (f (K1.squash (@pair nat (_functor K1.TF.F K1.predicate) n F1))) (K2.squash (@pair nat (_functor F K2.predicate) n (fF F1))) *)
apply (K2L.unsquash_inj).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite (f_unsquash (K1'.squash (n, F1)) (K1.unsquash (K1'.squash (n, F1)))); trivial.
(* Goal: None *)
rewrite K1.unsquash_squash.
(* Goal: None *)
rewrite K2.unsquash_squash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
replace (fF (fmap F (K1'.approx n) F1)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((fF oo (fmap F (K1.approx n))) F1) by trivial.
(* Goal: @eq (prod nat (_functor K2.TF.F K2.predicate)) (@pair nat (_functor F K2.predicate) n (@compose (_functor F K1.predicate) (_functor F K1.predicate) (_functor F K2.predicate) fF (@fmap F K1.predicate K1.predicate (K1.approx n)) F1)) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) (fF F1))) *)
rewrite fF_approx.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

Lemma g_squash : forall n F2,
  g (K2.squash (n, F2)) = K1.squash (n, gF F2).
Proof.
(* Goal: forall (n : nat) (F2 : _functor K2.TF.F K2.predicate), @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
intros.
(* Goal: @eq K1.knot (g (K2.squash (@pair nat (_functor K2.TF.F K2.predicate) n F2))) (K1.squash (@pair nat (_functor F K1.predicate) n (gF F2))) *)
apply (K1L.unsquash_inj).
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite (g_unsquash (K2'.squash (n, F2)) (K2.unsquash (K2'.squash (n, F2)))); trivial.
(* Goal: None *)
rewrite K1.unsquash_squash.
(* Goal: None *)
rewrite K2.unsquash_squash.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) (@fst nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))) (gF (@snd nat (_functor K2.TF.F K2.predicate) (@pair nat (_functor K2.TF.F K2.predicate) n (@fmap K2.TF.F K2.predicate K2.predicate (K2.approx n) F2))))) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
simpl.
replace (gF (fmap F (K2'.approx n) F2)) with
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
  ((gF oo (fmap F (K2.approx n))) F2) by trivial.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K2.predicate) (_functor F K1.predicate) gF (@fmap F K2.predicate K2.predicate (K2.approx n)) F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
rewrite gF_approx.
(* Goal: @eq (prod nat (_functor K1.TF.F K1.predicate)) (@pair nat (_functor F K1.predicate) n (@compose (_functor F K2.predicate) (_functor F K1.predicate) (_functor F K1.predicate) (@fmap F K1.predicate K1.predicate (K1.approx n)) gF F2)) (@pair nat (_functor K1.TF.F K1.predicate) n (@fmap K1.TF.F K1.predicate K1.predicate (K1.approx n) (gF F2))) *)
trivial.
Qed.

End Unique_Knot.
