text:
Set Implicit Arguments.
Require Import Metalib.Metatheory.
Require Import Program.Equality.
Require Export Variance.
Require Export Coq.micromega.Lia.

(* The first one is for recursive,
the second one is for universal. *)
Definition menv := list (nat * nat).
Notation empty_menv := (@nil (nat * nat)).

Definition genv  := list (atom * nat).

Fixpoint find  (n:nat) (E: list (nat * nat)) :=
  match E with
  | (k, v) :: E' =>
        if (n == k) then Some v else find n E'
  | nil => None
  end.

Fixpoint findX  (x:var) (G: list (atom * nat)) :=
  match G with
  | (k, v) :: E' =>
        if (x == k) then Some v else findX x E'
  | nil => None
  end.

Fixpoint bindings_rec (G:genv) (E: menv) (n: nat) (T:typ) : nat :=
  match T with
  | typ_nat => 1
  | typ_top => 1
  | typ_fvar x => 1 + match findX x G with
                      | Some k => k
                      | None => 1
                      end
  | typ_bvar m => 1 + match find (n - m) E with
                      | Some k => k
                      | None => 1
                      end
  | typ_arrow A B => S (bindings_rec G E n A) + (bindings_rec G E n B)
  | typ_label _ A => S (bindings_rec G E n A)
  | typ_all A B =>
    let i := bindings_rec G E n A in
    S (i + (bindings_rec G ((S n, i) :: E) (S n) B))
  | typ_mu A =>
       let i := bindings_rec G ((S n , 1) :: E) (S n) A in
       S (bindings_rec G ((S n, S i) :: E) (S n) A)
  end.

Fixpoint mk_benv (E:env) : genv :=
  match E with
  | nil => nil
  | (_, bind_typ _)::E' => mk_benv E'
  | (X, bind_sub U)::E' =>
        let G := mk_benv E' in
        (X, bindings_rec G nil 0 U) :: G
  end.

Definition bindings E T := bindings_rec (mk_benv E) nil 0 T.

Definition zero := 0.

Lemma bindings_find_in: forall (E1 E2:menv) k,
    find 0 (E1 ++ E2) = None ->
    find 0 (E1 ++ (0, k) :: E2) = Some k.
Proof with auto.
  induction E1...
  intros.
  destruct a.
  simpl in *.
  destruct n;simpl in *...
  inversion H.
Qed.

Lemma bindings_find_notin: forall (E1 E2:menv) k (n:nat),
    find (S n) (E1 ++ (0, k) :: E2) = find (S n) (E1++E2).
Proof with auto.
  induction E1;intros...
  -
    destruct a...
    simpl...
    destruct (S n == n0)...
Qed.

(* WFC typ n : type with <= k binded variables *)
Inductive WFC :  typ -> nat -> Prop :=
| WC_nat: forall k,
    WFC typ_nat k
| WC_top: forall k,
    WFC typ_top k
| WC_fvar: forall X k,
    WFC (typ_fvar X) k
| WC_bvar: forall b k,
    b <= k ->
    WFC (typ_bvar b) k
| WC_arrow: forall A B k,
    WFC A k ->
    WFC B k ->
    WFC (typ_arrow A B) k
| WC_all : forall A B n,
    WFC A n ->
    WFC B (S n) ->
    WFC (typ_all A B) n
| WC_rec: forall A n,
    WFC A (S n) ->
    WFC (typ_mu A) n
| WC_label: forall l A k,
    WFC A k ->
    WFC (typ_label l A) k
.

(* WFC typ n : type with < k binded variables *)
Inductive WFD :  typ -> nat -> Prop :=
| WD_nat: forall k,
    WFD typ_nat k
| WD_top: forall k,
    WFD typ_top k
| WD_fvar: forall X k,
    WFD (typ_fvar X) k
| WD_bvar: forall b k,
    b < k ->
    WFD (typ_bvar b) k
| WD_arrow: forall A B k,
    WFD A k ->
    WFD B k ->
    WFD (typ_arrow A B) k
| WD_rec: forall A n,
    WFD A (S n) ->
    WFD (typ_mu A) n
| WD_all: forall A B n,
    WFD A n ->
    WFD B (S n) ->
    WFD (typ_all A B) n
| WD_rcd: forall l A k,
    WFD A k ->
    WFD (typ_label l A) k
.

Inductive WFE : menv -> nat -> Prop :=
| WFE_empty:
    WFE nil 0
| WFE_cons: forall  b E k,
    WFE E k ->
    find (S k) E = None ->
    WFE ((S k,b)::E) (S k).

Hint Constructors WFC WFD WFE: core.

Fixpoint minusk (E:menv) (k:nat): menv :=
  match E with
  | nil => nil
  | (a,b)::E' => (a - k,b)::(minusk E' k)
  end.

Fixpoint maxfst (E:menv) : nat :=
  match E with
  | nil => 0
  | (a,_)::E' => max a (maxfst E')
  end.

Lemma WFE_maxfst : forall E k,
    WFE E k ->
    maxfst E <= k.
Proof with auto.
  induction 1...
  simpl...
  destruct (maxfst E)...
  lia.
Qed.

Lemma maxfst_find_none: forall E k,
    maxfst E <= k ->
    find (S k) E = None.
Proof with auto.
  induction E;intros...
  destruct a.
  simpl in *...
  destruct (S k == n)...
  lia.
  apply IHE...
  lia.
Qed.

Lemma WFE_find_none: forall k E,
    WFE E k ->
    find (S k) E = None.
Proof with auto.
  intros.
  apply maxfst_find_none...
  apply WFE_maxfst...
Qed.

Lemma WFE_S_n:forall E n k,
  WFE E n ->
  WFE ((S n, k)::E) (S n).
Proof with auto.
  induction E;intros...
  constructor...
  apply WFE_find_none...
Qed.

Lemma neq_minus: forall k n,
    n <= k ->
    n <> k ->
    exists q, k - n = S q.
Proof with auto.
  induction k;intros...
  inversion H...
  destruct H0...
  induction n...
  exists k...
  destruct IHk with (n:=n)...
  lia.
  exists x...
Qed.

Lemma neq_minus_v2: forall k n,
    n < k ->
    exists q, k - n = S q.
Proof with auto.
  induction k;intros...
  inversion H...
  induction n...
  exists k...
  destruct IHk with (n:=n)...
  lia.
  exists x...
Qed.

Fixpoint addone (E:menv) : menv :=
  match E with
  | nil => nil
  | (a,b)::E' => (S a,b)::(addone E')
  end.

Lemma find_add_eq: forall E k,
    find k E = find (S k) (addone E).
Proof with auto.
  induction E;intros...
  destruct a...
  simpl...
  destruct (k == n) ...
  destruct (S k == S n)...
  destruct n1...
  destruct (S k == S n)...
  destruct n1...
Qed.

Lemma find_add: forall E k b,
    k >= b ->
    find (k - b) E = find (S k - b) (addone E).
Proof with auto using find_add_eq.
  induction E;intros...
  -
    destruct a...
    assert (addone ((n, n0) :: E) = (S n, n0) :: addone E) by auto.
    rewrite H0.
    assert (S k - b = S (k-b)) by lia.
    rewrite H1.
    destruct (k-b);simpl...
    destruct (0==n)...
    destruct (1== S n)...
    destruct n1...
    destruct (1== S n)...
    destruct n1...
    destruct (S n1 == n)...
    destruct (S (S n1) == S n)...
    destruct n2...
    destruct (S (S n1) == S n)...
    destruct n2...
Qed.

Lemma bindings_add : forall E n A G,
    WFC A n ->
    bindings_rec G E n A = bindings_rec G (addone E) (S n) A.
Proof with auto.
  intros.
  generalize dependent E.
  induction H;intros;try solve [simpl;auto]...
  -
    simpl.
    rewrite find_add...
  -
    (* all *)
    simpl. f_equal.
    rewrite <- IHWFC1.
    replace ((S (S n), bindings_rec G E n A) :: addone E)
    with (addone ((S n, bindings_rec G E n A) :: E))...
  -
    simpl...
    f_equal...
    assert (bindings_rec G ((S (S n), 1) :: addone E) (S (S n)) A =
            bindings_rec G (addone ((S n, 1)::E)) (S (S n)) A) by auto.
    rewrite H0...
    rewrite <- IHWFC ...
    remember (S (bindings_rec G ((S n, 1) :: E) (S n) A)).
    assert ((S (S n), n0) :: addone E = addone ((S n,n0)::E)) by auto.
    rewrite H1.
    rewrite <- IHWFC...
Qed.

Fixpoint close_tt_rec (K : nat) (Z : atom) (T : typ) {struct T} : typ :=
  match T with
  | typ_nat         => typ_nat
  | typ_top         => typ_top
  | typ_bvar J      => typ_bvar J
  | typ_fvar X      => if X == Z then typ_bvar K else typ_fvar X
  | typ_arrow T1 T2 => typ_arrow (close_tt_rec K Z T1) (close_tt_rec K Z T2)
  | typ_mu T        => typ_mu (close_tt_rec (S K) Z T)
  | typ_all A B     => typ_all (close_tt_rec K Z A)
                                (close_tt_rec (S K) Z B)
  | typ_label l T => typ_label l (close_tt_rec K Z T)
  end.

Definition close_tt T X := close_tt_rec 0 X T.

Lemma close_wfc : forall A X,
    WFC A 0 ->
    WFC (close_tt A X) 0.
Proof with auto.
  intros A.
  unfold close_tt.
  generalize 0.
  induction A;intros;try solve [dependent destruction H;simpl in *;auto]...
  -
    simpl...
    destruct (a==X)...
Qed.

Lemma WFC_add_one : forall A k,
    WFC A k -> WFC A (S k).
Proof with auto.
  intros.
  induction H...
Qed.

Lemma close_wfd : forall A X,
    WFD A 0 ->
    WFD (close_tt A X) 1.
Proof with auto.
  intros A.
  unfold close_tt.
  generalize 0.
  induction A;intros;try solve [dependent destruction H;simpl in *;auto]...
  -
    simpl...
    destruct (a==X)...
Qed.

Lemma close_open_reverse_rec: forall T X,
    (X \notin fv_tt T) -> forall k, T = close_tt_rec k X (open_tt_rec k (typ_fvar X) T).
Proof with auto.
  intros T.
  induction T;intros;simpl in *;try solve [f_equal;auto]...
  -
    destruct (k==n)...
    simpl...
    destruct (X==X)...
    destruct n0...
  -
    destruct (a==X)...
    apply notin_singleton_1 in H...
    destruct H...
Qed.

Lemma close_open_reverse: forall T X,
    (X \notin fv_tt T) ->  T = close_tt (open_tt T (typ_fvar X)) X.
Proof with auto.
  intros.
  apply close_open_reverse_rec...
Qed.

Lemma close_type_wfc: forall A,
    type A -> WFC A 0.
Proof with auto.
  intros.
  induction H;intros...
  - constructor...
    apply WFC_add_one.
    pick fresh X.
    specialize_x_and_L X L.
    apply close_wfc with (X:=X) in H0.
    rewrite <- close_open_reverse in H0...
  - (* WFC_all *)
    constructor...
    apply WFC_add_one.
    pick_fresh X.
    specialize_x_and_L X L.
    apply close_wfc with (X:=X) in H1.
    rewrite <- close_open_reverse in H1...
Qed.

Lemma close_type_wfd: forall A,
    type A -> WFD A 0.
Proof with auto.
  intros.
  induction H;intros...
  - pick fresh X.
    specialize_x_and_L X L.
    constructor...
    apply close_wfd with (X:=X) in H0.
    rewrite <-close_open_reverse in H0...
  - (* WFD_all *)
    constructor...
    pick_fresh X.
    specialize_x_and_L X L.
    apply close_wfd with (X:=X) in H1.
    rewrite <- close_open_reverse in H1...
Qed.

Lemma type_open_tt_WFC :forall T X,
    X \notin fv_tt T ->
    type (open_tt T X) ->
    WFC T 0.
Proof with auto.
  intros.
  apply close_type_wfc in H0.
  apply close_wfc with (X:=X) in H0...
  rewrite <- close_open_reverse in H0...
Qed.

Lemma WFE_find_in: forall E k,
    WFE E k ->
    forall q n, 0 < n ->
    q < n ->
    find n E = find (n - q) (minusk E q).
Proof with auto.
  intros E k H.
  induction H;intros...
  remember (n-q).
  assert (minusk ((S k, b) :: E) q = (S k - q, b) :: (minusk E q)) as W by (simpl;auto).
  rewrite W.
  remember (S k - q).
  simpl...
  destruct (n==S k);destruct (n0==n1)...
  lia.
  lia.
  subst.
  apply IHWFE...
Qed.

Lemma bindings_WFD_drop: forall E n b q G,
    WFE E n -> q < n - b ->
    bindings_rec G E n b = bindings_rec G (minusk E q) (n - q) b.
Proof with auto.
  induction E;intros...
  dependent destruction H.
  assert (minusk ((S k, b0) :: E) q = (S k - q, b0) :: (minusk E q)) as W1 by (simpl;auto).
  rewrite W1...
  remember (S k - q).
  remember (S k).
  simpl...
  destruct (n-b == n);destruct (n0-b==n0)...
  lia.
  lia.
  subst.
  assert (S k - q - b = (S k - b) - q) as W2 by lia.
  rewrite W2.
  assert (0 < S k - b) as W3 by lia.
  remember (S k - b).
  rewrite <- WFE_find_in with (k:=k)...
Qed.

Lemma bindings_WFD_WFE: forall A k n E q G,
    WFD A k->  WFE E n -> k <= n - q -> q <= n ->
    bindings_rec G E n A = bindings_rec G (minusk E q) (n-q) A.
Proof with auto using WFE_S_n.
  intros.
  generalize dependent E.
  generalize dependent n.
  generalize dependent q.
  induction H;intros;try solve [simpl in *;auto]...
  -
    assert (q < n-b). lia.
    apply bindings_WFD_drop...
  - (* typ_mu *)
    simpl...
    f_equal.
    remember (bindings_rec G ((S (n0 - q), 1) :: minusk E q) (S (n0 - q)) A).
    assert (S (n0 - q) = (S n0) - q) as W by  lia.
    rewrite W.
    assert  ( ((S n0 - q, S n1) :: minusk E q) = minusk ((S n0, S n1)::E) q) as W2 by (simpl;auto).
    rewrite W2.
    rewrite <- IHWFD...
    f_equal...
    f_equal...
    f_equal...
    f_equal...
    subst.
    rewrite W.
    assert ((S n0 - q, 1) :: minusk E q = minusk ((S n0, 1)::E) q) as W3 by (simpl;auto).
    rewrite W3.
    rewrite <- IHWFD...
    lia.
    lia.
  - (* typ_all *)
    simpl...
    f_equal.
    rewrite <- IHWFD1... f_equal.
    replace (S (n0 - q)) with (S n0 - q) by lia.
    assert  ( ((S n0 - q, bindings_rec G E n0 A) :: minusk E q) = minusk ((S n0, bindings_rec G E n0 A)::E) q) as W2 by (simpl;auto).
    rewrite W2.
    rewrite <- IHWFD2... lia.
Qed.

Lemma find_former: forall (E2 E1:list (nat * nat)) (k:nat),
    (exists p, In (k,p) E1) ->
    find k E1 = find k (E1++E2).
