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 }. Proof. simpl in e. refine (equiv_sigma_prod _ _). recall (e (inr tt)) as y eqn:p. assert (p' := (moveL_equiv_V _ _ p)^). exists y. destruct y as [y|[]]. + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set} (fin_transpose_last_with m (inl y) oE e) _ _ ; _). { intros a. ev_equiv. assert (q : inl y <> e (inl a)) by exact (fun z => inl_ne_inr _ _ (equiv_inj e (z^ @ p^))). set (z := e (inl a)) in *. destruct z as [z|[]]. - rewrite fin_transpose_last_with_rest; try exact tt; try assumption. - rewrite fin_transpose_last_with_last; exact tt. } { intros []. ev_equiv. rewrite p. rewrite fin_transpose_last_with_with; exact tt. } intros x. unfold fst, snd; ev_equiv. simpl. destruct x as [x|[]]; simpl. * rewrite unfunctor_sum_l_beta. apply fin_transpose_last_with_invol. * refine (fin_transpose_last_with_last _ _ @ p^). + simple refine (equiv_unfunctor_sum_l@{Set Set Set Set Set Set} e _ _ ; _). { intros a. destruct (is_inl_or_is_inr (e (inl a))) as [l|r]. - exact l. - assert (q := inr_un_inr (e (inl a)) r). apply moveR_equiv_V in q. assert (s := q^ @ ap (e^-1 o inr) (path_unit _ _) @ p'). elim (inl_ne_inr _ _ s). } { intros []; exact (p^ # tt). } intros x. unfold fst, snd; ev_equiv. simpl. destruct x as [a|[]]. * rewrite fin_transpose_last_with_last_other. apply unfunctor_sum_l_beta. * simpl. rewrite fin_transpose_last_with_last. symmetry; apply p. Qed.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.