(* -*- mode: coq; mode: visual-line -*- *)
Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import HSet.
Require Import Spaces.Nat.Core.
Require Import Equiv.PathSplit.

(** By setting this, using [simple_induction] instead of [induction], and specifying universe variables in a couple of places, we can avoid all universe variables in this file.  Several results are confirmed to use no universe variables with an @{} annotation. *)
Local Set Universe Minimization ToSet.

Local Open Scope path_scope.
Local Open Scope nat_scope.

(** * Finite sets *)

(** ** Canonical finite sets *)

(** A *finite set* is a type that is merely equivalent to the canonical finite set determined by some natural number.  There are many equivalent ways to define the canonical finite sets, such as [{ k : nat & k < n}]; we instead choose a recursive one. *)

Fixpoint Fin (n : nat) : Type0
  := match n with
       | 0 => Empty
       | S n => Fin n + Unit
     end.

Fixpoint fin_to_nat {n} : Fin n -> nat
  := match n with
     | 0 => Empty_rec
     | S n' =>
       fun k =>
         match k with
         | inl k' => fin_to_nat k'
         | inr tt => n'
         end
     end.

Global Instance decidable_fin (n : nat)
: Decidable (Fin n).
n: nat
Decidable (Fin n)
Proof.
n: nat
Decidable (Fin n)
  destruct n as [|n]; try exact _.
n: nat
Decidable (Fin n.+1)
  exact (inl (inr tt)).
Defined.

Global Instance decidablepaths_fin@{} (n : nat)
: DecidablePaths (Fin n).
n: nat
DecidablePaths (Fin n)
Proof.
n: nat
DecidablePaths (Fin n)
  simple_induction n n IHn; simpl; exact _.
Defined.

Global Instance contr_fin1 : Contr (Fin 1).
Contr (Fin 1)
Proof.
Contr (Fin 1)
  refine (contr_equiv' Unit (sum_empty_l Unit)^-1).
Defined.

Definition fin_empty (n : nat) (f : Fin n -> Empty) : n = 0.
n: nat
f: Fin n -> Empty
n = 0
Proof.
n: nat
f: Fin n -> Empty
n = 0
  destruct n; [ reflexivity | ].
n: nat
f: Fin n.+1 -> Empty
n.+1 = 0
  elim (f (inr tt)).
Defined.

(** The zeroth element of a non-empty finite set is the left most element. It also happens to be the biggest by termsize. *)
Fixpoint fin_zero {n : nat} : Fin n.+1 :=
  match n with
  | O => inr tt
  | S _ => inl fin_zero
  end.

(** Where `fin_zero` computes the first element of Fin (S n), `fin_last` computes the last. *)
Definition fin_last {n : nat} : Fin (S n) := inr tt.

(** Injection Fin n -> Fin n.+1 mapping the kth element to the kth element. *)
Definition fin_incl {n : nat} (k : Fin n) : Fin (S n) := inl k.

(** There is an injection from Fin n -> Fin n.+1 that maps the kth element to the (k+1)th element. *)
Fixpoint fsucc {n : nat} : Fin n -> Fin n.+1 :=
  match n with
  | O => Empty_rec
  | S n' =>
    fun i : Fin (S n') =>
      match i with
      | inl i' => inl (fsucc i')
      | inr tt => inr tt
      end
  end.

(** This injection is an injection/embedding *)
Lemma isembedding_fsucc@{} {n : nat} : IsEmbedding (@fsucc n).
n: nat
IsEmbedding fsucc
Proof.
n: nat
IsEmbedding fsucc
  apply isembedding_isinj_hset.
n: nat
isinj fsucc
  simple_induction n n IHn.
isinj fsucc
n: nat
IHn: isinj fsucc
isinj fsucc
  -
isinj fsucc intro i.
i: Fin 0
forall x1 : Fin 0, fsucc i = fsucc x1 -> i = x1 elim i.
  -
n: nat
IHn: isinj fsucc
isinj fsucc intros [] []; intro p.
n: nat
IHn: isinj fsucc
f, f0: Fin n
p: fsucc (inl f) = fsucc (inl f0)
inl f = inl f0
n: nat
IHn: isinj fsucc
f: Fin n
u: Unit
p: fsucc (inl f) = fsucc (inr u)
inl f = inr u
n: nat
IHn: isinj fsucc
u: Unit
f: Fin n
p: fsucc (inr u) = fsucc (inl f)
inr u = inl f
n: nat
IHn: isinj fsucc
u, u0: Unit
p: fsucc (inr u) = fsucc (inr u0)
inr u = inr u0
    +
n: nat
IHn: isinj fsucc
f, f0: Fin n
p: fsucc (inl f) = fsucc (inl f0)
inl f = inl f0 f_ap.
n: nat
IHn: isinj fsucc
f, f0: Fin n
p: fsucc (inl f) = fsucc (inl f0)
f = f0 apply IHn.
n: nat
IHn: isinj fsucc
f, f0: Fin n
p: fsucc (inl f) = fsucc (inl f0)
fsucc f = fsucc f0 eapply path_sum_inl.
n: nat
IHn: isinj fsucc
f, f0: Fin n
p: fsucc (inl f) = fsucc (inl f0)
inl (fsucc f) = inl (fsucc f0) exact p.
    +
n: nat
IHn: isinj fsucc
f: Fin n
u: Unit
p: fsucc (inl f) = fsucc (inr u)
inl f = inr u destruct u.
n: nat
IHn: isinj fsucc
f: Fin n
p: fsucc (inl f) = fsucc (inr tt)
inl f = inr tt elim (inl_ne_inr _ _ p).
    +
n: nat
IHn: isinj fsucc
u: Unit
f: Fin n
p: fsucc (inr u) = fsucc (inl f)
inr u = inl f destruct u.
n: nat
IHn: isinj fsucc
f: Fin n
p: fsucc (inr tt) = fsucc (inl f)
inr tt = inl f elim (inr_ne_inl _ _ p).
    +
n: nat
IHn: isinj fsucc
u, u0: Unit
p: fsucc (inr u) = fsucc (inr u0)
inr u = inr u0 destruct u, u0; reflexivity.
Defined.

Lemma path_fin_fsucc_incl {n : nat} : forall k : Fin n, fsucc (fin_incl k) = fin_incl (fsucc k).
n: nat
forall k : Fin n,
fsucc (fin_incl k) = fin_incl (fsucc k)
Proof.
n: nat
forall k : Fin n,
fsucc (fin_incl k) = fin_incl (fsucc k)
  trivial.
Defined.

Definition path_nat_fin_incl {n : nat} (k : Fin n)
  : fin_to_nat (fin_incl k) = fin_to_nat k
  := 1.

Lemma path_nat_fsucc@{} {n : nat} : forall k : Fin n, fin_to_nat (fsucc k) = S (fin_to_nat k).
n: nat
forall k : Fin n,
fin_to_nat (fsucc k) = (fin_to_nat k).+1
Proof.
n: nat
forall k : Fin n,
fin_to_nat (fsucc k) = (fin_to_nat k).+1
  simple_induction n n IHn.
forall k : Fin 0,
fin_to_nat (fsucc k) = (fin_to_nat k).+1
n: nat
IHn: forall k : Fin n, fin_to_nat (fsucc k) = (fin_to_nat k).+1
forall k : Fin n.+1,
fin_to_nat (fsucc k) = (fin_to_nat k).+1
  -
forall k : Fin 0,
fin_to_nat (fsucc k) = (fin_to_nat k).+1 intros [].
  -
n: nat
IHn: forall k : Fin n, fin_to_nat (fsucc k) = (fin_to_nat k).+1
forall k : Fin n.+1,
fin_to_nat (fsucc k) = (fin_to_nat k).+1 intros [k'|[]].
n: nat
IHn: forall k : Fin n, fin_to_nat (fsucc k) = (fin_to_nat k).+1
k': Fin n
fin_to_nat (fsucc (inl k')) = (fin_to_nat (inl k')).+1
n: nat
IHn: forall k : Fin n, fin_to_nat (fsucc k) = (fin_to_nat k).+1
fin_to_nat (fsucc (inr tt)) = (fin_to_nat (inr tt)).+1
    +
n: nat
IHn: forall k : Fin n, fin_to_nat (fsucc k) = (fin_to_nat k).+1
k': Fin n
fin_to_nat (fsucc (inl k')) = (fin_to_nat (inl k')).+1 rewrite path_fin_fsucc_incl, path_nat_fin_incl.
n: nat
IHn: forall k : Fin n, fin_to_nat (fsucc k) = (fin_to_nat k).+1
k': Fin n
fin_to_nat (fsucc k') = (fin_to_nat (inl k')).+1
      apply IHn.
    +
n: nat
IHn: forall k : Fin n, fin_to_nat (fsucc k) = (fin_to_nat k).+1
fin_to_nat (fsucc (inr tt)) = (fin_to_nat (inr tt)).+1 reflexivity.
Defined.

Lemma path_nat_fin_zero@{} {n} : fin_to_nat (@fin_zero n) = 0.
n: nat
fin_to_nat fin_zero = 0
Proof.
n: nat
fin_to_nat fin_zero = 0
  simple_induction n n IHn.
fin_to_nat fin_zero = 0
n: nat
IHn: fin_to_nat fin_zero = 0
fin_to_nat fin_zero = 0
  -
fin_to_nat fin_zero = 0 reflexivity.
  -
n: nat
IHn: fin_to_nat fin_zero = 0
fin_to_nat fin_zero = 0 trivial.
Defined.

Definition path_nat_fin_last {n} : fin_to_nat (@fin_last n) = n
  := 1.

(** ** Transposition equivalences *)

(** To prove some basic facts about canonical finite sets, we need some standard automorphisms of them.  Here we define some transpositions and prove that they in fact do the desired things. *)

(** *** Swap the last two elements. *)

Definition fin_transpose_last_two (n : nat)
  : Fin n.+2 <~> Fin n.+2
  := ((equiv_sum_assoc _ _ _)^-1)
       oE (1 +E (equiv_sum_symm _ _))
       oE (equiv_sum_assoc _ _ _).

Arguments fin_transpose_last_two : simpl nomatch.

Definition fin_transpose_last_two_last (n : nat)
  : fin_transpose_last_two n (inr tt) = (inl (inr tt))
  := 1.

Definition fin_transpose_last_two_nextlast (n : nat)
  : fin_transpose_last_two n (inl (inr tt)) = (inr tt)
  := 1.

Definition fin_transpose_last_two_rest (n : nat) (k : Fin n)
  : fin_transpose_last_two n (inl (inl k)) = (inl (inl k))
  := 1.

(** *** Swap the last element with [k]. *)

Fixpoint fin_transpose_last_with (n : nat) (k : Fin n.+1)
  : Fin n.+1 <~> Fin n.+1.
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
k: Fin n.+1
Fin n.+1 <~> Fin n.+1
Proof.
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
k: Fin n.+1
Fin n.+1 <~> Fin n.+1
  destruct k as [k|].
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
k: Fin n
Fin n.+1 <~> Fin n.+1
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
u: Unit
Fin n.+1 <~> Fin n.+1
  -
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
k: Fin n
Fin n.+1 <~> Fin n.+1 destruct n as [|n].
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
k: Fin 0
Fin 1 <~> Fin 1
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
k: Fin n.+1
Fin n.+2 <~> Fin n.+2
    +
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
k: Fin 0
Fin 1 <~> Fin 1 elim k.
    +
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
k: Fin n.+1
Fin n.+2 <~> Fin n.+2 destruct k as [k|].
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
k: Fin n
Fin n.+2 <~> Fin n.+2
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
u: Unit
Fin n.+2 <~> Fin n.+2
      *
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
k: Fin n
Fin n.+2 <~> Fin n.+2 refine ((fin_transpose_last_two n)
                  oE _
                  oE (fin_transpose_last_two n)).
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
k: Fin n
Fin n.+2 <~> Fin n.+2
        refine ((fin_transpose_last_with n (inl k)) +E 1).
      *
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
u: Unit
Fin n.+2 <~> Fin n.+2 apply fin_transpose_last_two.
  -
fin_transpose_last_with: forall n : nat,
Fin n.+1 ->
Fin n.+1 <~> Fin n.+1
n: nat
u: Unit
Fin n.+1 <~> Fin n.+1 exact (equiv_idmap _).
Defined.

Arguments fin_transpose_last_with : simpl nomatch.

Definition fin_transpose_last_with_last@{} (n : nat) (k : Fin n.+1)
  : fin_transpose_last_with n k (inr tt) = k.
n: nat
k: Fin n.+1
fin_transpose_last_with n k (inr tt) = k
Proof.
n: nat
k: Fin n.+1
fin_transpose_last_with n k (inr tt) = k
  destruct k as [k|].
n: nat
k: Fin n
fin_transpose_last_with n (inl k) (inr tt) = inl k
n: nat
u: Unit
fin_transpose_last_with n (inr u) (inr tt) = inr u
  -
n: nat
k: Fin n
fin_transpose_last_with n (inl k) (inr tt) = inl k simple_induction n n IHn; intro k; simpl.
k: Fin 0
Overture.Empty_rec (Empty + Unit <~> Empty + Unit) k
  (inr tt) = inl k
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inr tt) = inl k
k: Fin n.+1
fin_transpose_last_with n.+1 (inl k) (inr tt) = inl k
    +
