bug.v

Notation idmap := (fun x => x).

Notation compose := (fun g f x => g (f x)).

Notation "g 'o' f" := (compose g f) (at level 40, left associativity).

Record Equiv A B := BuildEquiv {
  equiv_fun : A -> B ;
  equiv_inv : B -> A
}.

Coercion equiv_fun : Equiv >-> Funclass.

Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.

Notation "f ^-1" := (@equiv_inv _ _ f) (at level 3, format "f '^-1'").

Definition functor_prod {A A' B B' : Type} (f:A->A') (g:B->B')
  : A * B -> A' * B'
  := fun z => (f (fst z), g (snd z)).

Definition equiv_prod_symm (A B : Type) : A * B <~> B * A
  := BuildEquiv
       _ _ (fun ab => (snd ab, fst ab))
          (fun ba => (snd ba, fst ba)).

Definition equiv_prod_assoc (A B C : Type) : A * (B * C) <~> (A * B) * C
  := BuildEquiv
       _ _ (fun abc => ((fst abc, fst (snd abc)), snd (snd abc)))
          (fun abc => (fst (fst abc), (snd (fst abc), snd abc))).

Section NotaSec.
  Notation __ := (_:_ -> _).

  Definition merge_aux A B C D : A * B * (C * D) -> B * C * (A * D).
  Proof.
    refine (__ o (equiv_prod_assoc _ _ _)).
    refine (__ o (functor_prod (equiv_prod_assoc A B C)^-1 idmap)).
    refine (__ o (functor_prod (equiv_prod_symm _ _) idmap)).
    exact ((equiv_prod_assoc _ _ _)^-1).
  Defined.
End NotaSec.