Proof with auto.
  induction E1;intros...
  -
    inversion H...
    inversion H0.
  -
    destruct a.
    destruct H.
    destruct (k==n);subst...
    +
      simpl...
      destruct (n==n)...
      destruct n1...
    +
      simpl.
      destruct (k == n)...
      apply in_inv in H.
      destruct H...
      dependent destruction H...
      destruct n1...
      apply IHE1...
      exists x...
Qed.

Lemma minus_in_for_bindings: forall E ( n k:nat),
    (forall q, exists p, q < n -> In (n - q, p) E) ->
    (forall q, exists p, q < S n -> In (S n - q, p) ((S n, k) :: E)).
Proof with auto.
  intros.
  destruct n.
  -
    destruct q.
    exists k...
    intros.
    simpl...
    exists 0...
    intros.
    lia.
  -
    destruct q...
    exists k.
    intros.
    simpl...
    destruct H with (q:=q)...
    exists x.
    intros.
    assert (S (S n) - S q = S n - q).
    lia.
    rewrite H2.
    apply in_cons...
    apply H0...
    lia.
Qed.

Lemma bindings_close_env_aux: forall G A k,
    WFD A k->    forall E1 E2 ,
    (forall q, exists p, q < k -> In (k-q,p) E1) ->
    bindings_rec G (E1++E2) k A = bindings_rec G E1 k A.
Proof with eauto.
  intros G A k H.
  induction H;intros;try solve [simpl in *;auto]...
  -
    simpl...
    assert (find (k - b) E1 = find (k - b) (E1++E2)).
    {
      rewrite find_former with (E2:=E2)...
      destruct H0 with (q:=b)...
    }
    rewrite H1...
  -
    simpl.
    f_equal.
    remember (bindings_rec G ((S n, 1) :: E1 ++ E2) (S n) A).
    rewrite_env (((S n, S n0) :: E1) ++ E2).
    rewrite IHWFD...
    subst.
    rewrite_env (((S n, 1) :: E1) ++ E2).
    rewrite IHWFD...
    intros.
    apply minus_in_for_bindings...
    intros.
    apply minus_in_for_bindings...
  -
    simpl. f_equal.
    rewrite IHWFD1... f_equal.
    remember (bindings_rec G E1 n A).
    rewrite_env (((S n, n0) :: E1) ++ E2).
    rewrite IHWFD2...
    intros.
    apply minus_in_for_bindings...
Qed.

Lemma bindings_close_env: forall A E G,
    type A->
    bindings_rec G E 0 A = bindings_rec G nil 0 A.
Proof with eauto.
  intros.
  rewrite_env (nil++E).
  rewrite_env (nil ++ empty_menv).
  apply bindings_close_env_aux...
  apply close_type_wfd...
  intros.
  exists 0.
  intros.
  lia.
Qed.

Lemma bindings_local_close: forall B E n G,
  type B -> WFE E n ->
  bindings_rec G E n B = bindings_rec G nil 0 B.
Proof with auto.
  intros.
  rewrite bindings_WFD_WFE with (k:=0) (q:=n)...
  assert (0=n-n ) by lia.
  rewrite <- H1.
  rewrite bindings_close_env...
  apply close_type_wfd...
  lia.
Qed.

Lemma bindings_close : forall B a G E n,
    type B -> WFE E n ->
    bindings_rec G E n B = bindings_rec G ((S n, a) :: E) (S n) B.
Proof with auto.
  intros.
  rewrite bindings_local_close...
  remember (bindings_rec G empty_menv 0 B).
  rewrite bindings_local_close...
  apply WFE_S_n...
Qed.

Lemma bindings_rec_ge_1: forall G E n A,
  bindings_rec G E n A >= 1.
Proof.
  intros. revert E n.
  induction A;intros;simpl;try solve[lia]...
Qed.

Lemma findX_extend: forall Q G E X T n,
  WFD Q n ->
  X \notin fv_tt Q ->
  WFE E n ->
  bindings_rec (mk_benv G) E n Q =
  bindings_rec (mk_benv (X ~ T ++ G)) E n Q.
Proof with auto.
  intros. generalize dependent E.
  induction H;try solve [simpl in H0;simpl;intros;auto];intros...
  - simpl. destruct T...
    simpl. destruct (X0==X)...
    subst. exfalso.
    apply H0. simpl...
  - simpl. f_equal. destruct T...
    rewrite IHWFD... 2:{ constructor... apply WFE_find_none... }
    simpl. f_equal. f_equal. f_equal. f_equal.
    rewrite IHWFD... { constructor... apply WFE_find_none... }
  - simpl. f_equal. destruct T... simpl in H0.
    rewrite IHWFD1... f_equal.
    rewrite IHWFD2... { constructor... apply WFE_find_none... }
Qed.

Lemma findX_extend_spec: forall Q E X T,
  type Q ->
  X \notin fv_tt Q ->
  bindings_rec (mk_benv E) nil 0 Q =
  bindings_rec (mk_benv (X ~ T ++ E)) nil 0 Q.
Proof with auto.
  intros.
  apply findX_extend...
  apply close_type_wfd...
Qed.

Lemma findX_sem: forall E X Q,
  wf_env E ->
  binds X (bind_sub Q) E ->
  findX X (mk_benv E) = Some (bindings_rec (mk_benv E) nil 0 Q).
Proof with auto.
  induction E.
  - intros. inversion H0.
  - intros. destruct H0.
    + destruct a. inversion H0;subst.
      simpl. rewrite eq_dec_refl.
      f_equal. rewrite_alist (mk_benv (X ~ bind_sub Q ++ E)).
      apply findX_extend_spec...
      { inversion H;subst. apply WF_type in H5... }
      rewrite_env (nil ++ X ~ bind_sub Q ++ E) in H.
      apply notin_from_wf_env in H...
    + destruct a. simpl. destruct b...
      * simpl. destruct (X == a)...
        { subst. inversion H;subst.
          exfalso. apply H6.
          apply in_split in H0. destruct H0 as [E1 [E2 H1]].
          rewrite H1. rewrite dom_app. simpl... }
        { rewrite IHE with (Q:= Q)... 2:{ inversion H... }
          rewrite_alist (mk_benv (a ~ bind_sub t ++ E)). f_equal.
          apply findX_extend_spec...
          { inversion H;subst. apply in_split in H0. destruct H0 as [? [? ?]].
            rewrite H0 in H4. apply WF_from_binds_typ_strong in H4.
            apply WF_type in H4... }
          { rewrite_env (nil ++ a ~ bind_sub t ++ E) in H.
            apply notin_from_wf_env in H.
            assert (binds X (bind_sub Q) E)...
            apply notin_fv_tt_fv_env with (E:=E) (Y:=X)...
          }
        }
      * inversion H...
Qed.

Lemma bindings_find: forall A G E1 E2 B,
    find zero (E1++E2) = None ->
    type B ->
    WFC A 0 ->
    WFE (E1++E2)  0 ->
    (bindings_rec G (E1++E2) 0 (open_tt A B)) =
    bindings_rec G (E1 ++ (zero, (bindings_rec G (E1++E2) 0 B) - 1) :: E2) 0 A.
Proof with auto.
  intro A.
  unfold open_tt. remember 1 as one.
  generalize 0.
  unfold zero. subst one.
  induction A;intros;try solve [dependent destruction H1;simpl;auto]...
  - destruct (n0==n);subst...
    +
      assert (open_tt_rec n B n = B) as Q.
      {
        simpl...
        destruct (n==n)...
        destruct n0...
      }
      rewrite Q.
      simpl.
      rewrite Nat.sub_diag.
      rewrite bindings_find_in...
      pose proof bindings_rec_ge_1 G (E1 ++ E2) n B.
      lia.
    +
      assert (open_tt_rec n0 B n = n) as Q.
      {
        simpl...
        destruct (n0==n)...
        destruct e...
        destruct n1...
      }
      rewrite Q.
      simpl.
      dependent destruction H1.
      apply neq_minus in H1...
      destruct H1...
      rewrite H1.
      erewrite <- bindings_find_notin...
  - (* all *)
    dependent destruction H1.
    simpl. f_equal.
    rewrite IHA1... f_equal.
    remember ((S n,
    bindings_rec G (E1 ++ (0, bindings_rec G (E1 ++ E2) n B - 1) :: E2) n A1)) as R1.
    assert (bindings_rec G (E1++E2) n B = bindings_rec G (R1 :: E1++E2) (S n) B) as Q1.
    subst.
    apply bindings_close...
    rewrite Q1.
    rewrite_alist ((R1 :: E1) ++ (0, bindings_rec G ((R1 :: E1) ++ E2) (S n) B - 1) :: E2).
    rewrite <- IHA2...
    rewrite_alist (R1 :: E1 ++E2)...
    subst...
    rewrite_env (R1 :: E1 ++ E2).
    subst.
    apply WFE_S_n...

  -
    dependent destruction H1...
    simpl.
    f_equal.
    remember (S n, S
      (bindings_rec G
         ((S n, 1) :: E1 ++ (0, bindings_rec G (E1 ++ E2) n B - 1) :: E2)
         (S n) A)) as R1.
    assert (bindings_rec G (E1++E2) n B = bindings_rec G (R1 :: E1++E2) (S n) B) as Q1.
    subst.
    apply bindings_close...
    rewrite Q1.
    rewrite_alist ((R1 :: E1) ++ (0, bindings_rec G ((R1 :: E1) ++ E2) (S n) B - 1) :: E2).
    rewrite <- IHA...
    f_equal...
    remember (bindings_rec G ((S n, 0) :: E1 ++ E2) (S n) (open_tt_rec (S n) B A)) as R2.
    rewrite_alist (R1 :: E1 ++ E2).
    f_equal.
    subst.
    f_equal...
    f_equal.
    assert (bindings_rec G (E1++E2) n B = bindings_rec G (((S n, 1) :: E1)++E2) (S n) B) as Q2.
    apply bindings_close...
    rewrite Q2.
    rewrite_alist (((S n, 1) :: E1) ++ (0, bindings_rec G (((S n, 1) :: E1) ++ E2) (S n) B - 1) :: E2).
    rewrite <- IHA...
    rewrite_env ((S n, 1) :: E1 ++ E2).
    apply WFE_S_n...
    rewrite_alist (R1 :: E1 ++E2)...
    subst...
    rewrite_env (R1 :: E1 ++ E2).
    subst.
    apply WFE_S_n...
Qed.

Lemma bindings_find_spec: forall A G E B,
  find zero E = None ->
  type B ->
  WFC A 0 ->
  WFE E 0 ->
  bindings_rec
    (mk_benv G) E 0 (open_tt A B) =
  bindings_rec
    (mk_benv G) ((zero, (bindings_rec (mk_benv G) E 0 B - 1)) :: E) 0 A.
Proof with auto.
  intros.
  rewrite_env (nil ++ (zero, (bindings_rec (mk_benv G) E 0 B - 1)) :: E).
  rewrite_env (nil ++ E).
  apply bindings_find...
Qed.

(* minus one because we add one to each lookup *)
Lemma bindings_find_spec': forall A G B,
  type B ->
  WFC A 0 ->
  bindings_rec
    (mk_benv G) empty_menv 0 (open_tt A B) =
  bindings_rec
    (mk_benv G) ((1, (bindings_rec (mk_benv G) empty_menv 0 B - 1)) :: empty_menv) 1 A.
Proof with auto.
  intros.
  rewrite bindings_find_spec...
  rewrite bindings_add...
Qed.

Lemma bindings_fvar: forall A G E1 E2 X B,
    WFC A 0 ->
    X \notin fv_tt A ->
    wf_env (X ~ bind_sub B ++ G) ->
    find zero (E1++E2) = None ->
    type B ->
    WFE (E1 ++ E2) 0 ->
    bindings_rec (mk_benv (X ~ bind_sub B ++ G)) (E1 ++ E2) 0 (open_tt A X) =
    bindings_rec (mk_benv G)
    (E1 ++ [(zero, bindings_rec (mk_benv G) (E1 ++ E2) 0 B )] ++ E2) 0 A.
Proof with auto.
  intro A.
  unfold open_tt.
  generalize 0.
  unfold zero.
  induction A;intros;try solve [dependent destruction H;simpl;auto]...

  -
    destruct (n0==n);subst...
    +
      assert (open_tt_rec n X n = X) as Q.
      {
        simpl...
        destruct (n==n)...
        destruct n0...
      }
      rewrite Q.
      simpl. destruct (X == X)... 2:{ exfalso... }
      rewrite Nat.sub_diag.
      rewrite bindings_find_in...
      rewrite <- bindings_local_close with (E:=E1 ++ E2) (n:=n)...

    +
      assert (open_tt_rec n0 X n = n) as Q.
      {
        simpl...
        destruct (n0==n)...
        destruct e...
        destruct n1...
      }
      rewrite Q.
      simpl.
      dependent destruction H.
      apply neq_minus in H...
      destruct H...
      rewrite H.
      erewrite <- bindings_find_notin...

  -
    simpl. destruct (a == X)...
    subst X. exfalso. apply H0... simpl...

  -
    simpl.
    dependent destruction H. simpl in H1.
    simpl in IHA1. rewrite IHA1...
    simpl in IHA2. rewrite IHA2...

  -
    simpl.
    dependent destruction H. simpl in H1.
    simpl in IHA1. rewrite IHA1... f_equal. f_equal.

    remember (bindings_rec (mk_benv G) (E1 ++ (0, bindings_rec (mk_benv G) (E1 ++ E2) n B) :: E2) n A1) as K.

    rewrite_env (
      ((S n, K)
      :: E1) ++ E2
    ).
    simpl in IHA2. rewrite IHA2 at 1...

    2:{ constructor... apply WFE_find_none... }

    rewrite_alist ((S n, K) :: (E1 ++ E2)).
    rewrite <- bindings_close with (B:=B)...

  -
    simpl.
    dependent destruction H. simpl in H0.
    f_equal.

    remember (S (bindings_rec ((X, bindings_rec (mk_benv G) empty_menv 0 B) :: mk_benv G) ((S n, 1) :: E1 ++ E2) (S n) (open_tt_rec (S n) X A))) as K1.

    remember (S
    (bindings_rec (mk_benv G)
       ((S n, 1) :: E1 ++ (0, bindings_rec (mk_benv G) (E1 ++ E2) n B) :: E2)
       (S n) A))  as K2.

    rewrite_env (
      ((S n, K1)
      :: E1) ++ E2
    ). simpl in IHA. rewrite IHA...
    2:{ constructor... apply WFE_find_none... }

    rewrite_alist ((S n, K1) :: (E1 ++ E2)).
    rewrite <- bindings_close with (B:=B)... simpl.
    f_equal. f_equal. f_equal. subst K1 K2.
    f_equal.

    rewrite_alist (((S n, 1) :: E1) ++ E2).
    rewrite IHA...
    2:{ constructor... apply WFE_find_none... }

    rewrite_alist ((S n, 1) :: (E1 ++ E2)).
    rewrite <- bindings_close with (B:=B)...

  - simpl. f_equal. simpl in IHA. simpl in H0.
    rewrite IHA... inversion H...
Qed.