k: Fin 0
Overture.Empty_rec (Empty + Unit <~> Empty + Unit) k
  (inr tt) = inl k elim k.
    +
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inr tt) = inl k
k: Fin n.+1
fin_transpose_last_with n.+1 (inl k) (inr tt) = inl k destruct k as [k|].
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inr tt) = inl k
k: Fin n
fin_transpose_last_with n.+1 (inl (inl k)) (inr tt) =
inl (inl k)
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inr tt) = inl k
u: Unit
fin_transpose_last_with n.+1 (inl (inr u)) (inr tt) =
inl (inr u)
      *
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inr tt) = inl k
k: Fin n
fin_transpose_last_with n.+1 (inl (inl k)) (inr tt) =
inl (inl k) simpl.
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inr tt) = inl k
k: Fin n
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match
      fin_transpose_last_with n (inl k) (inr tt)
    with
    | inl a => inl a
    | inr b => inr (inl b)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl (inl k) rewrite IHn; reflexivity.
      *
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inr tt) = inl k
u: Unit
fin_transpose_last_with n.+1 (inl (inr u)) (inr tt) =
inl (inr u) simpl.
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inr tt) = inl k
u: Unit
inl (inr tt) = inl (inr u) apply ap, ap, path_contr.
  - (** We have to destruct [n] since fixpoints don't reduce unless their argument is a constructor. *)
n: nat
u: Unit
fin_transpose_last_with n (inr u) (inr tt) = inr u
    destruct n; simpl.
u: Unit
inr tt = inr u
n: nat
u: Unit
inr tt = inr u
    all:apply ap, path_contr.
Qed.

Definition fin_transpose_last_with_with@{} (n : nat) (k : Fin n.+1)
  : fin_transpose_last_with n k k = inr tt.
n: nat
k: Fin n.+1
fin_transpose_last_with n k k = inr tt
Proof.
n: nat
k: Fin n.+1
fin_transpose_last_with n k k = inr tt
  destruct k as [k|].
n: nat
k: Fin n
fin_transpose_last_with n (inl k) (inl k) = inr tt
n: nat
u: Unit
fin_transpose_last_with n (inr u) (inr u) = inr tt
  -
n: nat
k: Fin n
fin_transpose_last_with n (inl k) (inl k) = inr tt simple_induction n n IHn; intro k; simpl.
k: Fin 0
Overture.Empty_rec (Empty + Unit <~> Empty + Unit) k
  (inl k) = inr tt
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inl k) = inr tt
k: Fin n.+1
fin_transpose_last_with n.+1 (inl k) (inl k) = inr tt
    +
k: Fin 0
Overture.Empty_rec (Empty + Unit <~> Empty + Unit) k
  (inl k) = inr tt elim k.
    +
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inl k) = inr tt
k: Fin n.+1
fin_transpose_last_with n.+1 (inl k) (inl k) = inr tt destruct k as [|k]; simpl.
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inl k) = inr tt
f: Fin n
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match
      fin_transpose_last_with n (inl f) (inl f)
    with
    | inl a => inl a
    | inr b => inr (inl b)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inr tt
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inl k) = inr tt
k: Unit
inr k = inr tt
      *
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inl k) = inr tt
f: Fin n
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match
      fin_transpose_last_with n (inl f) (inl f)
    with
    | inl a => inl a
    | inr b => inr (inl b)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inr tt rewrite IHn; reflexivity.
      *
n: nat
IHn: forall k : Fin n, fin_transpose_last_with n (inl k) (inl k) = inr tt
k: Unit
inr k = inr tt apply ap, path_contr.
  -
n: nat
u: Unit
fin_transpose_last_with n (inr u) (inr u) = inr tt destruct n; simpl.
u: Unit
inr u = inr tt
n: nat
u: Unit
inr u = inr tt
    all:apply ap, path_contr.
Qed.

Definition fin_transpose_last_with_rest@{} (n : nat)
  (k : Fin n.+1) (l : Fin n)
  (notk : k <> inl l)
  : fin_transpose_last_with n k (inl l) = (inl l).
n: nat
k: Fin n.+1
l: Fin n
notk: k <> inl l
fin_transpose_last_with n k (inl l) = inl l
Proof.
n: nat
k: Fin n.+1
l: Fin n
notk: k <> inl l
fin_transpose_last_with n k (inl l) = inl l
  destruct k as [k|].
n: nat
k, l: Fin n
notk: inl k <> inl l
fin_transpose_last_with n (inl k) (inl l) = inl l
n: nat
u: Unit
l: Fin n
notk: inr u <> inl l
fin_transpose_last_with n (inr u) (inl l) = inl l
  -