Lemma bindings_fvar_spec: forall G A X B,
    WFC A 0 ->
    X \notin fv_tt A ->
    wf_env (X ~ bind_sub B ++ G) ->
    (* find zero (E1++E2) = None -> *)
    type B ->
    bindings_rec (mk_benv (X ~ bind_sub B ++ G)) empty_menv 0 (open_tt A X) =
    bindings_rec (mk_benv G)
    ((1, bindings_rec (mk_benv G) empty_menv 0 B ) :: empty_menv) 1 A.
Proof with auto.
  intros.
  rewrite_env (X ~ bind_sub B ++ G).
  rewrite_env (empty_menv ++ empty_menv).
  rewrite bindings_fvar...
  { simpl. rewrite bindings_add... }
Qed.

Lemma binds_key_dec: forall (E: env) X,
  {Q | binds X Q E} + {forall Q, ~ binds X Q E}.
Proof with auto.
induction E...
intros.
destruct a.
destruct (X==a)...
-
  subst. left. exists b. simpl...
-
  destruct IHE with (X:=X)...
  + destruct s. left. exists x. simpl...
  + right. intros. intros C. destruct C.
    * inversion H...
    * apply n0 with (Q:=Q)...
Qed.

Lemma WFC_WFD_S : forall A k,
    WFC A k -> WFD A (S k).
Proof with auto.
  intros.
  induction H...
  constructor. lia.
Qed.

Inductive sub_menv: menv -> menv -> Prop :=
| sub_menv_nil : sub_menv empty_menv empty_menv
| sub_menv_cons : forall n v1 v2 R1 R2,
    v1 <= v2 ->
    sub_menv R1 R2 ->
    sub_menv ((n, v1) :: R1) ((n, v2) :: R2).

Hint Constructors sub_menv : core.

Lemma sub_menv_find : forall R1 R2 n,
  sub_menv R1 R2 ->
  match find n R1 with
| Some k => k
| None => 1
  end <= match find n R2 with
       | Some k => k
       | None => 1
  end.
Proof with auto.
  intros.
  induction H.
  - simpl...
  - simpl in *. destruct (n == n0)...
Qed.

Lemma sub_menv_sem: forall G R1 R2 n A,
  sub_menv R1 R2 ->
  bindings_rec G R1 n A <= bindings_rec G R2 n A.
Proof with auto.
  intros. revert n R1 R2 H.
  induction A;intros...
  - simpl. apply le_n_S. apply sub_menv_find...
  - simpl. specialize (IHA1 n _ _ H).
    specialize (IHA2 n _ _ H). lia.
  - simpl.
    specialize (IHA1 n _ _ H).
    assert (sub_menv
      ((S n, (bindings_rec G R1 n A1)) :: R1)
      ((S n, (bindings_rec G R2 n A1)) :: R2)).
    { constructor... }
    specialize (IHA2 (S n) _ _ H0).
    lia.
  - simpl.
    assert (sub_menv ((S n, 1) :: R1) ((S n, 1) :: R2))...
    pose proof IHA (S n) _ _ H0.
    assert (sub_menv
    (((S n, S (bindings_rec G ((S n, 1) :: R1) (S n) A)) :: R1))
    (((S n, S (bindings_rec G ((S n, 1) :: R2) (S n) A)) :: R2))
    )...
    { constructor... lia. }
    pose proof IHA (S n) _ _ H2. lia.
  - simpl. specialize (IHA n _ _ H). lia.
Qed.

Ltac solve_right_dec := right;intro v;inversion v;auto.

Lemma WFC_dec : forall m A,
  {WFC A m} + {~ WFC A m}.
Proof with auto.
  intros. revert m.
  induction A;intros...
  - destruct (le_gt_dec n m)...
    right. intros C. inversion C;lia.
  - destruct (IHA1 m); try solve [solve_right_dec].
    destruct (IHA2 m); try solve [solve_right_dec]...
  - destruct (IHA1 m); try solve [solve_right_dec].
    destruct (IHA2 (S m)); try solve [solve_right_dec]...
  - destruct (IHA (S m)); try solve [solve_right_dec]...
  - destruct (IHA m); try solve [solve_right_dec]...
Qed.

Lemma wf_fvar_dec: forall E (a:atom),
  uniq E ->
  {WF E a} + {~ WF E a}.
Proof with auto.
  intros.
  pose proof binds_key_dec E a.
  destruct H0.
  { destruct s. destruct x.
    * left. apply WF_var with (U:=t)...
    * right. intros C. inversion C;subst.
      pose proof binds_unique _ _ _ _ _ b H2 H.
      inversion H0.
  }
  { right. intros C.
    inversion C;subst.
    apply n with (Q:=bind_sub U)...
  }
Qed.

Lemma findX_notin: forall G X,
    X \notin dom G ->
    findX X G = None.
Proof with auto.
  induction G;intros...
  simpl in *.
  destruct a.
  destruct (X==a)...
  apply notin_add_1 in H.
  destruct H...
Qed.

Lemma wf_dec_aux : forall G k A E,
  uniq E ->
  (* new constraint,
    to show (binds a typ) -> (binds a sub) -> False

    uniq should be decidable, indeed
  *)
    bindings_rec G nil 0 A <= k ->
    {WF E A} + {~ WF E A}.
Proof with auto.
  induction k.
  -
    induction A;intros;try solve [unfold bindings in *;simpl in *;lia]...
(*
    + (* bvar *)
      right. intros C. inversion C.
    + (* fvar *)
      apply wf_fvar_dec...
       *)
  -
    unfold bindings in *.
    induction A;intros;try solve [ solve_right_dec]...
    + (* fvar *)
      apply wf_fvar_dec...

    + (* arrow *)
      simpl in H0.
      destruct IHA1 with (E:=E);destruct IHA2 with (E:=E);try solve [lia|solve_right_dec]...

    + (* all *)
      simpl in H0.
      destruct IHA1 with (E:=E);try solve [lia|solve_right_dec]...
      assert (type A1). { apply WF_type with (E:=E)... }
      destruct (WFC_dec 0 A2).
      2:{ right. intros C. apply WF_type in C.
          inversion C;subst. apply n.
          pick_fresh X.
          apply type_open_tt_WFC with (X:=X)... }

      pick fresh X.
      remember (open_tt A2 X) as Q1.
      destruct IHk with (A:=Q1) (E:= X ~ bind_sub A1 ++ E)...
      { subst. rewrite_alist (empty_menv ++ empty_menv).
        rewrite bindings_find...
        rewrite bindings_add... unfold zero. simpl.
        simpl.

        eapply le_trans.
        { apply sub_menv_sem with
            (R2:=((1, bindings_rec G empty_menv 0 A1) :: empty_menv)).
          constructor...
          rewrite findX_notin...
          simpl.
          apply bindings_rec_ge_1. }
        lia.
      }
      * (* A2 is well formed *)
        left. apply WF_all with (L:={{X}} \u fv_tt A2 \u dom E)...
        intros. subst Q1.
        apply WF_replacing_var with (X:=X)...

      * (* A2 is not well formed *)
        right. intros C. apply n. subst Q1.
        dependent destruction C. pick_fresh Y.
        specialize_x_and_L Y L.
        apply WF_replacing_var with (X:=Y)...

    + (* mu *)
      simpl in H0.

      destruct (WFC_dec 0 A).
      2:{ right. intros C. apply WF_type in C.
          inversion C;subst. apply n.
          pick_fresh X.
          apply type_open_tt_WFC with (X:=X)... }

      pick fresh X.
      remember (open_tt A X) as Q1.
      remember (open_tt A (typ_label X (open_tt A X))) as Q2.
      destruct IHk with (A:=Q1) (E:= X ~ bind_sub typ_top ++ E)...
      { subst. rewrite_alist (empty_menv ++ empty_menv).
        rewrite bindings_find...
        rewrite bindings_add... unfold zero. simpl.
        simpl.
        eapply le_trans.
        { apply sub_menv_sem with
            (R2:=((1, S (bindings_rec G ((1, 1) :: empty_menv) 1 A)) :: empty_menv)).
          constructor...
          rewrite findX_notin...
          lia. }
        lia. }

      * (* open_tt A X is well-formed  *)
        destruct IHk with (A:=Q2) (E:= X ~ bind_sub typ_top ++ E)...
        { subst. rewrite_alist (empty_menv ++ empty_menv).
          rewrite bindings_find...
          2:{ apply WF_type in w0... }
          simpl.
          replace (bindings_rec G empty_menv 0 (open_tt A X))
          with (bindings_rec G ((1,  match findX X G with
          | Some k => k | None => 1 end )::empty_menv) 1 A).
          2:{ rewrite_alist (empty_menv ++ empty_menv).
            rewrite bindings_find... simpl.
            rewrite bindings_add with (n:=0)... unfold zero...
            rewrite Nat.sub_0_r... }
          rewrite bindings_add with (n:=0)...
          simpl. unfold zero.
          apply le_S_n in H0.
          eapply le_trans. 2:{ apply H0. }
          apply sub_menv_sem.
          constructor...
          rewrite findX_notin...
          lia. }

          ** (*  A [X |-> {x: A}] is well-formed *)
           left. subst Q1 Q2.
           apply WF_rec with (L:={{X}} \u fv_tt A \u dom E \u fl_tt A);intros...
           apply WF_replacing_var with (X:=X)...

           apply WF_replacing' with (Y:=X0) in w1...
           rewrite subst_tt_open_tt in w1... simpl in w1.
           rewrite subst_tt_open_tt in w1... simpl in w1.
           rewrite eq_dec_refl in w1.
           rewrite <- subst_tt_fresh in w1...
           (* stuck: how to get
           WF (X0 ~ bind_sub typ_top ++ E)
              (open_tt A (typ_label X0 (open_tt A X0)))

           from

           WF ((X0, bind_sub typ_top) :: E)
             (open_tt A (typ_label X (open_tt A X0)))
            *)
           apply WF_renaming_tl with (X:=X) (Y:=X0) in w1...
           rewrite label_transform in w1...
           solve_notin.
        ** (* A [X |-> {x: A}] is not well-formed *)
           right. intros C. apply n. subst Q1 Q2.
           inversion C;subst.
           pick_fresh Y.
           specialize_x_and_L Y L.
           apply WF_renaming_unfolding with (X:=Y)...
           (* Same issue as above case *)

      * (* open_tt A X is not well-formed *)
        right. intros C. apply n. subst Q1.
        inversion C. subst.
        pick_fresh Y.
        specialize_x_and_L Y L.
        apply WF_replacing_var with (X:=Y)...

  + (* label *)
    simpl in H0.
    destruct IHA with (E:=E);try solve [lia|solve_right_dec]...
Qed.

Lemma wf_dec : forall  A E,
  uniq E ->
    {WF E A} + {~ WF E A}.
Proof with auto.
  intros.
  apply wf_dec_aux with (k:=bindings_rec nil nil 0 A) (G:=nil)...
Qed.

Lemma binds_key_dom_dec: forall (E: env) X,
  {X \in dom E} + {X \notin dom E}.
Proof with auto.
induction E...
intros.
destruct a.
destruct (X==a)...
-
  subst. left. simpl...
-
  destruct IHE with (X:=X)...
  left. simpl...
Qed.

Lemma wf_env_dec: forall E,
    {wf_env E} + {~wf_env E}.
Proof with auto.
  induction E...
  destruct IHE.
  -
    pose proof wf_dec.
    assert (Ht:=w).
    apply uniq_from_wf_env in Ht.
    pose proof binds_key_dom_dec.
    destruct a.
    destruct b.
    +
      destruct H with (E:=E) (A:=t)...
      destruct H0 with (E:=E) (X:=a)...
      *
        right.
        intros v.
        dependent destruction v...
      *
        left.
        constructor...
      *
        right.
        intros v.
        dependent destruction v...
    +
      destruct H with (E:=E) (A:=t)...
      destruct H0 with (E:=E) (X:=a)...
      *
        right.
        intros v.
        dependent destruction v...
      *
        left.
        constructor...
      *
        right.
        intros v.
        dependent destruction v...
  -
    right.
    intros v.
    dependent destruction v;
      apply n...
Qed.

Ltac solve_top_dec E :=
  pose wf_env_dec as Q;destruct Q with (E:=E) as [Ql|Qr];try solve [
  left;auto |
  solve_right_dec  ].
Ltac solve_top_wfs_dec E A :=
  match goal with
  | H : wf_env E |- _ =>
    destruct (wf_dec A (uniq_from_wf_env H));
    try solve [left;auto|right;intros v;dependent destruction v;auto]
  | _ => idtac
  end.

Lemma subtyping_dec : forall k A B E,
bindings_rec (mk_benv E) nil 0 A +
bindings_rec (mk_benv E) nil 0 B <= k ->
{sub E A B} + {~ sub E A B}.
Proof with auto.
induction k.
-
induction A;intros;try solve [unfold bindings in *;simpl in *;lia]...
-
induction A.
+
  induction B;intros;try solve [ solve_right_dec | solve_top_dec E]...

+
  induction B;intros;try solve [ solve_right_dec | solve_top_dec E]...

+
  induction B;intros;try solve [ solve_right_dec | solve_top_dec E]...
  right. intros C. inversion C;subst. inversion H1.

+
  intros. simpl in H.
  destruct (wf_env_dec E).
  2:{ right. intros C. apply sub_regular in C. destruct C... }
  destruct (binds_key_dec E a).
  *
    pose proof uniq_from_wf_env w as u.
    destruct s.
    destruct x.
    { assert (WF E t).
      { apply WF_from_binds_typ with (x:=a)... }
      apply WF_type in H0.
      rewrite (findX_sem _ _ w b) in H.
      (* 2:{ apply binds_split in b.
        destruct b as [E1 [E2 b]]. rewrite b in w.
        apply wf_env_binds_not_fv_tt in w... } *)
      apply le_S_n in H.
      destruct (IHk _ _ _ H)...
      { left. apply sa_trans_tvar with (U:=t)... }
      { destruct (EqDec_eq a B).
        { left. subst. apply sa_fvar... apply WF_var with (U:=t)... }
        destruct (EqDec_eq typ_top B).
        { left. subst. apply sa_top... apply WF_var with (U:=t)... }
        right. intros C. inversion C;subst...
        { assert (bind_sub t =  bind_sub U).
          { eapply binds_unique with (x:=a) (E:=E)... }
          inversion H1;subst... }
      }
    }
    { right. intros C. apply uniq_from_wf_env in w.
      inversion C;subst.
      { inversion H3;subst. pose proof binds_unique _ _ _ _ _ b H4 w.
        inversion H0.  }
      { inversion H1;subst. pose proof binds_unique _ _ _ _ _ b H4 w.
        inversion H2.  }
      { pose proof binds_unique _ _ _ _ _ b H1 w.
        inversion H0.  }
    }

  *
    right. intros C.
    inversion C;subst...
    { inversion H3;subst. apply n in H4... }
    { inversion H1;subst. apply n in H4... }
    { apply n in H1... }

+ intros. simpl in H.
  induction B;intros;try solve [ solve_right_dec | solve_top_dec E]...
  * solve_top_dec E. solve_top_wfs_dec E (typ_arrow A1 A2).

  *
    simpl in H.
    destruct IHk with (A:=B1) (B:=A1) (E:=E); try solve [lia];
    destruct IHk with (A:=A2) (B:=B2) (E:=E);try solve [lia];
    try solve [solve_right_dec].
    left. apply sa_arrow...

+
  intros. simpl in H.
  induction B;intros;try solve [ solve_right_dec]...
  * solve_top_dec E. solve_top_wfs_dec E (typ_all A1 A2).

  *
    destruct (EqDec_eq A1 B1);try solve [solve_right_dec].
    subst B1. rename A1 into A.
    rename A2 into B1.

    destruct (wf_env_dec E).
    2:{ right. intros C. apply sub_regular in C. destruct C as [? [? ?]]... }
    pose proof uniq_from_wf_env w as u.
    destruct (wf_dec A u);try solve [solve_right_dec].

    pick_fresh X1. assert (uniq ((X1 ~ bind_sub A) ++ E)) as u2...
    destruct (wf_dec (open_tt B1 X1) u2).
    2:{ right. intros C.
        apply sub_regular in C. destruct C as [? [? ?]].
        inversion H1;subst.
        pick_fresh X2. specialize_x_and_L X2 L.
        apply n. apply WF_replacing_var with (X:=X2)... }
    destruct (wf_dec (open_tt B2 X1) u2).
    2:{ right. intros C.
        apply sub_regular in C. destruct C as [? [? ?]].
        inversion H2;subst.
        pick_fresh X2. specialize_x_and_L X2 L.
        apply n. apply WF_replacing_var with (X:=X2)... }

    clear IHA1 IHA2 IHB1 IHB2. simpl in H.

    specialize (IHk (open_tt B1 X1) (open_tt B2 X1)
    (X1 ~ bind_sub A ++ E)).

    rewrite <- bindings_fvar_spec with (X:=X1)in H...
    2:{ apply type_open_tt_WFC with (X:=X1)... apply WF_type in w1... }
    2:{ apply WF_type in w0... }

    rewrite <- bindings_fvar_spec with (X:=X1)in H...
    2:{ apply type_open_tt_WFC with (X:=X1)... apply WF_type in w2... }
    2:{ apply WF_type in w0... }

    destruct IHk.
    { lia. }
    { left.
      apply sa_all with (L:={{X1}} \u fv_tt A \u fv_tt B1 \u fv_tt B2 \u dom E);intros...
      apply sub_replacing_var with (X:=X1)...
    }
    { right. intros. intros C.
      inversion C. subst. pick_fresh X2.
      specialize_x_and_L X2 L.
      apply n. apply sub_replacing_var with (X:=X2)... }

+
  intros. simpl in H.
  induction B;intros;try solve [ solve_right_dec]...
  * solve_top_dec E. solve_top_wfs_dec E (typ_mu A).

  *
    destruct (wf_env_dec E).
    2:{ right. intros C. apply sub_regular in C. destruct C as [? [? ?]]... }
    pose proof uniq_from_wf_env w as u.

    pick_fresh X1. assert (uniq ((X1 ~ bind_sub typ_top) ++ E)) as u2...

    destruct (wf_dec (open_tt A X1) u2).
    2:{ right. intros C. apply n.
        inversion C. subst.
        pick_fresh X2. specialize_x_and_L X2 L.
        apply WF_replacing_var with (X:=X2)... }
    destruct (wf_dec (open_tt B X1) u2).
    2:{ right. intros C. apply n.
        inversion C. subst.
        pick_fresh X2. specialize_x_and_L X2 L.
        apply WF_replacing_var with (X:=X2)... }

    clear IHA IHB. simpl in H.

    specialize (IHk (open_tt A (typ_label X1 (open_tt A X1)))
    (open_tt B (typ_label X1 (open_tt B X1)))
    (X1 ~ bind_sub typ_top ++ E)).

    assert (WFC A 0). { apply WF_type in w0. apply type_open_tt_WFC in w0... }
    assert (WFC B 0). { apply WF_type in w1. apply type_open_tt_WFC in w1... }

    rewrite bindings_find_spec'
      with (A:=A) (B:= typ_label X1 (open_tt A X1)) in IHk...
    2:{ constructor. apply WF_type in w0... }
    rewrite bindings_find_spec'
      with (A:=B) (B:= typ_label X1 (open_tt B X1)) in IHk...
    2:{ constructor. apply WF_type in w1... }

    assert (Haux: forall G E n A X,
      bindings_rec G E n (typ_label X A) = S (bindings_rec G E n A))...
    rewrite !Haux in IHk. clear Haux.

    rewrite bindings_fvar_spec in IHk...
    rewrite bindings_fvar_spec in IHk...

    rewrite <- findX_extend in IHk...
    2:{ apply WFC_WFD_S... }
    rewrite <- findX_extend in IHk...
    2:{ apply WFC_WFD_S... }

    destruct IHk.
    { apply le_S_n in H. eapply le_trans;[|apply H].
      apply plus_le_compat.
      { apply sub_menv_sem. constructor...
        simpl. lia. }
      { apply le_S. apply sub_menv_sem.
        constructor... simpl. lia. }
    }

    { left.
      apply sa_rec with (L:={{X1}} \u fv_tt A \u fv_tt B \u dom E \u fl_tt A \u fl_tt B);intros...
      { apply WF_replacing_var with (X:=X1)... }
      { apply WF_replacing_var with (X:=X1)... }
      {
        apply sub_renaming_unfolding with (X:=X1)...
      }
    }
    { right. intros. intros C.
      inversion C. subst. pick_fresh X2.
      specialize_x_and_L X2 L.
      apply n. simpl.
      apply sub_renaming_unfolding with (X:=X2)...
    }

+
  intros. simpl in H.
  induction B;intros;try solve [ solve_right_dec]...
  * solve_top_dec E. solve_top_wfs_dec E (typ_label a A).

  *
    simpl in H. destruct IHk with (A:=A) (B:=B) (E:=E).
    { lia. }

    { destruct (a == a0).
      + subst. constructor...
      + right. intros C. inversion C;subst... }
    { right. intros C. inversion C;subst... }
Qed.

Lemma decidability : forall A B E,
{sub E A B} + {~ sub E A B}.
Proof with auto.
  intros.
  apply subtyping_dec with (k:=bindings_rec (mk_benv E) nil 0 A +
                               bindings_rec (mk_benv E) nil 0 B )...
Qed.

author: juda

repo: Recursive-Subtyping-for-All


text:
Require Coq.extraction.Extraction.
Extraction Language Haskell.

Require Import ExtrHaskellBasic.

From TinyRAM.Machine Require Import
     Parameters Handlers.
Import PeanoNat.Nat BinNat.

(* Example archetecture with 4 registers and a wordsize of 16 bits. *)
Module SixteenFour <: TinyRAMParameters.
  Definition wordSizeEighth : nat := 2.
  Definition registerCount : nat := 4.
  Definition wordSize := wordSizeEighth * 8.
  Definition wordSizeLength : nat := 4.
  Theorem wordSizePow2 : wordSize = 2 ^ wordSizeLength.
  Proof. unfold wordSize. simpl. reflexivity. Qed.
  Theorem encodingAxiom : 6 + 2 * log2_up registerCount <= wordSize.
  Proof. unfold registerCount. unfold wordSize. simpl.
         repeat (apply le_S; try apply le_n). Qed.
End SixteenFour.

Module TRHand := TinyRAMHandlers SixteenFour.
Import TRHand.

Extract Inductive Datatypes.nat => "Prelude.Integer" ["0" "succ"]
 "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
Extract Inductive positive => "Prelude.Integer" [ "((1 Prelude.+) GHC.Base.. (2 Prelude.*))" "(2 Prelude.*)" "1" ]
 "(\fxI fxO xH n -> if n Prelude.== 1 then xH () else
    ( if (Prelude.mod n 2) Prelude.== 1
      then fxI (Prelude.div (n Prelude.- 1) 2)
      else fxO (Prelude.div n 2)
    )
  )".
Extract Inductive N => "Prelude.Integer" [ "0" "GHC.Base.id" ]
 "(\fZ fP n -> if n Prelude.== 0 then fZ () else fP n)".
Extract Inductive Z => "Prelude.Integer" [ "0" "GHC.Base.id" "(0 Prelude.-)" ]
 "(\fZ fP fN n -> if n Prelude.== 0 then fZ () else
    ( if n Prelude.> 0
      then fP n
      else fN (Prelude.abs n)
    )
  )".
Extract Inductive comparison => "Prelude.Ordering" [ "Prelude.EQ" "Prelude.LT" "Prelude.GT" ].
Extract Inductive VectorDef.t => "([])" [ "[]" "(\x _ xs -> x : xs)" ]
  "(\fnil fcons v ->
     case v of
       [] -> fnil ()
       (x : xs) -> fcons x (Prelude.toInteger (Prelude.length xs)) xs)".

Extraction "Tinyram_VM.hs" interp_program_for.

author: Orbis-Tertius

repo: coq-tinyram


text:
(** ******************************************

Direct implementation of binary coproducts togther with:

- Proof that binary coproduct(cocone) is a property in a univalent_category ([isaprop_BinCoproductCocone])
- Specialized versions of beta rules for coproducts
- Definition of binary coproduct functor ([bincoproduct_functor])
- Definition of a coproduct structure on a functor category by taking pointwise coproducts in the
  target category ([BinCoproducts_functor_precat])
- Definition of the option functor ([option_functor])
- Binary coproducts from colimits ([BinCoproducts_from_Colims])
- Equivalent universal property: (A --> C) × (B --> C) ≃ (A + B --> C)
- The type of coproducts on a given diagram is a proposition
- Associativity
- Distribution over a functor

Written by Benedikt Ahrens, March 2015
Extended by Anders Mörtberg and Tomi Pannila, 2016
Extended by Langston Barrett (@siddharthist), 2018
Extended by Ralph Matthes, 2023

*********************************************)

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.PartA.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.MoreFoundations.WeakEquivalences.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.limits.zero.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.coproducts.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.ProductCategory.

Local Open Scope cat.

Local Open Scope cat.

(** * Definition of binary coproduct of objects in a precategory *)
Section coproduct_def.

Context (C : category).

Definition isBinCoproduct (a b co : C) (ia : a --> co) (ib : b --> co) :=
  ∏ (c : C) (f : a --> c) (g : b --> c),
  ∃! (fg : co --> c), (ia · fg = f) × (ib · fg = g).

Lemma isaprop_isBinCoproduct {a b co : C} {ia : a --> co} {ib : b --> co} :
  isaprop (isBinCoproduct a b co ia ib).
Proof.
  apply impred_isaprop. intros t.
  apply impred_isaprop. intros t0.
  apply impred_isaprop. intros g.
  apply isapropiscontr.
Qed.

Definition BinCoproduct (a b : C) :=
   ∑ coiaib : (∑ co : C, a --> co × b --> co),
      isBinCoproduct a b (pr1 coiaib) (pr1 (pr2 coiaib)) (pr2 (pr2 coiaib)).

Definition BinCoproducts := ∏ (a b : C), BinCoproduct a b.
Definition hasBinCoproducts := ∏ (a b : C), ∥ BinCoproduct a b ∥.

Definition BinCoproductObject {a b : C} (CC : BinCoproduct a b) : C := pr1 (pr1 CC).
Coercion BinCoproductObject : BinCoproduct >-> ob.
Definition BinCoproductIn1 {a b : C} (CC : BinCoproduct a b): a --> BinCoproductObject CC :=
  pr1 (pr2 (pr1 CC)).
Definition BinCoproductIn2 {a b : C} (CC : BinCoproduct a b) : b --> BinCoproductObject CC :=
   pr2 (pr2 (pr1 CC)).

Definition isBinCoproduct_BinCoproduct {a b : C} (CC : BinCoproduct a b) :
   isBinCoproduct a b  (BinCoproductObject CC) (BinCoproductIn1 CC) (BinCoproductIn2 CC).
Proof.
  exact (pr2 CC).
Defined.

Definition BinCoproductArrow {a b : C} (CC : BinCoproduct a b)
  {c : C} (f : a --> c) (g : b --> c) : BinCoproductObject CC --> c.
Proof.
  exact (pr1 (pr1 (isBinCoproduct_BinCoproduct CC _ f g))).
Defined.

Lemma BinCoproductIn1Commutes (a b : C) (CC : BinCoproduct a b):
     ∏ (c : C) (f : a --> c) g, BinCoproductIn1 CC · BinCoproductArrow CC f g  = f.
Proof.
  intros c f g.
  exact (pr1 (pr2 (pr1 (isBinCoproduct_BinCoproduct CC _ f g)))).
Qed.

Lemma BinCoproductIn2Commutes (a b : C) (CC : BinCoproduct a b):
     ∏ (c : C) (f : a --> c) g, BinCoproductIn2 CC · BinCoproductArrow CC f g = g.
Proof.
  intros c f g.
  exact (pr2 (pr2 (pr1 (isBinCoproduct_BinCoproduct CC _ f g)))).
Qed.

Lemma BinCoproductArrowUnique (a b : C) (CC : BinCoproduct a b) (x : C)
    (f : a --> x) (g : b --> x) (k : BinCoproductObject CC --> x) :
    BinCoproductIn1 CC · k = f → BinCoproductIn2 CC · k = g →
      k = BinCoproductArrow CC f g.