n: nat
k, l: Fin n
notk: inl k <> inl l
fin_transpose_last_with n (inl k) (inl l) = inl l simple_induction n n IHn; intros k l notk; simpl.
k, l: Fin 0
notk: inl k <> inl l
Overture.Empty_rec (Empty + Unit <~> Empty + Unit) k
  (inl l) = inl l
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k, l: Fin n.+1
notk: inl k <> inl l
fin_transpose_last_with n.+1 (inl k) (inl l) = inl l
    1: elim k.
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k, l: Fin n.+1
notk: inl k <> inl l
fin_transpose_last_with n.+1 (inl k) (inl l) = inl l
    destruct k as [k|]; simpl.
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k: Fin n
l: Fin n.+1
notk: inl (inl k) <> inl l
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match
      functor_sum (fin_transpose_last_with n (inl k))
        idmap
        match
          functor_sum idmap
            (fun ab : Unit + Unit =>
             match ab with
             | inl a => inr a
             | inr b => inl b
             end)
            match l with
            | inl a => inl a
            | inr b => inr (inl b)
            end
        with
        | inl a => inl (inl a)
        | inr (inl b) => inl (inr b)
        | inr (inr c) => inr c
        end
    with
    | inl (inl a) => inl a
    | inl (inr b) => inr (inl b)
    | inr c => inr (inr c)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl l
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
u: Unit
l: Fin n.+1
notk: inl (inr u) <> inl l
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match l with
    | inl a => inl a
    | inr b => inr (inl b)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl l
    {
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k: Fin n
l: Fin n.+1
notk: inl (inl k) <> inl l
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match
      functor_sum (fin_transpose_last_with n (inl k))
        idmap
        match
          functor_sum idmap
            (fun ab : Unit + Unit =>
             match ab with
             | inl a => inr a
             | inr b => inl b
             end)
            match l with
            | inl a => inl a
            | inr b => inr (inl b)
            end
        with
        | inl a => inl (inl a)
        | inr (inl b) => inl (inr b)
        | inr (inr c) => inr c
        end
    with
    | inl (inl a) => inl a
    | inl (inr b) => inr (inl b)
    | inr c => inr (inr c)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl l destruct l as [l|]; simpl.
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k, l: Fin n
notk: inl (inl k) <> inl (inl l)
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match
      fin_transpose_last_with n (inl k) (inl l)
    with
    | inl a => inl a
    | inr b => inr (inl b)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl (inl l)
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k: Fin n
u: Unit
notk: inl (inl k) <> inl (inr u)
inl (inr u) = inl (inr u)
      -
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k, l: Fin n
notk: inl (inl k) <> inl (inl l)
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match
      fin_transpose_last_with n (inl k) (inl l)
    with
    | inl a => inl a
    | inr b => inr (inl b)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl (inl l) rewrite IHn.
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k, l: Fin n
notk: inl (inl k) <> inl (inl l)
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end) (inl l)
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl (inl l)
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k, l: Fin n
notk: inl (inl k) <> inl (inl l)
inl k <> inl l
        +
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k, l: Fin n
notk: inl (inl k) <> inl (inl l)
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end) (inl l)
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl (inl l) reflexivity.
        +
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k, l: Fin n
notk: inl (inl k) <> inl (inl l)
inl k <> inl l exact (fun p => notk (ap inl p)).
      -
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
k: Fin n
u: Unit
notk: inl (inl k) <> inl (inr u)
inl (inr u) = inl (inr u) reflexivity. }
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
u: Unit
l: Fin n.+1
notk: inl (inr u) <> inl l
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match l with
    | inl a => inl a
    | inr b => inr (inl b)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl l
    {
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
u: Unit
l: Fin n.+1
notk: inl (inr u) <> inl l
match
  functor_sum idmap
    (fun ab : Unit + Unit =>
     match ab with
     | inl a => inr a
     | inr b => inl b
     end)
    match l with
    | inl a => inl a
    | inr b => inr (inl b)
    end
with
| inl a => inl (inl a)
| inr (inl b) => inl (inr b)
| inr (inr c) => inr c
end = inl l destruct l as [l|]; simpl.
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
u: Unit
l: Fin n
notk: inl (inr u) <> inl (inl l)
inl (inl l) = inl (inl l)
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
u, u0: Unit
notk: inl (inr u) <> inl (inr u0)
inr u0 = inl (inr u0)
      -
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
u: Unit
l: Fin n
notk: inl (inr u) <> inl (inl l)
inl (inl l) = inl (inl l) reflexivity.
      -
n: nat
IHn: forall k l : Fin n,
inl k <> inl l ->
fin_transpose_last_with n (inl k) (inl l) =
inl l
u, u0: Unit
notk: inl (inr u) <> inl (inr u0)
inr u0 = inl (inr u0) elim (notk (ap inl (ap inr (path_unit _ _)))). }
  -
n: nat
u: Unit
l: Fin n
notk: inr u <> inl l
fin_transpose_last_with n (inr u) (inl l) = inl l destruct n; reflexivity.
Defined.

Definition fin_transpose_last_with_last_other (n : nat) (k : Fin n.+1)
  : fin_transpose_last_with n (inr tt) k = k.
n: nat
k: Fin n.+1
fin_transpose_last_with n (inr tt) k = k
Proof.
n: nat
k: Fin n.+1
fin_transpose_last_with n (inr tt) k = k
  destruct n; reflexivity.
Defined.

Definition fin_transpose_last_with_invol (n : nat) (k : Fin n.+1)
  : fin_transpose_last_with n k o fin_transpose_last_with n k == idmap.
n: nat
k: Fin n.+1
fin_transpose_last_with n k
o fin_transpose_last_with n k == idmap
Proof.
n: nat
k: Fin n.+1
fin_transpose_last_with n k
o fin_transpose_last_with n k == idmap
  intros l.
n: nat
k, l: Fin n.+1
fin_transpose_last_with n k
  (fin_transpose_last_with n k l) = l
  destruct l as [l|[]].
n: nat
k: Fin n.+1
l: Fin n
fin_transpose_last_with n k
  (fin_transpose_last_with n k (inl l)) = inl l
n: nat
k: Fin n.+1
fin_transpose_last_with n k
  (fin_transpose_last_with n k (inr tt)) = inr tt
  -
n: nat
k: Fin n.+1
l: Fin n
fin_transpose_last_with n k
  (fin_transpose_last_with n k (inl l)) = inl l destruct k as [k|[]].
n: nat
k, l: Fin n
fin_transpose_last_with n (inl k)
  (fin_transpose_last_with n (inl k) (inl l)) = inl l
n: nat
l: Fin n
fin_transpose_last_with n (inr tt)
  (fin_transpose_last_with n (inr tt) (inl l)) = inl l
    {
n: nat
k, l: Fin n
fin_transpose_last_with n (inl k)
  (fin_transpose_last_with n (inl k) (inl l)) = inl l destruct (dec_paths k l) as [p|p].
n: nat
k, l: Fin n
p: k = l
fin_transpose_last_with n (inl k)
  (fin_transpose_last_with n (inl k) (inl l)) = inl l
n: nat
k, l: Fin n
p: k <> l
fin_transpose_last_with n (inl k)
  (fin_transpose_last_with n (inl k) (inl l)) = inl l
      -
n: nat
k, l: Fin n
p: k = l
fin_transpose_last_with n (inl k)
  (fin_transpose_last_with n (inl k) (inl l)) = inl l rewrite p.
n: nat
k, l: Fin n
p: k = l
fin_transpose_last_with n (inl l)
  (fin_transpose_last_with n (inl l) (inl l)) = inl l
        rewrite fin_transpose_last_with_with.
n: nat
k, l: Fin n
p: k = l
fin_transpose_last_with n (inl l) (inr tt) = inl l
        apply fin_transpose_last_with_last.
      -
n: nat
k, l: Fin n
p: k <> l
fin_transpose_last_with n (inl k)
  (fin_transpose_last_with n (inl k) (inl l)) = inl l rewrite fin_transpose_last_with_rest;
          try apply fin_transpose_last_with_rest;
          exact (fun q => p (path_sum_inl _ q)). }
n: nat
l: Fin n
fin_transpose_last_with n (inr tt)
  (fin_transpose_last_with n (inr tt) (inl l)) = inl l
    +
n: nat
l: Fin n
fin_transpose_last_with n (inr tt)
  (fin_transpose_last_with n (inr tt) (inl l)) = inl l rewrite fin_transpose_last_with_last_other.
n: nat
l: Fin n
fin_transpose_last_with n (inr tt) (inl l) = inl l
      apply fin_transpose_last_with_last_other.
  -
n: nat
k: Fin n.+1
fin_transpose_last_with n k
  (fin_transpose_last_with n k (inr tt)) = inr tt rewrite fin_transpose_last_with_last.
n: nat
k: Fin n.+1
fin_transpose_last_with n k k = inr tt
    apply fin_transpose_last_with_with.
Defined.

(** ** Equivalences between canonical finite sets *)

(** To give an equivalence [Fin n.+1 <~> Fin m.+1] is equivalent to giving an element of [Fin m.+1] (the image of the last element) together with an equivalence [Fin n <~> Fin m].  More specifically, any such equivalence can be decomposed uniquely as a last-element transposition followed by an equivalence fixing the last element.  *)

(** Here is the uncurried map that constructs an equivalence [Fin n.+1 <~> Fin m.+1]. *)
Definition fin_equiv (n m : nat)
  (k : Fin m.+1) (e : Fin n <~> Fin m)
  : Fin n.+1 <~> Fin m.+1
  := (fin_transpose_last_with m k) oE (e +E 1).

(** Here is the curried version that we will prove to be an equivalence. *)
Definition fin_equiv' (n m : nat)
  : ((Fin m.+1) * (Fin n <~> Fin m)) -> (Fin n.+1 <~> Fin m.+1)
  := fun ke => fin_equiv n m (fst ke) (snd ke).