Proof.
  intros H1 H2.
  set (H := tpair (λ h, dirprod _ _ ) k (make_dirprod H1 H2)).
  set (H' := (pr2 (isBinCoproduct_BinCoproduct CC _ f g)) H).
  apply (base_paths _ _ H').
Qed.

Lemma BinCoproductArrowsEq (c d : C) (CC : BinCoproduct c d) (x : C)
      (k1 k2 : BinCoproductObject CC --> x) :
  BinCoproductIn1 CC · k1 = BinCoproductIn1 CC · k2 ->
  BinCoproductIn2 CC · k1 = BinCoproductIn2 CC · k2 ->
  k1 = k2.
Proof.
  intros H1 H2.
  set (p1 := BinCoproductIn1 CC · k1).
  set (p2 := BinCoproductIn2 CC · k1).
  rewrite (BinCoproductArrowUnique _ _ CC _ p1 p2 k1).
  apply pathsinv0.
  apply BinCoproductArrowUnique.
  unfold p1. apply pathsinv0. apply H1.
  unfold p2. apply pathsinv0. apply H2.
  apply idpath. apply idpath.
Qed.

Lemma BinCoproductArrowEta (a b : C) (CC : BinCoproduct a b) (x : C)
    (f : BinCoproductObject CC --> x) :
    f = BinCoproductArrow CC (BinCoproductIn1 CC · f) (BinCoproductIn2 CC · f).
Proof.
  apply BinCoproductArrowUnique;
  apply idpath.
Qed.

Definition BinCoproductOfArrows {a b : C} (CCab : BinCoproduct a b) {c d : C}
    (CCcd : BinCoproduct c d) (f : a --> c) (g : b --> d) :
          BinCoproductObject CCab --> BinCoproductObject CCcd :=
    BinCoproductArrow CCab (f · BinCoproductIn1 CCcd) (g · BinCoproductIn2 CCcd).

Lemma BinCoproductOfArrowsIn1 {a b : C} (CCab : BinCoproduct a b) {c d : C}
    (CCcd : BinCoproduct c d) (f : a --> c) (g : b --> d) :
    BinCoproductIn1 CCab · BinCoproductOfArrows CCab CCcd f g = f · BinCoproductIn1 CCcd.
Proof.
  unfold BinCoproductOfArrows.
  apply BinCoproductIn1Commutes.
Qed.

Lemma BinCoproductOfArrowsIn2 {a b : C} (CCab : BinCoproduct a b) {c d : C}
    (CCcd : BinCoproduct c d) (f : a --> c) (g : b --> d) :
    BinCoproductIn2 CCab · BinCoproductOfArrows CCab CCcd f g = g · BinCoproductIn2 CCcd.
Proof.
  unfold BinCoproductOfArrows.
  apply BinCoproductIn2Commutes.
Qed.

Definition make_BinCoproduct (a b : C) :
  ∏ (c : C) (f : a --> c) (g : b --> c),
   isBinCoproduct _ _ _ f g →  BinCoproduct a b.
Proof.
  intros.
  use tpair.
  - exists c.
    exists f.
    exact g.
  - apply X.
Defined.

Definition make_isBinCoproduct (hsC : has_homsets C) (a b co : C)
   (ia : a --> co) (ib : b --> co) :
   (∏ (c : C) (f : a --> c) (g : b --> c),
    ∃! k : C ⟦co, c⟧,
      ia · k = f ×
      ib · k = g)
   → isBinCoproduct a b co ia ib.
Proof.
  intros H c cc.
  apply H.
Defined.

Lemma precompWithBinCoproductArrow {a b : C} (CCab : BinCoproduct a b) {c d : C}
    (CCcd : BinCoproduct c d) (f : a --> c) (g : b --> d)
    {x : C} (k : c --> x) (h : d --> x) :
        BinCoproductOfArrows CCab CCcd f g · BinCoproductArrow CCcd k h =
         BinCoproductArrow CCab (f · k) (g · h).
Proof.
  apply BinCoproductArrowUnique.
  - rewrite assoc. rewrite BinCoproductOfArrowsIn1.
    rewrite <- assoc, BinCoproductIn1Commutes.
    apply idpath.
  - rewrite assoc, BinCoproductOfArrowsIn2.
    rewrite <- assoc, BinCoproductIn2Commutes.
    apply idpath.
Qed.

Lemma postcompWithBinCoproductArrow {a b : C} (CCab : BinCoproduct a b) {c : C}
    (f : a --> c) (g : b --> c) {x : C} (k : c --> x)  :
       BinCoproductArrow CCab f g · k = BinCoproductArrow CCab (f · k) (g · k).
Proof.
  apply BinCoproductArrowUnique.
  -  rewrite assoc, BinCoproductIn1Commutes;
     apply idpath.
  -  rewrite assoc, BinCoproductIn2Commutes;
     apply idpath.
Qed.

Lemma BinCoproduct_endo_is_identity {a b : C} (CC : BinCoproduct a b)
  (k : BinCoproductObject CC --> BinCoproductObject CC)
  (H1 : BinCoproductIn1 CC · k = BinCoproductIn1 CC)
  (H2 : BinCoproductIn2 CC · k = BinCoproductIn2 CC)
  : identity _ = k.
Proof.
  set (H' := pr2 CC _ (BinCoproductIn1 CC) (BinCoproductIn2 CC) ); simpl in *.
  set (X := (∑ fg : pr1 (pr1 CC) --> BinCoproductObject CC,
          pr1 (pr2 (pr1 CC))· fg = BinCoproductIn1 CC
          × pr2 (pr2 (pr1 CC))· fg = BinCoproductIn2 CC)).
  set (t1 := tpair _ k (make_dirprod H1 H2) : X).
  set (t2 := tpair _ (identity _ ) (make_dirprod (id_right _ ) (id_right _ ) ) : X).
  assert (X' : t1 = t2).
  { apply proofirrelevancecontr. apply H'. }
  apply pathsinv0.
  apply (base_paths _ _ X').
Qed.

Definition from_BinCoproduct_to_BinCoproduct {a b : C} (CC CC' : BinCoproduct a b)
  : BinCoproductObject CC --> BinCoproductObject CC'.
Proof.
  apply (BinCoproductArrow CC  (BinCoproductIn1 _ ) (BinCoproductIn2 _ )).
Defined.

Lemma is_inverse_from_BinCoproduct_to_BinCoproduct {a b : C} (CC CC' : BinCoproduct a b) :
  is_inverse_in_precat (from_BinCoproduct_to_BinCoproduct CC CC')
    (from_BinCoproduct_to_BinCoproduct CC' CC).
Proof.
  split; simpl.
  - apply pathsinv0.
    apply BinCoproduct_endo_is_identity.
    + rewrite assoc. unfold from_BinCoproduct_to_BinCoproduct.
      rewrite BinCoproductIn1Commutes.
      rewrite BinCoproductIn1Commutes.
      apply idpath.
    + rewrite assoc. unfold from_BinCoproduct_to_BinCoproduct.
      rewrite BinCoproductIn2Commutes.
      rewrite BinCoproductIn2Commutes.
      apply idpath.
  - apply pathsinv0.
    apply BinCoproduct_endo_is_identity.
    + rewrite assoc; unfold from_BinCoproduct_to_BinCoproduct.
      repeat rewrite BinCoproductIn1Commutes; apply idpath.
    + rewrite assoc; unfold from_BinCoproduct_to_BinCoproduct.
      repeat rewrite BinCoproductIn2Commutes; apply idpath.
Qed.

Lemma is_z_iso_from_BinCoproduct_to_BinCoproduct {a b : C} (CC CC' : BinCoproduct a b)
  : is_z_isomorphism (from_BinCoproduct_to_BinCoproduct CC CC').
Proof.
  exists (from_BinCoproduct_to_BinCoproduct CC' CC).
  apply is_inverse_from_BinCoproduct_to_BinCoproduct.
Defined.

Definition z_iso_from_BinCoproduct_to_BinCoproduct {a b : C} (CC CC' : BinCoproduct a b)
  : z_iso (BinCoproductObject CC) (BinCoproductObject CC')
  := _ ,, is_z_iso_from_BinCoproduct_to_BinCoproduct CC CC'.

End coproduct_def.

Arguments BinCoproduct [_] _ _.
Arguments BinCoproductObject [_ _ _] _ .
Arguments BinCoproductArrow [_ _ _] _ [_] _ _.
Arguments BinCoproductIn1 [_ _ _] _.
Arguments BinCoproductIn2 [_ _ _] _.

(** * Proof that coproducts are unique when the precategory [C] is a univalent_category *)

Section coproduct_unique.

Context (C : category) (H : is_univalent C) (a b : C).

Lemma isaprop_BinCoproduct : isaprop (BinCoproduct a b).
Proof.
  apply invproofirrelevance.
  intros CC CC'.
  apply subtypePath.
  + intros.
    intro. do 3 (apply impred; intro); apply isapropiscontr.
  + apply (total2_paths_f (isotoid _ H (z_iso_from_BinCoproduct_to_BinCoproduct _ CC CC'))).
    rewrite transportf_dirprod.
    rewrite transportf_isotoid'. simpl.
    rewrite transportf_isotoid'.
    destruct CC as [CC bla].
    destruct CC' as [CC' bla']; simpl in *.
    destruct CC as [CC [CC1 CC2]].
    destruct CC' as [CC' [CC1' CC2']]; simpl in *.
    unfold from_BinCoproduct_to_BinCoproduct.
    rewrite BinCoproductIn1Commutes.
    rewrite BinCoproductIn2Commutes.
    apply idpath.
Qed.

End coproduct_unique.

Section BinCoproducts.

Context (C : category) (CC : BinCoproducts C) (a b c d x y : C).

Lemma BinCoproductArrow_eq_cor (f f' : BinCoproductObject (CC a b) --> c)
  : BinCoproductIn1 _· f = BinCoproductIn1 _· f' → BinCoproductIn2 _· f = BinCoproductIn2 _· f' →
      f = f' .
Proof.
  intros Hyp1 Hyp2.
  rewrite (BinCoproductArrowEta _ _ _ _ _ f).
  rewrite (BinCoproductArrowEta _ _ _ _ _ f').
  apply maponpaths_12; assumption.
Qed.

(** specialized versions of beta rules for coproducts *)
(* all the following lemmas for manipulation of the hypothesis
Lemma BinCoproductIn1Commutes_left (f : a --> c)(g : b --> c)(h : a --> c):
  BinCoproductIn1 C (CC _ _) · BinCoproductArrow C (CC _ _) f g = h -> f = h.
Proof.
  intro Hyp.
  rewrite BinCoproductIn1Commutes in Hyp.
  exact Hyp.
Qed.

Lemma BinCoproductIn1Commutes_right (f : a --> c)(g : b --> c)(h : a --> c):
  h = BinCoproductIn1 C (CC _ _) · BinCoproductArrow C (CC _ _) f g -> h = f.
Proof.
  intro Hyp.
  rewrite BinCoproductIn1Commutes in Hyp.
  exact Hyp.
Qed.

Lemma BinCoproductIn2Commutes_left (f : a --> c)(g : b --> c)(h : b --> c):
  BinCoproductIn2 C (CC _ _) · BinCoproductArrow C (CC _ _) f g = h -> g = h.
Proof.
  intro Hyp.
  rewrite BinCoproductIn2Commutes in Hyp.
  exact Hyp.
Qed.

Lemma BinCoproductIn2Commutes_right (f : a --> c)(g : b --> c)(h : b --> c):
  h = BinCoproductIn2 C (CC _ _) · BinCoproductArrow C (CC _ _) f g -> h = g.
Proof.
  intro Hyp.
  rewrite BinCoproductIn2Commutes in Hyp.
  exact Hyp.
Qed.

Lemma BinCoproductIn1Commutes_left_in_ctx (f : a --> c)(g : b --> c)(h : c --> d)(h' : a --> d):
  BinCoproductIn1 C (CC _ _) · (BinCoproductArrow C (CC _ _) f g · h) = h' -> f · h = h'.
Proof.
  intro Hyp.
  rewrite assoc in Hyp.
  rewrite BinCoproductIn1Commutes in Hyp.
  exact Hyp.
Qed.

Lemma BinCoproductIn1Commutes_right_in_ctx (f : a --> c)(g : b --> c)(h : c --> d)(h' : a --> d):
  h' = BinCoproductIn1 C (CC _ _) · (BinCoproductArrow C (CC _ _) f g · h)  -> h' = f · h.
Proof.
  intro Hyp.
  apply pathsinv0 in Hyp.
  apply pathsinv0.
  exact (BinCoproductIn1Commutes_left_in_ctx _ _ _ _ Hyp).
Qed.

Lemma BinCoproductIn2Commutes_left_in_ctx (f : a --> c)(g : b --> c)(h : c --> d)(h' : b --> d):
  BinCoproductIn2 C (CC _ _) · (BinCoproductArrow C (CC _ _) f g · h) = h' -> g · h = h'.
Proof.
  intro Hyp.
  rewrite assoc in Hyp.
  rewrite BinCoproductIn2Commutes in Hyp.
  exact Hyp.
Qed.

Lemma BinCoproductIn2Commutes_right_in_ctx (f : a --> c)(g : b --> c)(h : c --> d)(h' : b --> d):
  h' = BinCoproductIn2 C (CC _ _) · (BinCoproductArrow C (CC _ _) f g · h)  -> h' = g · h.
Proof.
  intro Hyp.
  apply pathsinv0 in Hyp.
  apply pathsinv0.
  exact (BinCoproductIn2Commutes_left_in_ctx _ _ _ _ Hyp).
Qed.

Lemma BinCoproductIn2Commutes_right_in_double_ctx (g0 : x --> b)(f : a --> c)(g : b --> c)
 (h : c --> d)(h' : x --> d):
  h' = g0 · BinCoproductIn2 C (CC _ _) · (BinCoproductArrow C (CC _ _) f g · h)  ->
  h' = g0 · g · h.
Proof.
  intro Hyp.
  rewrite Hyp.
  repeat rewrite <- assoc.
  apply maponpaths.
  rewrite assoc.
  rewrite BinCoproductIn2Commutes.
  apply idpath.
Qed.
*)

(* optimized versions in direct style *)
Lemma BinCoproductIn1Commutes_right_dir (f : a --> c) (g : b --> c) (h : a --> c) :
  h = f -> h = BinCoproductIn1 (CC _ _) · BinCoproductArrow (CC _ _) f g.
Proof.
  intro Hyp.
  rewrite Hyp.
  apply pathsinv0.
  apply BinCoproductIn1Commutes.
Qed.

Lemma BinCoproductIn2Commutes_right_dir (f : a --> c) (g : b --> c) (h : b --> c) :
  h = g -> h = BinCoproductIn2 (CC _ _) · BinCoproductArrow (CC _ _) f g.
Proof.
  intro Hyp.
  rewrite Hyp.
  apply pathsinv0.
  apply BinCoproductIn2Commutes.
Qed.

Lemma BinCoproductIn1Commutes_right_in_ctx_dir (f : a --> c) (g : b --> c) (h : c --> d) (h' : a --> d) :
  h' = f · h -> h' = BinCoproductIn1 (CC _ _) · (BinCoproductArrow (CC _ _) f g · h).
Proof.
  intro Hyp.
  rewrite Hyp.
  rewrite assoc.
  rewrite BinCoproductIn1Commutes.
  apply idpath.
Qed.

Lemma BinCoproductIn2Commutes_right_in_ctx_dir (f : a --> c) (g : b --> c) (h : c --> d) (h' : b --> d) :
  h' = g · h -> h' = BinCoproductIn2 (CC _ _) · (BinCoproductArrow (CC _ _) f g · h).
Proof.
  intro Hyp.
  rewrite Hyp.
  rewrite assoc.
  rewrite BinCoproductIn2Commutes.
  apply idpath.
Qed.

Lemma BinCoproductIn1Commutes_left_dir (f : a --> c) (g : b --> c) (h : a --> c) :
  f = h -> BinCoproductIn1 (CC _ _) · BinCoproductArrow (CC _ _) f g = h.
Proof.
  intro Hyp.
  rewrite Hyp.
  apply BinCoproductIn1Commutes.
Qed.

Lemma BinCoproductIn2Commutes_left_dir (f : a --> c) (g : b --> c) (h : b --> c) :
  g = h -> BinCoproductIn2 (CC _ _) · BinCoproductArrow (CC _ _) f g = h.
Proof.
  intro Hyp.
  rewrite Hyp.
  apply BinCoproductIn2Commutes.
Qed.

Lemma BinCoproductIn1Commutes_left_in_ctx_dir (f : a --> c) (g : b --> c)
  (h : c --> d) (h' : a --> d) :
  f · h = h' -> BinCoproductIn1 (CC _ _) · (BinCoproductArrow (CC _ _) f g · h) = h'.
Proof.
  intro Hyp.
  rewrite <- Hyp.
  rewrite assoc.
  rewrite BinCoproductIn1Commutes.
  apply idpath.
Qed.

Lemma BinCoproductIn2Commutes_left_in_ctx_dir (f : a --> c) (g : b --> c)
  (h : c --> d) (h' : b --> d) :
  g · h = h' -> BinCoproductIn2 (CC _ _) · (BinCoproductArrow (CC _ _) f g · h) = h'.
Proof.
  intro Hyp.
  rewrite <- Hyp.
  rewrite assoc.
  rewrite BinCoproductIn2Commutes.
  apply idpath.
Qed.

Lemma BinCoproductIn1Commutes_right_in_double_ctx_dir (g0 : x --> a) (f : a --> c) (g : b --> c)
  (h : c --> d) (h' : x --> d) : h' = g0 · f · h ->
  h' = g0 · BinCoproductIn1 (CC _ _) · (BinCoproductArrow (CC _ _) f g · h).
Proof.
  intro Hyp.
  rewrite Hyp.
  repeat rewrite <- assoc.
  apply maponpaths.
  rewrite assoc.
  rewrite BinCoproductIn1Commutes.
  apply idpath.
Qed.

Lemma BinCoproductIn2Commutes_right_in_double_ctx_dir (g0 : x --> b) (f : a --> c) (g : b --> c)
  (h : c --> d) (h' : x --> d) : h' = g0 · g · h ->
  h' = g0 · BinCoproductIn2 (CC _ _) · (BinCoproductArrow (CC _ _) f g · h).
Proof.
  intro Hyp.
  rewrite Hyp.
  repeat rewrite <- assoc.
  apply maponpaths.
  rewrite assoc.
  rewrite BinCoproductIn2Commutes.
  apply idpath.
Qed.
(** end of specialized versions of the beta laws for coproducts *)

(* do we ever want to create a multitude of similar lemmas for other rewrite rules?
Lemma id_left_to_the_right (C': precategory)(a b : C')(f h : C' ⟦ a, b ⟧): h = f -> h = identity a· f.
Proof.
  intro Hyp.
  rewrite Hyp.
  apply pathsinv0, id_left.
Qed.

Lemma id_left_to_the_right_in_ctx (C': precategory)(a b c: C')(f : C' ⟦ a, b ⟧)(g : C' ⟦ b, c ⟧)
  (h : C' ⟦ a, c ⟧): h = f · g -> h = identity a · f · g.
Proof.
  intro Hyp.
  rewrite Hyp.
  rewrite id_left.
  apply idpath.
Qed.

Lemma assoc_to_the_right (C' : precategory) (a b c d : C') (f : C' ⟦ a, b ⟧)
       (g : C' ⟦ b, c ⟧) (h : C' ⟦ c, d ⟧)(res: C' ⟦ a, d ⟧) : res = f· g· h -> res = f· (g· h).
Proof.
  intro Hyp.
  rewrite Hyp.
  apply pathsinv0, assoc.
Qed.

Lemma assoc_back_to_the_right (C' : precategory) (a b c d : C') (f : C' ⟦ a, b ⟧)
       (g : C' ⟦ b, c ⟧) (h : C' ⟦ c, d ⟧)(res: C' ⟦ a, d ⟧) : res = f· (g· h) -> res = f· g· h.
Proof.
  intro Hyp.
  rewrite Hyp.
  apply assoc.
Qed.
*)

Definition BinCoproductOfArrows_comp (f : a --> c) (f' : b --> d) (g : c --> x) (g' : d --> y)
  : BinCoproductOfArrows _ (CC a b) (CC c d) f f' ·
    BinCoproductOfArrows _ (CC _ _) (CC _ _) g g'
    =
    BinCoproductOfArrows _ (CC _ _) (CC _ _) (f · g) (f' · g').
Proof.
  apply BinCoproductArrowUnique.
  - rewrite assoc.
    rewrite BinCoproductOfArrowsIn1.
    rewrite <- assoc.
    rewrite BinCoproductOfArrowsIn1.
    apply assoc.
  - rewrite assoc.
    rewrite BinCoproductOfArrowsIn2.
    rewrite <- assoc.
    rewrite BinCoproductOfArrowsIn2.
    apply assoc.
Qed.

Lemma precompWithBinCoproductArrow_eq  (CCab : BinCoproduct a b)
    (CCcd : BinCoproduct c d) (f : a --> c) (g : b --> d)
     (k : c --> x) (h : d --> x) (fk : a --> x) (gh : b --> x):
      fk = f · k → gh = g · h →
        BinCoproductOfArrows _ CCab CCcd f g · BinCoproductArrow CCcd k h =
         BinCoproductArrow CCab (fk) (gh).
Proof.
  intros H H'.
  rewrite H.
  rewrite H'.
  apply precompWithBinCoproductArrow.
Qed.

End BinCoproducts.

(** * Binary coproducts from colimits *)
Section BinCoproducts_from_Colims.

Context (C : category).

Definition two_graph : graph := (bool,,λ _ _,empty).

Definition bincoproduct_diagram (a b : C) : diagram two_graph C.
Proof.
exists (λ x : bool, if x then a else b).
abstract (intros u v F; induction F).
Defined.

Definition BinCoprod {a b c : C} (ac : a --> c) (bc : b --> c) :
   cocone (bincoproduct_diagram a b) c.
Proof.
use make_cocone.
+ intros x; induction x; assumption.
+ abstract (intros x y e; destruct e).
Defined.

Lemma BinCoproducts_from_Colims : Colims_of_shape two_graph C -> BinCoproducts C.
Proof.
intros H a b.
set (CC := H (bincoproduct_diagram a b)).
use make_BinCoproduct.
+ apply (colim CC).
+ apply (colimIn CC true).
+ apply (colimIn CC false).
+ apply (make_isBinCoproduct _ C); intros c f g.
  use unique_exists.
  - apply colimArrow, (BinCoprod f g).
  - abstract (split;
      [ apply (colimArrowCommutes CC c (BinCoprod f g) true)
      | apply (colimArrowCommutes CC c (BinCoprod f g) false) ]).
  - abstract (intros h; apply isapropdirprod; apply C).
  - abstract (now intros h [H1 H2]; apply colimArrowUnique; intro x; induction x).
Defined.

End BinCoproducts_from_Colims.

(** * Coproducts over bool from binary coproducts *)
Section CoproductsBool.

Lemma CoproductsBool {C : category}
  (HC : BinCoproducts C) : Coproducts bool C.
Proof.
intros H.
use make_Coproduct.
- apply (HC (H true) (H false)).
- induction i; apply (pr1 (HC (H true) (H false))).
- use (make_isCoproduct _ _ C); intros c f.
  set (uniqex := pr2 (HC (H true) (H false)) c (f true) (f false)).
  (* induction (pr2 (HC (H true) (H false)) c (f true) (f false)) as [[x1 [x2 x3]] x4]. *)
  use unique_exists.
  + exact (pr1 (pr1 uniqex)).
  + abstract (cbn; induction i;
              [exact (pr1 (pr2 (pr1 uniqex))) | exact (pr2 (pr2 (pr1 uniqex)))]).
  + abstract (intros x; apply impred; intros; apply C).
  + abstract (intros h1 h2;
              apply (maponpaths pr1 (pr2 uniqex (h1,,(h2 true,,h2 false))))).
Defined.

End CoproductsBool.

Section functors.

Definition bincoproduct_functor_data {C : category} (PC : BinCoproducts C) :
  functor_data (category_binproduct C C) C.
Proof.
use tpair.
- intros p.
  apply (BinCoproductObject (PC (pr1 p) (pr2 p))).
- intros p q f.
  apply (BinCoproductOfArrows _ (PC (pr1 p) (pr2 p))
                             (PC (pr1 q) (pr2 q)) (pr1 f) (pr2 f)).
Defined.

(* The binary coproduct functor: C * C -> C *)

Lemma is_functor_bincoproduct_functor_data {C : category} (PC : BinCoproducts C)
  : is_functor (bincoproduct_functor_data PC).
Proof.
  split.
  - intro x; simpl; apply pathsinv0.
    use BinCoproduct_endo_is_identity.
    + now rewrite BinCoproductOfArrowsIn1, id_left.
    + now rewrite BinCoproductOfArrowsIn2, id_left.
  -  now intros x y z f g; simpl; rewrite BinCoproductOfArrows_comp.
Qed.

Definition bincoproduct_functor {C : category} (PC : BinCoproducts C)
  : functor (category_binproduct C C) C
  := make_functor _ (is_functor_bincoproduct_functor_data PC).

(* Defines the coproduct of two functors *)
Definition BinCoproduct_of_functors_alt {C D : category}
           (HD : BinCoproducts D) (F G : C ⟶ D) : C ⟶ D :=
    tuple_functor (λ b, bool_rect (λ _, C ⟶ D) F G b) ∙
    coproduct_functor bool (CoproductsBool HD).

(* Defines the coproduct of two functors by:
    x -> (x,x) -> (F x,G x) -> F x + G x

  For a direct and equal definition see FunctorsPointwiseBinCoproduct.v (seems obsolete)

  Above is a slightly simpler definition
*)
Definition BinCoproduct_of_functors_alt2 {C D : category}
  (HD : BinCoproducts D) (F G : functor C D) : functor C D :=
    bindelta_functor C ∙ (pair_functor F G ∙ bincoproduct_functor HD).

End functors.

(** In the following section we show that if the morphisms to components are
    zero, then the unique morphism factoring through the bincoproduct is the
    zero morphism. *)
Section BinCoproduct_zeroarrow.

  Context (C : category) (Z : Zero C).

  Lemma BinCoproductArrowZero {x y z: C} {BP : BinCoproduct x y} (f : x --> z) (g : y --> z) :
    f = ZeroArrow Z _ _ -> g = ZeroArrow Z _ _ -> BinCoproductArrow BP f g = ZeroArrow Z _ _ .
  Proof.
    intros X X0. apply pathsinv0.
    use BinCoproductArrowUnique.
    rewrite X. apply ZeroArrow_comp_right.
    rewrite X0. apply ZeroArrow_comp_right.
  Qed.

End BinCoproduct_zeroarrow.

(** Goal: lift coproducts from the target (pre)category to the functor (pre)category *)

Section def_functor_pointwise_coprod.

Context (C D : category) (HD : BinCoproducts D).

Section BinCoproduct_of_functors.

Context (F G : functor C D).

Local Notation "c ⊗ d" := (BinCoproductObject (HD c d)).

Definition BinCoproduct_of_functors_ob (c : C) : D := F c ⊗ G c.

Definition BinCoproduct_of_functors_mor (c c' : C) (f : c --> c')
  : BinCoproduct_of_functors_ob c --> BinCoproduct_of_functors_ob c'
  := BinCoproductOfArrows _ _ _ (#F f) (#G f).

Definition BinCoproduct_of_functors_data : functor_data C D.
Proof.
  exists BinCoproduct_of_functors_ob.
  exact BinCoproduct_of_functors_mor.
Defined.

Lemma is_functor_BinCoproduct_of_functors_data : is_functor BinCoproduct_of_functors_data.
Proof.
  split; simpl; intros.
  - unfold functor_idax; intros; simpl in *.
    apply pathsinv0.
    apply BinCoproduct_endo_is_identity.
    + unfold BinCoproduct_of_functors_mor.
      rewrite BinCoproductOfArrowsIn1.
      rewrite functor_id.
      apply id_left.
    + unfold BinCoproduct_of_functors_mor.
      rewrite BinCoproductOfArrowsIn2.
      rewrite functor_id.
      apply id_left.
  - unfold functor_compax, BinCoproduct_of_functors_mor;
    intros; simpl in *.
    unfold BinCoproduct_of_functors_mor.
    do 2 rewrite functor_comp.
    rewrite <- BinCoproductOfArrows_comp.
    apply idpath.
(* former proof:
    unfold BinCoproductOfArrows.
    apply pathsinv0.
    apply BinCoproductArrowUnique.
    + rewrite assoc. simpl in *.
      set (H:= BinCoproductIn1Commutes ).
      set (H2 := H D _ _ (HD (F a) (G a))).
      rewrite H2.
      rewrite <- assoc.
      rewrite functor_comp.
      repeat rewrite <- assoc.
      apply maponpaths.
      apply BinCoproductIn1Commutes.
    + rewrite assoc.
      set (H:= BinCoproductIn2Commutes D _ _ (HD (F a) (G a))).
      rewrite H.
      rewrite functor_comp.
      repeat rewrite <- assoc.
      apply maponpaths.
      apply BinCoproductIn2Commutes.
*)
Qed.

Definition BinCoproduct_of_functors : functor C D :=
  tpair _ _ is_functor_BinCoproduct_of_functors_data.

Lemma BinCoproduct_of_functors_alt2_eq_BinCoproduct_of_functors :
  BinCoproduct_of_functors_alt2 HD F G = BinCoproduct_of_functors.
Proof.
now apply (functor_eq _ _ D).
Qed.

Lemma BinCoproduct_of_functors_alt_eq_BinCoproduct_of_functors :
  BinCoproduct_of_functors_alt HD F G = BinCoproduct_of_functors.
Proof.
now apply (functor_eq _ _ D).
Qed.

Lemma BinCoproduct_of_functors_alt_eq_BinCoproduct_of_functors_alt2 :
  BinCoproduct_of_functors_alt  HD F G = BinCoproduct_of_functors_alt2 HD F G.
Proof.
now apply (functor_eq _ _ D).
Qed.

Definition coproduct_nat_trans_in1_data : ∏ c, F c --> BinCoproduct_of_functors c
  := λ c : C, BinCoproductIn1 (HD (F c) (G c)).

Lemma is_nat_trans_coproduct_nat_trans_in1_data
  : is_nat_trans _ _ coproduct_nat_trans_in1_data.
Proof.
  unfold is_nat_trans.
  intros c c' f.
  unfold coproduct_nat_trans_in1_data.
  unfold BinCoproduct_of_functors. simpl.
  unfold BinCoproduct_of_functors_mor.
  assert (XX:= BinCoproductOfArrowsIn1).
  assert (X1 := XX _ (F c) (G c) (HD (F c) (G c))).
  assert (X2 := X1 _ _ (HD (F c') (G c'))).
  rewrite X2.
  apply idpath.
Qed.

Definition coproduct_nat_trans_in1 : nat_trans _ _
  := tpair _ _ is_nat_trans_coproduct_nat_trans_in1_data.

Definition coproduct_nat_trans_in2_data : ∏ c, G c --> BinCoproduct_of_functors c
  := λ c : C, BinCoproductIn2 (HD (F c) (G c)).

Lemma is_nat_trans_coproduct_nat_trans_in2_data
  : is_nat_trans _ _ coproduct_nat_trans_in2_data.
Proof.
  unfold is_nat_trans.
  intros c c' f.
  unfold coproduct_nat_trans_in2_data.
  unfold BinCoproduct_of_functors. simpl.
  unfold BinCoproduct_of_functors_mor.
  assert (XX:= BinCoproductOfArrowsIn2).
  assert (X1 := XX _ (F c) (G c) (HD (F c) (G c))).
  assert (X2 := X1 _ _ (HD (F c') (G c'))).
  rewrite X2.
  apply idpath.
Qed.

Definition coproduct_nat_trans_in2 : nat_trans _ _
  := tpair _ _ is_nat_trans_coproduct_nat_trans_in2_data.

Section vertex.

(** The coproduct morphism of a diagram with vertex [A] *)

Context (A : functor C D) (f : F ⟹ A) (g : G ⟹ A).

Definition coproduct_nat_trans_data : ∏ c, BinCoproduct_of_functors c --> A c.
Proof.
  intro c.
  apply BinCoproductArrow.
  - exact (f c).
  - exact (g c).
Defined.

Lemma is_nat_trans_coproduct_nat_trans_data : is_nat_trans _ _ coproduct_nat_trans_data.
Proof.
  intros a b k.
  simpl.
  unfold BinCoproduct_of_functors_mor.
  unfold coproduct_nat_trans_data.
  simpl.
  set (XX:=precompWithBinCoproductArrow).
  set (X1 := XX D _ _ (HD (F a) (G a))).
  set (X2 := X1 _ _ (HD (F b) (G b))).
  rewrite X2.
  clear X2 X1 XX.
  set (XX:=postcompWithBinCoproductArrow).
  set (X1 := XX D _ _ (HD (F a) (G a))).
  rewrite X1.
  rewrite (nat_trans_ax f).
  rewrite (nat_trans_ax g).
  apply idpath.
Qed.

Definition coproduct_nat_trans : nat_trans _ _
  := tpair _ _ is_nat_trans_coproduct_nat_trans_data.

Lemma coproduct_nat_trans_In1Commutes :
  nat_trans_comp _ _ _ coproduct_nat_trans_in1 coproduct_nat_trans = f.
Proof.
  apply nat_trans_eq.
  - apply D.
  - intro c; simpl.
    apply BinCoproductIn1Commutes.
Qed.

Lemma coproduct_nat_trans_In2Commutes :
  nat_trans_comp _ _ _ coproduct_nat_trans_in2 coproduct_nat_trans = g.
Proof.
  apply nat_trans_eq.
  - apply D.
  - intro c; simpl.
    apply BinCoproductIn2Commutes.
Qed.

End vertex.

Lemma coproduct_nat_trans_univ_prop (A : [C, D])
  (f : (F : [C,D]) --> A) (g : (G : [C,D]) --> A) :
   ∏
   t : ∑ fg : (BinCoproduct_of_functors:[C,D]) --> A,
       (coproduct_nat_trans_in1 : (F:[C,D]) --> BinCoproduct_of_functors)· fg = f
      ×
       (coproduct_nat_trans_in2: (G : [C,D]) --> BinCoproduct_of_functors)· fg = g,
   t =
   tpair
     (λ fg : (BinCoproduct_of_functors:[C,D]) --> A,
      (coproduct_nat_trans_in1 : (F:[C,D]) --> BinCoproduct_of_functors)· fg = f
   ×
      (coproduct_nat_trans_in2 : (G:[C,D]) --> BinCoproduct_of_functors) · fg = g)
     (coproduct_nat_trans A f g)
     (make_dirprod (coproduct_nat_trans_In1Commutes A f g)
        (coproduct_nat_trans_In2Commutes A f g)).
Proof.
  intro t.
  simpl in *.
  destruct t as [t1 [ta tb]].
  simpl in *.
  apply subtypePath.
  - intro.
    apply isapropdirprod;
    apply isaset_nat_trans;
    apply D.
  - simpl.
    apply nat_trans_eq.
    + apply D.
    + intro c.
      unfold coproduct_nat_trans.
      simpl.
      unfold coproduct_nat_trans_data.
      simpl.
      apply BinCoproductArrowUnique.
      * apply (nat_trans_eq_pointwise ta).
      * apply (nat_trans_eq_pointwise tb).
Qed.

Definition functor_precat_coproduct_cocone
  : @BinCoproduct [C, D] F G.
Proof.
  use make_BinCoproduct.
  - apply BinCoproduct_of_functors.
  - apply coproduct_nat_trans_in1.
  - apply coproduct_nat_trans_in2.
  - use make_isBinCoproduct.
    + apply functor_category_has_homsets.
    + intros A f g.
     exists (tpair _ (coproduct_nat_trans A f g)
             (make_dirprod (coproduct_nat_trans_In1Commutes _ _ _ )
                          (coproduct_nat_trans_In2Commutes _ _ _ ))).
     apply coproduct_nat_trans_univ_prop.
Defined.

End BinCoproduct_of_functors.

Definition BinCoproducts_functor_precat : BinCoproducts [C, D].
Proof.
  intros F G.
  apply functor_precat_coproduct_cocone.
Defined.

End def_functor_pointwise_coprod.

Section generalized_option_functors.

Context {C : category} (CC : BinCoproducts C).

(* The functors "a + _" and "_ + a" *)
Definition constcoprod_functor1 (a : C) : functor C C :=
  BinCoproduct_of_functors C C CC (constant_functor C C a) (functor_identity C).

Definition constcoprod_functor2 (a : C) : functor C C :=
  BinCoproduct_of_functors C C CC (functor_identity C) (constant_functor C C a).

Section option_functor.

Context (TC : Terminal C).
Let one : C := TerminalObject TC.

Definition option_functor : functor C C :=
  constcoprod_functor1 one.

End option_functor.

End generalized_option_functors.

(** ** Construction of isBinCoproduct from an isomorphism to BinCoproduct. *)
Section BinCoproduct_from_z_iso.

  Context (C : category).

  Local Lemma z_iso_to_isBinCoproduct_comm {x y z : C} (BP : BinCoproduct x y)
        (i : z_iso z (BinCoproductObject BP)) (w : C) (f : x --> w) (g : y --> w) :
    (BinCoproductIn1 BP · inv_from_z_iso i · (i · BinCoproductArrow BP f g) = f)
      × (BinCoproductIn2 BP · inv_from_z_iso i · (i · BinCoproductArrow BP f g) = g).
  Proof.
    split.
    - rewrite <- assoc. rewrite (assoc _ i).
      rewrite (z_iso_after_z_iso_inv i). rewrite id_left.
      apply BinCoproductIn1Commutes.
    - rewrite <- assoc. rewrite (assoc _ i).
      rewrite (z_iso_after_z_iso_inv i). rewrite id_left.
      apply BinCoproductIn2Commutes.
  Qed.

  Local Lemma z_iso_to_isBinCoproduct_unique {x y z : C} (BP : BinCoproduct x y)
        (i : z_iso z (BinCoproductObject BP)) (w : C) (f : x --> w) (g : y --> w) (y0 : C ⟦ z, w ⟧)
        (T : (BinCoproductIn1 BP · inv_from_z_iso i · y0 = f)
               × (BinCoproductIn2 BP · inv_from_z_iso i · y0 = g)) :
    y0 = i · BinCoproductArrow BP f g.
  Proof.
    apply (pre_comp_with_z_iso_is_inj (z_iso_inv_from_z_iso i)).
    rewrite assoc. cbn. rewrite (z_iso_after_z_iso_inv i). rewrite id_left.
    apply BinCoproductArrowUnique.
    - rewrite assoc. apply (dirprod_pr1 T).
    - rewrite assoc. apply (dirprod_pr2 T).
  Qed.

  Lemma z_iso_to_isBinCoproduct {x y z : C} (BP : BinCoproduct x y)
        (i : z_iso z (BinCoproductObject BP)) :
    isBinCoproduct C _ _ z
                         ((BinCoproductIn1 BP) · (z_iso_inv_from_z_iso i))
                         ((BinCoproductIn2 BP) · (z_iso_inv_from_z_iso i)).
  Proof.
    intros w f g.
    use unique_exists.
    (* The arrow *)
    - exact (i · (BinCoproductArrow BP f g)).
    (* Commutativity *)
    - exact (z_iso_to_isBinCoproduct_comm BP i w f g).
    (* Equality on equalities of morphisms. *)
    - abstract (intros y0; apply isapropdirprod; apply C).
    (* Uniqueness *)
    - abstract (intros y0 T; exact (z_iso_to_isBinCoproduct_unique BP i w f g y0 T)).
  Qed.

  Definition z_iso_to_BinCoproduct {x y z : C} (BP : BinCoproduct x y)
             (i : z_iso z (BinCoproductObject BP)) :
    BinCoproduct x y := make_BinCoproduct
                                  C _ _ z
                                  ((BinCoproductIn1 BP) · (z_iso_inv_from_z_iso i))
                                  ((BinCoproductIn2 BP) · (z_iso_inv_from_z_iso i))
                                  (z_iso_to_isBinCoproduct BP i).

End BinCoproduct_from_z_iso.

(** Equivalent universal property: (A --> C) × (B --> C) ≃ (A + B --> C)

 Compare to [weqfunfromcoprodtoprod].
 *)

Section EquivalentDefinition.
  Context {C : category} {a b co : ob C} (i1 : a --> co) (i2 : b --> co) .

  Definition precomp_with_injections (c : ob C) (f : co --> c) : (a --> c) × (b --> c) :=
    make_dirprod (i1 · f)  (i2 · f).

  Definition isBinCoproduct' : UU :=
    ∏ c : ob C, isweq (precomp_with_injections c).

  Definition isBinCoproduct'_weq (is : isBinCoproduct') :
    ∏ c, (co --> c) ≃ (a --> c) × (b --> c) :=
    λ a, make_weq (precomp_with_injections a) (is a).

  Lemma isBinCoproduct'_to_isBinCoproduct :
    isBinCoproduct' -> isBinCoproduct _ _ _ co i1 i2.
  Proof.
    intros isBCP' ? f g.
    apply (@iscontrweqf (hfiber (isBinCoproduct'_weq isBCP' _)
                                (make_dirprod f g))).
    - use weqfibtototal; intro; cbn.
      unfold precomp_with_injections.
      apply pathsdirprodweq.
    - apply weqproperty.
  Defined.

  Lemma isBinCoproduct_to_isBinCoproduct' :
    isBinCoproduct _ _ _ co i1 i2 -> isBinCoproduct'.
  Proof.
    intros isBCP ? fg.
    unfold hfiber, precomp_with_injections.
    apply (@iscontrweqf (∑ u : C ⟦ co, c ⟧, i1 · u = pr1 fg × i2 · u = pr2 fg)).
    - use weqfibtototal; intros to_prod.
      apply invweq, pathsdirprodweq.
    - exact (isBCP c (pr1 fg) (pr2 fg)). (* apply universal property *)
  Defined.

  (* TODO: prove that [isBinCoproduct'_to_isBinCoproduct] is an equivalence *)

End EquivalentDefinition.

(** Match non-implicit arguments of [isBinCoproduct] *)
Arguments isBinCoproduct' _ _ _ _ _ : clear implicits.

(**
 Coproducts when the inclusions are equal
 *)
Definition isBinCoproduct_eq_arrow
           {C : category}
           {x y z : C}
           {ι₁ ι₁' : x --> z}
           (p₁ : ι₁ = ι₁')
           {ι₂ ι₂' : y --> z}
           (p₂ : ι₂ = ι₂')
           (H : isBinCoproduct C x y z ι₁ ι₂)
  : isBinCoproduct C x y z ι₁' ι₂'.
Proof.
  pose (P := make_BinCoproduct _ _ _ _ _ _ H).
  intros w f g.
  use iscontraprop1.
  - abstract
      (induction p₁, p₂ ;
       apply isapropifcontr ;
       apply H).
  - simple refine (_ ,, _ ,, _).
    + exact (BinCoproductArrow P f g).
    + abstract
        (induction p₁ ;
         exact (BinCoproductIn1Commutes _ _ _ P _ f g)).
    + abstract
        (induction p₂ ;
         exact (BinCoproductIn2Commutes _ _ _ P _ f g)).
Defined.

(**
 Coproduct of isos
 *)
Section BinCoproductOfIsos.
  Context {C : category}
          {a b c d : C}
          (Pab : BinCoproduct a b)
          (Pcd : BinCoproduct c d)
          (f : z_iso a c)
          (g : z_iso b d).

  Let fg : BinCoproductObject Pab --> BinCoproductObject Pcd
    := BinCoproductOfArrows _ _ _ f g.

  Let fg_inv : BinCoproductObject Pcd --> BinCoproductObject Pab
    := BinCoproductOfArrows _ _ _ (inv_from_z_iso f) (inv_from_z_iso g).

  Lemma bincoproduct_of_z_iso_inv
    : is_inverse_in_precat fg fg_inv.
  Proof.
    split; use BinCoproductArrowsEq; unfold fg, fg_inv.
    - rewrite !assoc.
      rewrite BinCoproductOfArrowsIn1.
      rewrite !assoc'.
      rewrite BinCoproductOfArrowsIn1.
      rewrite !assoc.
      rewrite z_iso_inv_after_z_iso.
      rewrite id_left, id_right.
      apply idpath.
    - rewrite !assoc.
      rewrite BinCoproductOfArrowsIn2.
      rewrite !assoc'.
      rewrite BinCoproductOfArrowsIn2.
      rewrite !assoc.
      rewrite z_iso_inv_after_z_iso.
      rewrite id_left, id_right.
      apply idpath.
    - rewrite !assoc.
      rewrite BinCoproductOfArrowsIn1.
      rewrite !assoc'.
      rewrite BinCoproductOfArrowsIn1.
      rewrite !assoc.
      rewrite z_iso_after_z_iso_inv.
      rewrite id_left, id_right.
      apply idpath.
    - rewrite !assoc.
      rewrite BinCoproductOfArrowsIn2.
      rewrite !assoc'.
      rewrite BinCoproductOfArrowsIn2.
      rewrite !assoc.
      rewrite z_iso_after_z_iso_inv.
      rewrite id_left, id_right.
      apply idpath.
  Qed.

  Definition bincoproduct_of_z_iso
    : z_iso (BinCoproductObject Pab) (BinCoproductObject Pcd).
  Proof.
    use make_z_iso.
    - exact fg.
    - exact fg_inv.
    - exact bincoproduct_of_z_iso_inv.
  Defined.

End BinCoproductOfIsos.

Section AssociativityOfBinaryCoproduct.

  Context {C : category} (BCP : BinCoproducts C).

  Definition bincoprod_associator_data (c d e : C) : BCP (BCP c d) e --> BCP c (BCP d e).
  Proof.
    use BinCoproductArrow.
    - use BinCoproductOfArrows.
      + exact (identity c).
      + apply BinCoproductIn1.
    - refine (_ · BinCoproductIn2 _).
      apply BinCoproductIn2.
  Defined.

  Definition bincoprod_associatorinv_data (c d e : C) : BCP c (BCP d e) --> BCP (BCP c d) e.
  Proof.
    use BinCoproductArrow.
    - refine (_ · BinCoproductIn1 _).
      apply BinCoproductIn1.
    - use BinCoproductOfArrows.
      + apply BinCoproductIn2.
      + exact (identity e).
  Defined.

  Lemma bincoprod_associator_inverses (c d e : C) :
    is_inverse_in_precat (bincoprod_associator_data c d e) (bincoprod_associatorinv_data c d e).
  Proof.
    split.
    + apply pathsinv0, BinCoproduct_endo_is_identity.
      * rewrite assoc.
        etrans.
        { apply cancel_postcomposition.
          apply BinCoproductIn1Commutes. }
        use BinCoproductArrowsEq.
        -- repeat rewrite assoc.
           etrans.
           { apply cancel_postcomposition.
             apply BinCoproductIn1Commutes. }
           rewrite id_left.
           etrans.
           { apply BinCoproductIn1Commutes. }
           apply idpath.
        -- repeat rewrite assoc.
           etrans.
           { apply cancel_postcomposition.
             apply BinCoproductIn2Commutes. }
           etrans.
           { rewrite assoc'.
             apply maponpaths.
             apply BinCoproductIn2Commutes. }
           apply BinCoproductOfArrowsIn1.
      * rewrite assoc.
        etrans.
        { apply cancel_postcomposition.
          apply BinCoproductIn2Commutes. }
        etrans.
        { rewrite assoc'.
          apply maponpaths.
          apply BinCoproductIn2Commutes. }
        rewrite BinCoproductOfArrowsIn2.
        apply id_left.
    + apply pathsinv0, BinCoproduct_endo_is_identity.
      * rewrite assoc.
        etrans.
        { apply cancel_postcomposition.
          apply BinCoproductIn1Commutes. }
        etrans.
        { rewrite assoc'.
          apply maponpaths.
          apply BinCoproductIn1Commutes. }
        rewrite BinCoproductOfArrowsIn1.
        apply id_left.
      * rewrite assoc.
        etrans.
        { apply cancel_postcomposition.
          apply BinCoproductIn2Commutes. }
        use BinCoproductArrowsEq.
        -- repeat rewrite assoc.
           etrans.
           { apply cancel_postcomposition.
             apply BinCoproductOfArrowsIn1. }
           etrans.
           { rewrite assoc'.
             apply maponpaths.
             apply BinCoproductIn1Commutes. }
           apply BinCoproductOfArrowsIn2.
        -- repeat rewrite assoc.
           etrans.
           { apply cancel_postcomposition.
             apply BinCoproductOfArrowsIn2. }
           rewrite id_left.
           etrans.
           { apply BinCoproductIn2Commutes. }
           apply idpath.
  Qed.

  Definition bincoprod_associator (c d e : C) : z_iso (BCP (BCP c d) e) (BCP c (BCP d e))
    := bincoprod_associator_data c d e,,
         bincoprod_associatorinv_data c d e,,
         bincoprod_associator_inverses c d e.

End AssociativityOfBinaryCoproduct.

Section DistributionThroughFunctor.

  Context {C D : category} (BCPC : BinCoproducts C) (BCPD : BinCoproducts D) (F : functor C D).

  Definition bincoprod_antidistributor (c c' : C) :
    BCPD (F c) (F c') --> F (BCPC c c').
  Proof.
    use BinCoproductArrow; apply #F; [apply BinCoproductIn1 | apply BinCoproductIn2 ].
  Defined.

  Lemma bincoprod_antidistributor_nat
    (cc'1 cc'2 : category_binproduct C C) (g : category_binproduct C C ⟦ cc'1, cc'2 ⟧) :
    bincoprod_antidistributor (pr1 cc'1) (pr2 cc'1) · #F (#(bincoproduct_functor BCPC) g) =
    #(bincoproduct_functor BCPD) (#(pair_functor F F) g) · bincoprod_antidistributor (pr1 cc'2) (pr2 cc'2).
  Proof.
    etrans.
    { apply postcompWithBinCoproductArrow. }
    etrans.
    2: { apply pathsinv0, precompWithBinCoproductArrow. }
    apply maponpaths_12.
    - etrans.
      { apply pathsinv0, functor_comp. }
      etrans.
      2: { apply functor_comp. }
      apply maponpaths.
      apply BinCoproductIn1Commutes.
    - etrans.
      { apply pathsinv0, functor_comp. }
      etrans.
      2: { apply functor_comp. }
      apply maponpaths.
      apply BinCoproductIn2Commutes.
  Qed.

   Lemma bincoprod_antidistributor_commutes_with_associativity_of_coproduct (c d e : C) :
    #(bincoproduct_functor BCPD) (catbinprodmor (bincoprod_antidistributor c d) (identity (F e))) ·
      bincoprod_antidistributor (BCPC c d) e ·
      #F (bincoprod_associator_data BCPC c d e) =
    bincoprod_associator_data BCPD (F c) (F d) (F e) ·
      #(bincoproduct_functor BCPD) (catbinprodmor (identity (F c)) (bincoprod_antidistributor d e)) ·
      bincoprod_antidistributor c (BCPC d e).
  Proof.
    etrans.
    { apply cancel_postcomposition.
      apply precompWithBinCoproductArrow. }
    etrans.
    { apply postcompWithBinCoproductArrow. }
    etrans.
    2: { rewrite assoc'.
         apply maponpaths.
         apply pathsinv0, precompWithBinCoproductArrow. }
    etrans.
    2: { apply pathsinv0, postcompWithBinCoproductArrow. }
    apply maponpaths_12.
    - etrans.
      2: { apply pathsinv0, precompWithBinCoproductArrow. }
      etrans.
      { rewrite assoc'.
        apply maponpaths.
        etrans.
        { apply pathsinv0, functor_comp. }
        apply maponpaths.
        apply BinCoproductIn1Commutes.
      }
      etrans.
      { cbn. apply postcompWithBinCoproductArrow. }
      apply maponpaths_12.
      + cbn.
        do 2 rewrite id_left.
        etrans.
        { apply pathsinv0, functor_comp. }
        apply maponpaths.
        rewrite BinCoproductOfArrowsIn1.
        apply id_left.
      + cbn.
        etrans.
        { apply pathsinv0, functor_comp. }
        etrans.
        { apply maponpaths.
          apply BinCoproductOfArrowsIn2. }
        rewrite assoc.
        etrans.
        2: { apply cancel_postcomposition.
             apply pathsinv0, BinCoproductIn1Commutes. }
        apply functor_comp.
    - etrans.
      { cbn. rewrite id_left.
        apply pathsinv0, functor_comp. }
      etrans.
      2: { rewrite assoc'.
           apply maponpaths.
           apply pathsinv0, BinCoproductIn2Commutes. }
      cbn.
      rewrite assoc.
      etrans.
      2: { apply cancel_postcomposition.
           apply pathsinv0, BinCoproductIn2Commutes. }
      etrans.
      { apply maponpaths.
        apply BinCoproductIn2Commutes. }
      apply functor_comp.
  Qed.

(** axiomatize extra requirements *)

  Definition bincoprod_distributor_data : UU := ∏ (c c' : C),
      F (BCPC c c') --> BCPD (F c) (F c').

  Identity Coercion bincoprod_distributor_data_funclass: bincoprod_distributor_data >-> Funclass.

  Definition bincoprod_distributor_iso_law (δ : bincoprod_distributor_data) : UU :=
    ∏ (c c' : C), is_inverse_in_precat (δ c c') (bincoprod_antidistributor c c').

  Definition bincoprod_distributor : UU := ∑ δ : bincoprod_distributor_data, bincoprod_distributor_iso_law δ.

  Definition bincoprod_distributor_to_data (δ : bincoprod_distributor) : bincoprod_distributor_data := pr1 δ.
  Coercion bincoprod_distributor_to_data : bincoprod_distributor >-> bincoprod_distributor_data.

End DistributionThroughFunctor.

Section DistributionForPrecompositionFunctor.

  Context {A B C : category} (BCPC : BinCoproducts C) (H : functor A B).

  Let BCPAC : BinCoproducts [A,C] := BinCoproducts_functor_precat A C BCPC.
  Let BCPBC : BinCoproducts [B,C] := BinCoproducts_functor_precat B C BCPC.
  Let precomp : functor [B,C] [A,C] := pre_composition_functor A B C H.

  Definition precomp_bincoprod_distributor_data :  bincoprod_distributor_data BCPBC BCPAC precomp.
  Proof.
    intros G1 G2.
    apply nat_trans_id.
  Defined.

  Lemma precomp_bincoprod_distributor_law :
    bincoprod_distributor_iso_law _ _ _ precomp_bincoprod_distributor_data.
  Proof.
    intros F G.
    split.
    - apply (nat_trans_eq C).
      intro c.
      cbn.
      rewrite id_left.
      apply pathsinv0, BinCoproduct_endo_is_identity.
      + apply BinCoproductIn1Commutes.
      + apply BinCoproductIn2Commutes.
    - etrans.
      { apply postcompWithBinCoproductArrow. }
      etrans.
      2: { apply pathsinv0, BinCoproductArrowEta. }
      apply maponpaths_12;
        (rewrite id_right; apply (nat_trans_eq C); intro c; apply id_right).
  Qed.

  Definition precomp_bincoprod_distributor :  bincoprod_distributor BCPBC BCPAC precomp :=
    _,,precomp_bincoprod_distributor_law.

End DistributionForPrecompositionFunctor.

author: UniMath

repo: UniMath

save_path: github-repos/coq/UniMath-UniMath


text:
Require Import HoTT.
Require Import GR.bicategories.bicategories.
Require Import GR.bicategories.lax_functors.
Require Import GR.bicategories.lax_transformations.
Require Import GR.bicategories.modifications.

Record BiAdjunction_d
       `{Univalence}
       (C D : BiCategory)
  := Build_BiAdjunction_d
       { left_adjoint_d : LaxFunctor C D ;
         left_adjoint_pseudo_d : is_pseudo left_adjoint_d ;
         right_adjoint_d : LaxFunctor D C ;
         right_adjoint_pseudo_d : is_pseudo right_adjoint_d ;
         unit_d : LaxTransformation
                    (lax_id_functor C)
                    (lax_comp right_adjoint_d left_adjoint_d) ;
         counit_d : LaxTransformation
                      (lax_comp left_adjoint_d right_adjoint_d)
                      (lax_id_functor D) ;
       }.

Arguments Build_BiAdjunction_d {_ C D} _ _ _ _ _ _.
Ltac make_biadjunction := simple refine (Build_BiAdjunction_d _ _ _ _ _ _).
Arguments left_adjoint_d {_ C D}.
Arguments right_adjoint_d {_ C D}.
Arguments unit_d {_ C D}.
Arguments counit_d {_ C D}.

Global Instance left_adjoint_pseudo_functor
       `{Univalence}
       {C D : BiCategory}
       (F : BiAdjunction_d C D)
  : is_pseudo (left_adjoint_d F).
Proof.
  apply left_adjoint_pseudo_d.
Defined.

Global Instance right_adjoint_pseudo_functor
       `{Univalence}
       {C D : BiCategory}
       (F : BiAdjunction_d C D)
  : is_pseudo (right_adjoint_d F).
Proof.
  apply right_adjoint_pseudo_d.
Defined.

Definition triangle_l_lhs
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction_d C D)
  : LaxTransformation (left_adjoint_d F) (left_adjoint_d F)
  := compose
       (lax_right_identity_inv (left_adjoint_d F))
       (compose
          (whisker_L (left_adjoint_d F) (unit_d F))
          (compose
             (lax_associativity_inv _ _ _)
             (compose
                (whisker_R (left_adjoint_d F) (counit_d F))
                (lax_left_identity (left_adjoint_d F))
             )
          )
       ).

(*
Definition laxnaturality_of_triangle_l_lhs
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction_d C D)
           {X Y : C}
           (f : C⟦X,Y⟧)
  : laxnaturality_of (triangle_l_lhs F) f
    =
    (assoc_inv _ _ _)
      ∘ (_ ◅ (left_unit_inv _ ∘ right_unit _))
      ∘ assoc _ _ _
      ∘ ((assoc_inv _ _ _)
           ∘ _ ◅ ((Fcomp₁_inv _ _ _)
                    ∘ (_ ₂ (laxnaturality_of (unit_d F) f))
                    ∘ Fcomp₁ _ _ _)
           ∘ assoc _ _ _
           ∘ ((assoc_inv _ _ _)
                ∘ _ ◅ (left_unit_inv _ ∘ right_unit _)
                ∘ assoc _ _ _
                ∘ ((assoc_inv _ _ _)
                     ∘ _ ◅ (laxnaturality_of (counit_d F) _)
                     ∘ assoc _ _ _
                     ∘ (left_unit_inv _ ∘ right_unit _) ▻ _
                     ∘ assoc_inv _ _ _) ▻ _
                ∘ assoc_inv _ _ _) ▻ _
           ∘ assoc_inv _ _ _) ▻ _
      ∘ assoc_inv _ _ _.
Proof.
  reflexivity.
Qed.
*)

Definition triangle_r_lhs
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction_d C D)
  : LaxTransformation (right_adjoint_d F) (right_adjoint_d F)
  := compose
       (lax_left_identity_inv (right_adjoint_d F))
       (compose
          (whisker_R (right_adjoint_d F) (unit_d F))
          (compose
             (lax_associativity _ _ _)
             (compose
                (whisker_L (right_adjoint_d F) (counit_d F))
                (lax_right_identity (right_adjoint_d F))
             )
          )
       ).

(*
Definition laxnaturality_of_triangle_r_lhs
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction_d C D)
           {X Y : D}
           (f : D⟦X,Y⟧)
  : laxnaturality_of (triangle_r_lhs F) f = ?
 *)
Record is_biadjunction
       `{Univalence}
       {C D : BiCategory}
       (F : BiAdjunction_d C D)
  := Build_is_biadjunction
       {
         unit_pseudo_p : is_pseudo_transformation (unit_d F) ;
         counit_pseudo_p : is_pseudo_transformation (counit_d F) ;
         adj_triangle_l_p :
           IsoModification
             (triangle_l_lhs F)
             (identity_transformation (left_adjoint_d F)) ;
         adj_triangle_r_p :
           IsoModification
             (triangle_r_lhs F)
             (identity_transformation (right_adjoint_d F))
       }.

Arguments Build_is_biadjunction {_ C D F} _ _ _ _.
Ltac make_is_biadjunction := simple refine (Build_is_biadjunction _ _ _ _).
Arguments unit_pseudo_p {_ C D F} _.
Arguments counit_pseudo_p {_ C D F} _.
Arguments adj_triangle_l_p {_ C D F} _.
Arguments adj_triangle_r_p {_ C D F} _.

Definition BiAdjunction
           `{Univalence}
           (C D : BiCategory)
  : Type
  := {F : BiAdjunction_d C D & is_biadjunction F}.

Definition Build_BiAdjunction
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction_d C D)
           (HF : is_biadjunction F)
  : BiAdjunction C D
  := (F;HF).

Definition left_adjoint
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction C D)
  : LaxFunctor C D
  := left_adjoint_d F.1.

Global Instance left_adjoint_pseudo
       `{Univalence}
       {C D : BiCategory}
       (F : BiAdjunction C D)
  : is_pseudo (left_adjoint F)
  := _.

Definition right_adjoint
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction C D)
  : LaxFunctor D C
  := right_adjoint_d F.1.

Global Instance right_adjoint_pseudo
       `{Univalence}
       {C D : BiCategory}
       (F : BiAdjunction C D)
  : is_pseudo (right_adjoint F)
  := _.

Definition unit
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction C D)
  := unit_d F.1.

Definition counit
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction C D)
  := counit_d F.1.

Definition adj_triangle_l
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction C D)
  : IsoModification
      (triangle_l_lhs F.1)
      (identity_transformation (left_adjoint F))
  := adj_triangle_l_p F.2.

Definition adj_triangle_r
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction C D)
  : IsoModification
      (triangle_r_lhs F.1)
      (identity_transformation (right_adjoint F))
  := adj_triangle_r_p F.2.

Definition is_biequivalence
           `{Univalence}
           {C D : BiCategory}
           (F : BiAdjunction C D)
  : Type
  := (@is_adjoint_equivalence (Lax C C)
                              (lax_id_functor C).1
                              (lax_comp (right_adjoint F) (left_adjoint F))
                              (unit F))
     *
     (@is_adjoint_equivalence (Lax D D)
                              (lax_comp (left_adjoint F) (right_adjoint F))
                              (lax_id_functor D).1
                              (counit F)).

Ltac make_is_biequivalence := split.

Definition BiEquivalence
       `{Univalence}
       (C D : BiCategory)
  := {F : BiAdjunction C D & is_biequivalence F}.

Ltac make_biequivalence := simple refine (_;_).

author: nmvdw

repo: groupoids

save_path: github-repos/coq/nmvdw-groupoids