(** We construct its inverse and the two homotopies first as versions using homotopies without funext (similar to [ExtendableAlong]), then apply funext at the end. *)
Definition fin_equiv_hfiber@{} (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
  : { kf : (Fin m.+1) * (Fin n <~> Fin m) & fin_equiv' n m kf == e }.
n, m: nat
e: Fin n.+1 <~> Fin m.+1
{kf : Fin m.+1 * (Fin n <~> Fin m) &
fin_equiv' n m kf == e}
Proof.
n, m: nat
e: Fin n.+1 <~> Fin m.+1
{kf : Fin m.+1 * (Fin n <~> Fin m) &
fin_equiv' n m kf == e}
  simpl in e.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
{kf : Fin m.+1 * (Fin n <~> Fin m) &
fin_equiv' n m kf == e}
  refine (equiv_sigma_prod _ _).
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
{a : Fin m.+1 &
{b : Fin n <~> Fin m & fin_equiv' n m (a, b) == e}}
  recall (e (inr tt)) as y eqn:p.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: (Fin m + Unit)%type
p: e (inr tt) = y
{a : Fin m.+1 &
{b : Fin n <~> Fin m & fin_equiv' n m (a, b) == e}}
  assert (p' := (moveL_equiv_V _ _ p)^).
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: (Fin m + Unit)%type
p: e (inr tt) = y
p': e^-1 y = inr tt
{a : Fin m.+1 &
{b : Fin n <~> Fin m & fin_equiv' n m (a, b) == e}}
  exists y.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: (Fin m + Unit)%type
p: e (inr tt) = y
p': e^-1 y = inr tt
{b : Fin n <~> Fin m & fin_equiv' n m (y, b) == e}
  destruct y as [y|[]].
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
{b : Fin n <~> Fin m & fin_equiv' n m (inl y, b) == e}
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
{b : Fin n <~> Fin m &
fin_equiv' n m (inr tt, b) == e}
  +
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
{b : Fin n <~> Fin m & fin_equiv' n m (inl y, b) == e} simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set}
              (fin_transpose_last_with m (inl y) oE e)
              _ _ ; _).
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
forall a : Fin n,
is_inl
  ((fin_transpose_last_with m (inl y) oE e) (inl a))
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
forall b : Unit,
is_inr
  ((fin_transpose_last_with m (inl y) oE e) (inr b))
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
(fun b : Fin n <~> Fin m =>
 fin_equiv' n m (inl y, b) == e)
  (equiv_unfunctor_sum_l
     (fin_transpose_last_with m (inl y) oE e) ?Ha 
     ?Hb)
    {
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
forall a : Fin n,
is_inl
  ((fin_transpose_last_with m (inl y) oE e) (inl a)) intros a.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
a: Fin n
is_inl
  ((fin_transpose_last_with m (inl y) oE e) (inl a)) ev_equiv.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
a: Fin n
is_inl (fin_transpose_last_with m (inl y) (e (inl a)))
      assert (q : inl y <> e (inl a))
        by exact (fun z => inl_ne_inr _ _ (equiv_inj e (z^ @ p^))).
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
a: Fin n
q: inl y <> e (inl a)
is_inl (fin_transpose_last_with m (inl y) (e (inl a)))
      set (z := e (inl a)) in *.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
a: Fin n
z:= e (inl a): (Fin m + Unit)%type
q: inl y <> z
is_inl (fin_transpose_last_with m (inl y) z)
      destruct z as [z|[]].
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
a: Fin n
z: Fin m
q: inl y <> inl z
is_inl (fin_transpose_last_with m (inl y) (inl z))
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
a: Fin n
q: inl y <> inr tt
is_inl (fin_transpose_last_with m (inl y) (inr tt))
      -
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
a: Fin n
z: Fin m
q: inl y <> inl z
is_inl (fin_transpose_last_with m (inl y) (inl z)) rewrite fin_transpose_last_with_rest;
        try exact tt; try assumption.
      -
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
a: Fin n
q: inl y <> inr tt
is_inl (fin_transpose_last_with m (inl y) (inr tt)) rewrite fin_transpose_last_with_last; exact tt. }
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
forall b : Unit,
is_inr
  ((fin_transpose_last_with m (inl y) oE e) (inr b))
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
(fun b : Fin n <~> Fin m =>
 fin_equiv' n m (inl y, b) == e)
  (equiv_unfunctor_sum_l
     (fin_transpose_last_with m (inl y) oE e)
     (fun a : Fin n =>
      let q :=
        fun z : inl y = e (inl a) =>
        inl_ne_inr a tt (equiv_inj e (z^ @ p^)) in
      let z := e (inl a) in
      match
        z as s
        return
          (inl y <> s ->
           is_inl
             (fin_transpose_last_with m (inl y) s))
      with
      | inl f =>
          (fun (z0 : Fin m) (q0 : inl y <> inl z0) =>
           internal_paths_rew_r
             (fun f0 : Fin m.+1 => is_inl f0) tt
             (fin_transpose_last_with_rest m (inl y)
                z0 q0)) f
      | inr u =>
          (fun u0 : Unit =>
           match
             u0 as u1
             return
               (inl y <> inr u1 ->
                is_inl
                  (fin_transpose_last_with m (inl y)
                     (inr u1)))
           with
           | tt =>
               fun _ : inl y <> inr tt =>
               internal_paths_rew_r
                 (fun f : Fin m.+1 => is_inl f) tt
                 (fin_transpose_last_with_last m
                    (inl y))
           end) u
      end q) ?Hb)
    {
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
forall b : Unit,
is_inr
  ((fin_transpose_last_with m (inl y) oE e) (inr b)) intros [].
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
is_inr
  ((fin_transpose_last_with m (inl y) oE e) (inr tt)) ev_equiv.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
is_inr
  (fin_transpose_last_with m (inl y) (e (inr tt)))
      rewrite p.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
is_inr (fin_transpose_last_with m (inl y) (inl y))
      rewrite fin_transpose_last_with_with; exact tt. }
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
(fun b : Fin n <~> Fin m =>
 fin_equiv' n m (inl y, b) == e)
  (equiv_unfunctor_sum_l
     (fin_transpose_last_with m (inl y) oE e)
     (fun a : Fin n =>
      let q :=
        fun z : inl y = e (inl a) =>
        inl_ne_inr a tt (equiv_inj e (z^ @ p^)) in
      let z := e (inl a) in
      match
        z as s
        return
          (inl y <> s ->
           is_inl
             (fin_transpose_last_with m (inl y) s))
      with
      | inl f =>
          (fun (z0 : Fin m) (q0 : inl y <> inl z0) =>
           internal_paths_rew_r
             (fun f0 : Fin m.+1 => is_inl f0) tt
             (fin_transpose_last_with_rest m (inl y)
                z0 q0)) f
      | inr u =>
          (fun u0 : Unit =>
           match
             u0 as u1
             return
               (inl y <> inr u1 ->
                is_inl
                  (fin_transpose_last_with m (inl y)
                     (inr u1)))
           with
           | tt =>
               fun _ : inl y <> inr tt =>
               internal_paths_rew_r
                 (fun f : Fin m.+1 => is_inl f) tt
                 (fin_transpose_last_with_last m
                    (inl y))
           end) u
      end q)
     (fun b : Unit =>
      match
        b as u
        return
          (is_inr
             ((fin_transpose_last_with m (inl y) oE e)
                (inr u)))
      with
      | tt =>
          internal_paths_rew_r
            (fun s : Fin m + Unit =>
             is_inr
               (fin_transpose_last_with m (inl y) s))
            (internal_paths_rew_r
               (fun f : Fin m.+1 => is_inr f) tt
               (fin_transpose_last_with_with m (inl y)))
            p
      end))
    intros x.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
x: Fin n.+1
fin_equiv' n m
  (inl y,
  equiv_unfunctor_sum_l
    (fin_transpose_last_with m (inl y) oE e)
    (fun a : Fin n =>
     let q :=
       fun z : inl y = e (inl a) =>
       inl_ne_inr a tt (equiv_inj e (z^ @ p^)) in
     let z := e (inl a) in
     match
       z as s
       return
         (inl y <> s ->
          is_inl (fin_transpose_last_with m (inl y) s))
     with
     | inl f =>
         fun q0 : inl y <> inl f =>
         internal_paths_rew_r
           (fun f0 : Fin m.+1 => is_inl f0) tt
           (fin_transpose_last_with_rest m (inl y) f
              q0)
     | inr u =>
         match
           u as u0
           return
             (inl y <> inr u0 ->
              is_inl
                (fin_transpose_last_with m (inl y)
                   (inr u0)))
         with
         | tt =>
             fun _ : inl y <> inr tt =>
             internal_paths_rew_r
               (fun f : Fin m.+1 => is_inl f) tt
               (fin_transpose_last_with_last m (inl y))
         end
     end q)
    (fun b : Unit =>
     match
       b as u
       return
         (is_inr
            ((fin_transpose_last_with m (inl y) oE e)
               (inr u)))
     with
     | tt =>
         internal_paths_rew_r
           (fun s : Fin m + Unit =>
            is_inr
              (fin_transpose_last_with m (inl y) s))
           (internal_paths_rew_r
              (fun f : Fin m.+1 => is_inr f) tt
              (fin_transpose_last_with_with m (inl y)))
           p
     end)) x = e x unfold fst, snd; ev_equiv.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
x: Fin n.+1
fin_equiv' n m
  (inl y,
  equiv_unfunctor_sum_l
    (fin_transpose_last_with m (inl y) oE e)
    (fun a : Fin n =>
     match
       e (inl a) as s
       return
         (inl y <> s ->
          is_inl (fin_transpose_last_with m (inl y) s))
     with
     | inl f =>
         fun q : inl y <> inl f =>
         internal_paths_rew_r
           (fun f0 : Fin m.+1 => is_inl f0) tt
           (fin_transpose_last_with_rest m (inl y) f q)
     | inr u =>
         match
           u as u0
           return
             (inl y <> inr u0 ->
              is_inl
                (fin_transpose_last_with m (inl y)
                   (inr u0)))
         with
         | tt =>
             fun _ : inl y <> inr tt =>
             internal_paths_rew_r
               (fun f : Fin m.+1 => is_inl f) tt
               (fin_transpose_last_with_last m (inl y))
         end
     end
       (fun z : inl y = e (inl a) =>
        inl_ne_inr a tt (equiv_inj e (z^ @ p^))))
    (fun b : Unit =>
     match
       b as u
       return
         (is_inr
            ((fin_transpose_last_with m (inl y) o e)
               (inr u)))
     with
     | tt =>
         internal_paths_rew_r
           (fun s : Fin m + Unit =>
            is_inr
              (fin_transpose_last_with m (inl y) s))
           (internal_paths_rew_r
              (fun f : Fin m.+1 => is_inr f) tt
              (fin_transpose_last_with_with m (inl y)))
           p
     end)) x = e x simpl.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
x: Fin n.+1
fin_transpose_last_with m (inl y)
  (functor_sum
     (unfunctor_sum_l
        (fun x : Fin n + Unit =>
         fin_transpose_last_with m (inl y) (e x))
        (fun a : Fin n =>
         match
           e (inl a) as s
           return
             (inl y <> s ->
              is_inl
                (fin_transpose_last_with m (inl y) s))
         with
         | inl f =>
             fun q : inl y <> inl f =>
             internal_paths_rew_r
               (fun f0 : Fin m + Unit => is_inl f0) tt
               ((fix IHn (n0 : nat) :
                     forall k l : Fin n0,
                     inl k <> inl l ->
                     fin_transpose_last_with n0
                       (inl k) (inl l) = inl l :=
                   match
                     n0 as n
                     return
                       (forall k l : Fin n,
                        inl k <> inl l ->
                        fin_transpose_last_with n
                          (...) (...) = inl l)
                   with
                   | 0 =>
                       fun (k l : Empty)
                         (_ : inl k <> inl l) =>
                       Overture.Empty_rec
                         (Overture.Empty_rec
                            (Empty + Unit <~>
                             Empty + Unit) k (inl l) =
                          inl l) k
                   | n.+1 =>
                       fun (k l : Fin n + Unit)
                         (notk : inl k <> inl l) =>
                       match
                         k as s return (... -> ...)
                       with
                       | inl f0 =>
                           fun notk0 : ... <> ... =>
                           match ... with
                           | ... ...
                           | ... ...
                           end notk0
                       | inr u =>
                           fun notk0 : ... <> ... =>
                           match ... with
                           | ... ...
                           | ... ...
                           end notk0
                       end notk
                   end) m y f q)
         | inr u =>
             match
               u as u0
               return
                 (inl y <> inr u0 ->
                  is_inl
                    (fin_transpose_last_with m (inl y)
                       (inr u0)))
             with
             | tt =>
                 fun _ : inl y <> inr tt =>
                 internal_paths_rew_r
                   (fun f : Fin m + Unit => is_inl f)
                   tt
                   (fin_transpose_last_with_last m
                      (inl y))
             end
         end
           (fun z : inl y = e (inl a) =>
            inl_ne_inr a tt (equiv_inj e (z^ @ p^)))))
     idmap x) = e x
    destruct x as [x|[]]; simpl.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
x: Fin n
fin_transpose_last_with m (inl y)
  (inl
     (unfunctor_sum_l
        (fun x : Fin n + Unit =>
         fin_transpose_last_with m (inl y) (e x))
        (fun a : Fin n =>
         match
           e (inl a) as s
           return
             (inl y <> s ->
              is_inl
                (fin_transpose_last_with m (inl y) s))
         with
         | inl f =>
             fun q : inl y <> inl f =>
             internal_paths_rew_r
               (fun f0 : Fin m + Unit => is_inl f0) tt
               ((fix IHn (n0 : nat) :
                     forall k l : Fin n0,
                     inl k <> inl l ->
                     fin_transpose_last_with n0
                       (inl k) (inl l) = inl l :=
                   match
                     n0 as n
                     return
                       (forall k l : Fin n,
                        inl k <> inl l ->
                        fin_transpose_last_with n
                          (...) (...) = inl l)
                   with
                   | 0 =>
                       fun (k l : Empty)
                         (_ : inl k <> inl l) =>
                       Overture.Empty_rec
                         (Overture.Empty_rec
                            (Empty + Unit <~>
                             Empty + Unit) k (inl l) =
                          inl l) k
                   | n.+1 =>
                       fun (k l : Fin n + Unit)
                         (notk : inl k <> inl l) =>
                       match
                         k as s return (... -> ...)
                       with
                       | inl f0 =>
                           fun notk0 : ... <> ... =>
                           match ... with
                           | ... ...
                           | ... ...
                           end notk0
                       | inr u =>
                           fun notk0 : ... <> ... =>
                           match ... with
                           | ... ...
                           | ... ...
                           end notk0
                       end notk
                   end) m y f q)
         | inr u =>
             match
               u as u0
               return
                 (inl y <> inr u0 ->
                  is_inl
                    (fin_transpose_last_with m (inl y)
                       (inr u0)))
             with
             | tt =>
                 fun _ : inl y <> inr tt =>
                 internal_paths_rew_r
                   (fun f : Fin m + Unit => is_inl f)
                   tt
                   (fin_transpose_last_with_last m
                      (inl y))
             end
         end
           (fun z : inl y = e (inl a) =>
            inl_ne_inr a tt (equiv_inj e (z^ @ p^))))
        x)) = e (inl x)
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
fin_transpose_last_with m (inl y) (inr tt) =
e (inr tt)
    *
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
x: Fin n
fin_transpose_last_with m (inl y)
  (inl
     (unfunctor_sum_l
        (fun x : Fin n + Unit =>
         fin_transpose_last_with m (inl y) (e x))
        (fun a : Fin n =>
         match
           e (inl a) as s
           return
             (inl y <> s ->
              is_inl
                (fin_transpose_last_with m (inl y) s))
         with
         | inl f =>
             fun q : inl y <> inl f =>
             internal_paths_rew_r
               (fun f0 : Fin m + Unit => is_inl f0) tt
               ((fix IHn (n0 : nat) :
                     forall k l : Fin n0,
                     inl k <> inl l ->
                     fin_transpose_last_with n0
                       (inl k) (inl l) = inl l :=
                   match
                     n0 as n
                     return
                       (forall k l : Fin n,
                        inl k <> inl l ->
                        fin_transpose_last_with n
                          (...) (...) = inl l)
                   with
                   | 0 =>
                       fun (k l : Empty)
                         (_ : inl k <> inl l) =>
                       Overture.Empty_rec
                         (Overture.Empty_rec
                            (Empty + Unit <~>
                             Empty + Unit) k (inl l) =
                          inl l) k
                   | n.+1 =>
                       fun (k l : Fin n + Unit)
                         (notk : inl k <> inl l) =>
                       match
                         k as s return (... -> ...)
                       with
                       | inl f0 =>
                           fun notk0 : ... <> ... =>
                           match ... with
                           | ... ...
                           | ... ...
                           end notk0
                       | inr u =>
                           fun notk0 : ... <> ... =>
                           match ... with
                           | ... ...
                           | ... ...
                           end notk0
                       end notk
                   end) m y f q)
         | inr u =>
             match
               u as u0
               return
                 (inl y <> inr u0 ->
                  is_inl
                    (fin_transpose_last_with m (inl y)
                       (inr u0)))
             with
             | tt =>
                 fun _ : inl y <> inr tt =>
                 internal_paths_rew_r
                   (fun f : Fin m + Unit => is_inl f)
                   tt
                   (fin_transpose_last_with_last m
                      (inl y))
             end
         end
           (fun z : inl y = e (inl a) =>
            inl_ne_inr a tt (equiv_inj e (z^ @ p^))))
        x)) = e (inl x) rewrite unfunctor_sum_l_beta.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
x: Fin n
fin_transpose_last_with m (inl y)
  (fin_transpose_last_with m (inl y) (e (inl x))) =
e (inl x)
      apply fin_transpose_last_with_invol.
    *
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
y: Fin m
p: e (inr tt) = inl y
p': e^-1 (inl y) = inr tt
fin_transpose_last_with m (inl y) (inr tt) =
e (inr tt) refine (fin_transpose_last_with_last _ _ @ p^).
  +
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
{b : Fin n <~> Fin m &
fin_equiv' n m (inr tt, b) == e} simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set Set Set Set Set} e _ _ ; _).
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
forall a : Fin n, is_inl (e (inl a))
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
forall b : Unit, is_inr (e (inr b))
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
(fun b : Fin n <~> Fin m =>
 fin_equiv' n m (inr tt, b) == e)
  (equiv_unfunctor_sum_l e ?Ha ?Hb)
    {
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
forall a : Fin n, is_inl (e (inl a)) intros a.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
is_inl (e (inl a))
      destruct (is_inl_or_is_inr (e (inl a))) as [l|r].
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
l: is_inl (e (inl a))
is_inl (e (inl a))
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
r: is_inr (e (inl a))
is_inl (e (inl a))
      -
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
l: is_inl (e (inl a))
is_inl (e (inl a)) exact l.
      -
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
r: is_inr (e (inl a))
is_inl (e (inl a)) assert (q := inr_un_inr (e (inl a)) r).
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
r: is_inr (e (inl a))
q: inr (un_inr (e (inl a)) r) = e (inl a)
is_inl (e (inl a))
        apply moveR_equiv_V in q.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
r: is_inr (e (inl a))
q: e^-1 (inr (un_inr (e (inl a)) r)) = inl a
is_inl (e (inl a))
        assert (s := q^ @ ap (e^-1 o inr) (path_unit _ _) @ p').
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
r: is_inr (e (inl a))
q: e^-1 (inr (un_inr (e (inl a)) r)) = inl a
s: inl a = inr tt
is_inl (e (inl a))
        elim (inl_ne_inr _ _ s). }
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
forall b : Unit, is_inr (e (inr b))
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
(fun b : Fin n <~> Fin m =>
 fin_equiv' n m (inr tt, b) == e)
  (equiv_unfunctor_sum_l e
     (fun a : Fin n =>
      let s := is_inl_or_is_inr (e (inl a)) in
      match s with
      | inl i => idmap i
      | inr i =>
          (fun r : is_inr (e (inl a)) =>
           let q := inr_un_inr (e (inl a)) r in
           let q0 :=
             moveR_equiv_V
               (inr (un_inr (e (inl a)) r)) (inl a) q
             in
           let s0 :=
             (q0^ @
              ap (e^-1 o inr)
                (path_unit (un_inr (e (inl a)) r) tt)) @
             p' in
           Overture.Empty_rec (is_inl (e (inl a)))
             (inl_ne_inr a tt s0)) i
      end) ?Hb)
    {
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
forall b : Unit, is_inr (e (inr b)) intros []; exact (p^ # tt). }
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
(fun b : Fin n <~> Fin m =>
 fin_equiv' n m (inr tt, b) == e)
  (equiv_unfunctor_sum_l e
     (fun a : Fin n =>
      let s := is_inl_or_is_inr (e (inl a)) in
      match s with
      | inl i => idmap i
      | inr i =>
          (fun r : is_inr (e (inl a)) =>
           let q := inr_un_inr (e (inl a)) r in
           let q0 :=
             moveR_equiv_V
               (inr (un_inr (e (inl a)) r)) (inl a) q
             in
           let s0 :=
             (q0^ @
              ap (e^-1 o inr)
                (path_unit (un_inr (e (inl a)) r) tt)) @
             p' in
           Overture.Empty_rec (is_inl (e (inl a)))
             (inl_ne_inr a tt s0)) i
      end)
     (fun b : Unit =>
      match b as u return (is_inr (e (inr u))) with
      | tt => transport is_inr p^ tt
      end))
    intros x.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
x: Fin n.+1
fin_equiv' n m
  (inr tt,
  equiv_unfunctor_sum_l e
    (fun a : Fin n =>
     let s := is_inl_or_is_inr (e (inl a)) in
     match s with
     | inl i => i
     | inr i =>
         let q := inr_un_inr (e (inl a)) i in
         let q0 :=
           moveR_equiv_V (inr (un_inr (e (inl a)) i))
             (inl a) q in
         let s0 :=
           (q0^ @
            ap (fun x : Unit => e^-1 (inr x))
              (path_unit (un_inr (e (inl a)) i) tt)) @
           p' in
         Overture.Empty_rec (is_inl (e (inl a)))
           (inl_ne_inr a tt s0)
     end)
    (fun b : Unit =>
     match b as u return (is_inr (e (inr u))) with
     | tt => transport is_inr p^ tt
     end)) x = e x unfold fst, snd; ev_equiv.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
x: Fin n.+1
fin_equiv' n m
  (inr tt,
  equiv_unfunctor_sum_l e
    (fun a : Fin n =>
     match is_inl_or_is_inr (e (inl a)) with
     | inl i => i
     | inr i =>
         Overture.Empty_rec (is_inl (e (inl a)))
           (inl_ne_inr a tt
              (((moveR_equiv_V
                   (inr (un_inr (e (inl a)) i))
                   (inl a) (inr_un_inr (e (inl a)) i))^ @
                ap (fun x : Unit => e^-1 (inr x))
                  (path_unit (un_inr (e (inl a)) i) tt)) @
               p'))
     end)
    (fun b : Unit =>
     match b as u return (is_inr (e (inr u))) with
     | tt => transport is_inr p^ tt
     end)) x = e x simpl.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
x: Fin n.+1
fin_transpose_last_with m (inr tt)
  (functor_sum
     (unfunctor_sum_l e
        (fun a : Fin n =>
         match is_inl_or_is_inr (e (inl a)) with
         | inl i => i
         | inr i =>
             Overture.Empty_rec (is_inl (e (inl a)))
               (inl_ne_inr a tt
                  (((moveR_equiv_V
                       (inr (un_inr (e (inl a)) i))
                       (inl a)
                       (inr_un_inr (e (inl a)) i))^ @
                    ap (fun x : Unit => e^-1 (inr x))
                      (path_unit
                         (un_inr (e (inl a)) i) tt)) @
                   p'))
         end)) idmap x) = e x
    destruct x as [a|[]].
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
fin_transpose_last_with m (inr tt)
  (functor_sum
     (unfunctor_sum_l e
        (fun a : Fin n =>
         match is_inl_or_is_inr (e (inl a)) with
         | inl i => i
         | inr i =>
             Overture.Empty_rec (is_inl (e (inl a)))
               (inl_ne_inr a tt
                  (((moveR_equiv_V
                       (inr (un_inr (e (inl a)) i))
                       (inl a)
                       (inr_un_inr (e (inl a)) i))^ @
                    ap (fun x : Unit => e^-1 (inr x))
                      (path_unit
                         (un_inr (e (inl a)) i) tt)) @
                   p'))
         end)) idmap (inl a)) = e (inl a)
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
fin_transpose_last_with m (inr tt)
  (functor_sum
     (unfunctor_sum_l e
        (fun a : Fin n =>
         match is_inl_or_is_inr (e (inl a)) with
         | inl i => i
         | inr i =>
             Overture.Empty_rec (is_inl (e (inl a)))
               (inl_ne_inr a tt
                  (((moveR_equiv_V
                       (inr (un_inr (e (inl a)) i))
                       (inl a)
                       (inr_un_inr (e (inl a)) i))^ @
                    ap (fun x : Unit => e^-1 (inr x))
                      (path_unit
                         (un_inr (e (inl a)) i) tt)) @
                   p'))
         end)) idmap (inr tt)) = e (inr tt)
    *
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
fin_transpose_last_with m (inr tt)
  (functor_sum
     (unfunctor_sum_l e
        (fun a : Fin n =>
         match is_inl_or_is_inr (e (inl a)) with
         | inl i => i
         | inr i =>
             Overture.Empty_rec (is_inl (e (inl a)))
               (inl_ne_inr a tt
                  (((moveR_equiv_V
                       (inr (un_inr (e (inl a)) i))
                       (inl a)
                       (inr_un_inr (e (inl a)) i))^ @
                    ap (fun x : Unit => e^-1 (inr x))
                      (path_unit
                         (un_inr (e (inl a)) i) tt)) @
                   p'))
         end)) idmap (inl a)) = e (inl a) rewrite fin_transpose_last_with_last_other.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
a: Fin n
functor_sum
  (unfunctor_sum_l e
     (fun a : Fin n =>
      match is_inl_or_is_inr (e (inl a)) with
      | inl i => i
      | inr i =>
          Overture.Empty_rec (is_inl (e (inl a)))
            (inl_ne_inr a tt
               (((moveR_equiv_V
                    (inr (un_inr (e (inl a)) i))
                    (inl a) (inr_un_inr (e (inl a)) i))^ @
                 ap (fun x : Unit => e^-1 (inr x))
                   (path_unit (un_inr (e (inl a)) i)
                      tt)) @ p'))
      end)) idmap (inl a) = e (inl a)
      apply unfunctor_sum_l_beta.
    *
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
fin_transpose_last_with m (inr tt)
  (functor_sum
     (unfunctor_sum_l e
        (fun a : Fin n =>
         match is_inl_or_is_inr (e (inl a)) with
         | inl i => i
         | inr i =>
             Overture.Empty_rec (is_inl (e (inl a)))
               (inl_ne_inr a tt
                  (((moveR_equiv_V
                       (inr (un_inr (e (inl a)) i))
                       (inl a)
                       (inr_un_inr (e (inl a)) i))^ @
                    ap (fun x : Unit => e^-1 (inr x))
                      (path_unit
                         (un_inr (e (inl a)) i) tt)) @
                   p'))
         end)) idmap (inr tt)) = e (inr tt) simpl.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
fin_transpose_last_with m (inr tt) (inr tt) =
e (inr tt)
      rewrite fin_transpose_last_with_last.
n, m: nat
e: Fin n + Unit <~> Fin m + Unit
p: e (inr tt) = inr tt
p': e^-1 (inr tt) = inr tt
inr tt = e (inr tt)
      symmetry; apply p.
Qed.

Definition fin_equiv_inv (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
  : (Fin m.+1) * (Fin n <~> Fin m)
  := (fin_equiv_hfiber n m e).1.

Definition fin_equiv_issect (n m : nat) (e : Fin n.+1 <~> Fin m.+1)
  : fin_equiv' n m (fin_equiv_inv n m e) == e
  := (fin_equiv_hfiber n m e).2.

Definition fin_equiv_inj_fst (n m : nat)
           (k l : Fin m.+1) (e f : Fin n <~> Fin m)
  : (fin_equiv n m k e == fin_equiv n m l f) -> (k = l).
n, m: nat
k, l: Fin m.+1
e, f: Fin n <~> Fin m
fin_equiv n m k e == fin_equiv n m l f -> k = l
Proof.
n, m: nat
k, l: Fin m.+1
e, f: Fin n <~> Fin m
fin_equiv n m k e == fin_equiv n m l f -> k = l
  intros p.
n, m: nat
k, l: Fin m.+1
e, f: Fin n <~> Fin m
p: fin_equiv n m k e == fin_equiv n m l f
k = l
  refine (_ @ p (inr tt) @ _); simpl;
  rewrite fin_transpose_last_with_last; reflexivity.
Qed.

Definition fin_equiv_inj_snd (n m : nat)
           (k l : Fin m.+1) (e f : Fin n <~> Fin m)
  : (fin_equiv n m k e == fin_equiv n m l f) -> (e == f).
n, m: nat
k, l: Fin m.+1
e, f: Fin n <~> Fin m
fin_equiv n m k e == fin_equiv n m l f -> e == f
Proof.
n, m: nat
k, l: Fin m.+1
e, f: Fin n <~> Fin m
fin_equiv n m k e == fin_equiv n m l f -> e == f
  intros p.
n, m: nat
k, l: Fin m.+1
e, f: Fin n <~> Fin m
p: fin_equiv n m k e == fin_equiv n m l f
e == f
  intros x.
n, m: nat
k, l: Fin m.+1
e, f: Fin n <~> Fin m
p: fin_equiv n m k e == fin_equiv n m l f
x: Fin n
e x = f x assert (q := p (inr tt)); simpl in q.
n, m: nat
k, l: Fin m.+1
e, f: Fin n <~> Fin m
p: fin_equiv n m k e == fin_equiv n m l f
x: Fin n
q: fin_transpose_last_with m k (inr tt) =
fin_transpose_last_with m l (inr tt)
e x = f x
  rewrite !fin_transpose_last_with_last in q.
n, m: nat
k, l: Fin m.+1
e, f: Fin n <~> Fin m
p: fin_equiv n m k e == fin_equiv n m l f
x: Fin n
q: k = l
e x = f x
  rewrite <- q in p; clear q l.
n, m: nat
k: Fin m.+1
e, f: Fin n <~> Fin m
p: fin_equiv n m k e == fin_equiv n m k f
x: Fin n
e x = f x
  exact (path_sum_inl _
           (equiv_inj (fin_transpose_last_with m k) (p (inl x)))).
Qed.

(** Now it's time for funext. *)
Global Instance isequiv_fin_equiv `{Funext} (n m : nat)
  : IsEquiv (fin_equiv' n m).
H: Funext
n, m: nat
IsEquiv (fin_equiv' n m)
Proof.
H: Funext
n, m: nat
IsEquiv (fin_equiv' n m)
  refine (isequiv_pathsplit 0 _); split.
H: Funext
n, m: nat
forall a : Fin n.+1 <~> Fin m.+1,
hfiber (fin_equiv' n m) a
H: Funext
n, m: nat
forall x y : Fin m.+1 * (Fin n <~> Fin m),
PathSplit 1 (ap (fin_equiv' n m))
  -
H: Funext
n, m: nat
forall a : Fin n.+1 <~> Fin m.+1,
hfiber (fin_equiv' n m) a intros e; exists (fin_equiv_inv n m e).
H: Funext
n, m: nat
e: Fin n.+1 <~> Fin m.+1
fin_equiv' n m (fin_equiv_inv n m e) = e
    apply path_equiv, path_arrow, fin_equiv_issect.
  -
H: Funext
n, m: nat
forall x y : Fin m.+1 * (Fin n <~> Fin m),
PathSplit 1 (ap (fin_equiv' n m)) intros [k e] [l f]; simpl.
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
((forall
  a : fin_equiv' n m (k, e) = fin_equiv' n m (l, f),
  hfiber (ap (fin_equiv' n m)) a) *
 ((k, e) = (l, f) -> (k, e) = (l, f) -> Unit))%type
    refine (_ , fun _ _ => tt).
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
forall
a : fin_equiv' n m (k, e) = fin_equiv' n m (l, f),
hfiber (ap (fin_equiv' n m)) a
    intros p; refine (_ ; path_ishprop _ _).
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
p: fin_equiv' n m (k, e) = fin_equiv' n m (l, f)
(k, e) = (l, f)
    apply (ap equiv_fun) in p.
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
p: fin_equiv' n m (k, e) = fin_equiv' n m (l, f)
(k, e) = (l, f)
    apply ap10 in p.
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
p: fin_equiv' n m (k, e) == fin_equiv' n m (l, f)
(k, e) = (l, f)
    apply path_prod'.
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
p: fin_equiv' n m (k, e) == fin_equiv' n m (l, f)
k = l
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
p: fin_equiv' n m (k, e) == fin_equiv' n m (l, f)
e = f
    +
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
p: fin_equiv' n m (k, e) == fin_equiv' n m (l, f)
k = l refine (fin_equiv_inj_fst n m k l e f p).
    +
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
p: fin_equiv' n m (k, e) == fin_equiv' n m (l, f)
e = f apply path_equiv, path_arrow.
H: Funext
n, m: nat
k: Fin m.+1
e: Fin n <~> Fin m
l: Fin m.+1
f: Fin n <~> Fin m
p: fin_equiv' n m (k, e) == fin_equiv' n m (l, f)
e == f
      refine (fin_equiv_inj_snd n m k l e f p).
Defined.

Definition equiv_fin_equiv `{Funext} (n m : nat)
  : ((Fin m.+1) * (Fin n <~> Fin m)) <~> (Fin n.+1 <~> Fin m.+1)
  := Build_Equiv _ _ (fin_equiv' n m) _.

(** In particular, this implies that if two canonical finite sets are equivalent, then their cardinalities are equal. *)
Definition nat_eq_fin_equiv (n m : nat)
: (Fin n <~> Fin m) -> (n = m).
n, m: nat
Fin n <~> Fin m -> n = m
Proof.
n, m: nat
Fin n <~> Fin m -> n = m
  revert m; simple_induction n n IHn; intro m; simple_induction m m IHm; intros e.
e: Fin 0 <~> Fin 0
0 = 0
m: nat
IHm: Fin 0 <~> Fin m -> 0 = m
e: Fin 0 <~> Fin m.+1
0 = m.+1
n: nat
IHn: forall m : nat, Fin n <~> Fin m -> n = m
e: Fin n.+1 <~> Fin 0
n.+1 = 0
n: nat
IHn: forall m : nat, Fin n <~> Fin m -> n = m
m: nat
IHm: Fin n.+1 <~> Fin m -> n.+1 = m
e: Fin n.+1 <~> Fin m.+1
n.+1 = m.+1
  -
e: Fin 0 <~> Fin 0
0 = 0 exact idpath.
  -
m: nat
IHm: Fin 0 <~> Fin m -> 0 = m
e: Fin 0 <~> Fin m.+1
0 = m.+1 elim (e^-1 (inr tt)).
  -
n: nat
IHn: forall m : nat, Fin n <~> Fin m -> n = m
e: Fin n.+1 <~> Fin 0
n.+1 = 0 elim (e (inr tt)).
  -
n: nat
IHn: forall m : nat, Fin n <~> Fin m -> n = m
m: nat
IHm: Fin n.+1 <~> Fin m -> n.+1 = m
e: Fin n.+1 <~> Fin m.+1
n.+1 = m.+1 refine (ap S (IHn m _)).
n: nat
IHn: forall m : nat, Fin n <~> Fin m -> n = m
m: nat
IHm: Fin n.+1 <~> Fin m -> n.+1 = m
e: Fin n.+1 <~> Fin m.+1
Fin n <~> Fin m
    exact (snd (fin_equiv_inv n m e)).
Defined.

(** ** Initial segments of [nat] *)

Definition nat_fin (n : nat) (k : Fin n) : nat.
n: nat
k: Fin n
nat
Proof.
n: nat
k: Fin n
nat
  simple_induction n n nf; intro k.
k: Fin 0
nat
n: nat
nf: Fin n -> nat
k: Fin n.+1
nat
  -
k: Fin 0
nat contradiction.
  -
n: nat
nf: Fin n -> nat
k: Fin n.+1
nat destruct k as [k|_].
n: nat
nf: Fin n -> nat
k: Fin n
nat
n: nat
nf: Fin n -> nat
nat
    +
n: nat
nf: Fin n -> nat
k: Fin n
nat exact (nf k).
    +
n: nat
nf: Fin n -> nat
nat exact n.
Defined.

Definition nat_fin_inl (n : nat) (k : Fin n)
  : nat_fin n.+1 (inl k) = nat_fin n k
  := 1.

Definition nat_fin_compl (n : nat) (k : Fin n) : nat.
n: nat
k: Fin n
nat
Proof.
n: nat
k: Fin n
nat
  simple_induction n n nfc; intro k.
k: Fin 0
nat
n: nat
nfc: Fin n -> nat
k: Fin n.+1
nat
  -
k: Fin 0
nat contradiction.
  -
n: nat
nfc: Fin n -> nat
k: Fin n.+1
nat destruct k as [k|_].
n: nat
nfc: Fin n -> nat
k: Fin n
nat
n: nat
nfc: Fin n -> nat
nat
    +
n: nat
nfc: Fin n -> nat
k: Fin n
nat exact (nfc k).+1.
    +
n: nat
nfc: Fin n -> nat
nat exact 0.
Defined.

Definition nat_fin_compl_compl n k
  : (nat_fin n k + nat_fin_compl n k).+1 = n.
n: nat
k: Fin n
(nat_fin n k + nat_fin_compl n k).+1 = n
Proof.
n: nat
k: Fin n
(nat_fin n k + nat_fin_compl n k).+1 = n
  simple_induction n n IHn; intro k.
k: Fin 0
(nat_fin 0 k + nat_fin_compl 0 k).+1 = 0
n: nat
IHn: forall k : Fin n, (nat_fin n k + nat_fin_compl n k).+1 = n
k: Fin n.+1
(nat_fin n.+1 k + nat_fin_compl n.+1 k).+1 = n.+1
  -
k: Fin 0
(nat_fin 0 k + nat_fin_compl 0 k).+1 = 0 contradiction.
  -
n: nat
IHn: forall k : Fin n, (nat_fin n k + nat_fin_compl n k).+1 = n
k: Fin n.+1
(nat_fin n.+1 k + nat_fin_compl n.+1 k).+1 = n.+1 destruct k as [k|?]; simpl.
n: nat
IHn: forall k : Fin n, (nat_fin n k + nat_fin_compl n k).+1 = n
k: Fin n
(nat_fin n k + (nat_fin_compl n k).+1).+1 = n.+1
n: nat
IHn: forall k : Fin n, (nat_fin n k + nat_fin_compl n k).+1 = n
u: Unit
(n + 0).+1 = n.+1
    +
n: nat
IHn: forall k : Fin n, (nat_fin n k + nat_fin_compl n k).+1 = n
k: Fin n
(nat_fin n k + (nat_fin_compl n k).+1).+1 = n.+1 rewrite nat_add_comm.
n: nat
IHn: forall k : Fin n, (nat_fin n k + nat_fin_compl n k).+1 = n
k: Fin n
((nat_fin_compl n k).+1 + nat_fin n k).+1 = n.+1
      specialize (IHn k).
n: nat
k: Fin n
IHn: (nat_fin n k + nat_fin_compl n k).+1 = n
((nat_fin_compl n k).+1 + nat_fin n k).+1 = n.+1
      rewrite nat_add_comm in IHn.
n: nat
k: Fin n
IHn: (nat_fin_compl n k + nat_fin n k).+1 = n
((nat_fin_compl n k).+1 + nat_fin n k).+1 = n.+1
      exact (ap S IHn).
    +
n: nat
IHn: forall k : Fin n, (nat_fin n k + nat_fin_compl n k).+1 = n
u: Unit
(n + 0).+1 = n.+1 rewrite nat_add_comm; reflexivity.
Qed.

(** [fsucc_mod] is the successor function mod n *)
Definition fsucc_mod@{} {n : nat} : Fin n -> Fin n.
n: nat
Fin n -> Fin n
Proof.
n: nat
Fin n -> Fin n
  destruct n.
Fin 0 -> Fin 0
n: nat
Fin n.+1 -> Fin n.+1
  1: exact idmap.
n: nat
Fin n.+1 -> Fin n.+1
  intros [x|].
n: nat
x: Fin n
Fin n.+1
n: nat
u: Unit
Fin n.+1
  -
n: nat
x: Fin n
Fin n.+1 exact (fsucc x).
  -
n: nat
u: Unit
Fin n.+1 exact fin_zero.
Defined.

(** fsucc allows us to convert a natural number into an element of a finite set. This can be thought of as the modulo map. *)
Fixpoint fin_nat {n : nat} (m : nat) : Fin n.+1
  := match m with
      | 0 => fin_zero
      | S m => fsucc_mod (fin_nat m)
     end.

(** The 1-dimensional version of Sperner's lemma says that given any finite sequence of decidable hProps, where the sequence starts with true and ends with false, we can find a point in the sequence where the sequence changes from true to false. This is like a discrete intermediate value theorem. *)
Fixpoint sperners_lemma_1d {n} :
  forall (f : Fin (n.+2) -> Type)
         {dprop : forall i, Decidable (f i)}
         (left_true : f fin_zero)
         (right_false : ~ f fin_last),
    {k : Fin n.+1 & f (fin_incl k) /\ ~ f (fsucc k)}.
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
forall f : Fin n.+2 -> Type,
(forall i : Fin n.+2, Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 & (f (fin_incl k) * ~ f (fsucc k))%type}
Proof.
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
forall f : Fin n.+2 -> Type,
(forall i : Fin n.+2, Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 & (f (fin_incl k) * ~ f (fsucc k))%type}
  intros ???.
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+2 -> Type
dprop: forall i : Fin n.+2, Decidable (f i)
left_true: f fin_zero
~ f fin_last ->
{k : Fin n.+1 & (f (fin_incl k) * ~ f (fsucc k))%type}
  destruct n as [|n].
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
f: Fin 2 -> Type
dprop: forall i : Fin 2, Decidable (f i)
left_true: f fin_zero
~ f fin_last ->
{k : Fin 1 & (f (fin_incl k) * ~ f (fsucc k))%type}
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+3 -> Type
dprop: forall i : Fin n.+3, Decidable (f i)
left_true: f fin_zero
~ f fin_last ->
{k : Fin n.+2 & (f (fin_incl k) * ~ f (fsucc k))%type}
  -
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
f: Fin 2 -> Type
dprop: forall i : Fin 2, Decidable (f i)
left_true: f fin_zero
~ f fin_last ->
{k : Fin 1 & (f (fin_incl k) * ~ f (fsucc k))%type} exists fin_zero.
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
f: Fin 2 -> Type
dprop: forall i : Fin 2, Decidable (f i)
left_true: f fin_zero
right_false: ~ f fin_last
(f (fin_incl fin_zero) * ~ f (fsucc fin_zero))%type split; assumption.
  -
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+3 -> Type
dprop: forall i : Fin n.+3, Decidable (f i)
left_true: f fin_zero
~ f fin_last ->
{k : Fin n.+2 & (f (fin_incl k) * ~ f (fsucc k))%type} destruct (dec (f (fin_incl fin_last))) as [prev_true|prev_false].
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+3 -> Type
dprop: forall i : Fin n.+3, Decidable (f i)
left_true: f fin_zero
prev_true: f (fin_incl fin_last)
~ f fin_last ->
{k : Fin n.+2 & (f (fin_incl k) * ~ f (fsucc k))%type}
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+3 -> Type
dprop: forall i : Fin n.+3, Decidable (f i)
left_true: f fin_zero
prev_false: ~ f (fin_incl fin_last)
~ f fin_last ->
{k : Fin n.+2 & (f (fin_incl k) * ~ f (fsucc k))%type}
    +
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+3 -> Type
dprop: forall i : Fin n.+3, Decidable (f i)
left_true: f fin_zero
prev_true: f (fin_incl fin_last)
~ f fin_last ->
{k : Fin n.+2 & (f (fin_incl k) * ~ f (fsucc k))%type} exists fin_last.
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+3 -> Type
dprop: forall i : Fin n.+3, Decidable (f i)
left_true: f fin_zero
prev_true: f (fin_incl fin_last)
right_false: ~ f fin_last
(f (fin_incl fin_last) * ~ f (fsucc fin_last))%type split; assumption.
    +
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+3 -> Type
dprop: forall i : Fin n.+3, Decidable (f i)
left_true: f fin_zero
prev_false: ~ f (fin_incl fin_last)
~ f fin_last ->
{k : Fin n.+2 & (f (fin_incl k) * ~ f (fsucc k))%type} destruct (sperners_lemma_1d _ (f o fin_incl) _ left_true prev_false) as [k' [fleft fright]].
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+3 -> Type
dprop: forall i : Fin n.+3, Decidable (f i)
left_true: f fin_zero
prev_false: ~ f (fin_incl fin_last)
k': Fin n.+1
fleft: f (fin_incl (fin_incl k'))
fright: ~ f (fin_incl (fsucc k'))
~ f fin_last ->
{k : Fin n.+2 & (f (fin_incl k) * ~ f (fsucc k))%type}
      exists (fin_incl k').
sperners_lemma_1d: forall (n : nat)
(f : Fin n.+2 -> Type),
(forall i : Fin n.+2,
 Decidable (f i)) ->
f fin_zero ->
~ f fin_last ->
{k : Fin n.+1 &
(f (fin_incl k) * ~ f (fsucc k))%type}
n: nat
f: Fin n.+3 -> Type
dprop: forall i : Fin n.+3, Decidable (f i)
left_true: f fin_zero
prev_false: ~ f (fin_incl fin_last)
k': Fin n.+1
fleft: f (fin_incl (fin_incl k'))
fright: ~ f (fin_incl (fsucc k'))
right_false: ~ f fin_last
(f (fin_incl (fin_incl k')) *
 ~ f (fsucc (fin_incl k')))%type
      split; assumption.
Defined.