equiv_composeR' {A B C} (f : A <~> B) (g : B <~> C) := equiv_compose' g f. Ltac equiv_via mid := apply @equiv_composeR' with (B := mid). Ltac ev_equiv := repeat match goal with | [ |- context[equiv_fun (equiv_inverse (equiv_inverse ?f))] ] => change (equiv_fun (equiv_inverse (equiv_inverse f))) with (equiv_fun f) | [ |- context[(@equiv_inv ?B ?A (equiv_fun (equiv_inverse ?f)) ?iseq)] ] => change (@equiv_inv B A (equiv_fun (equiv_inverse f)) iseq) with (equiv_fun f) | [ |- context[((equiv_fun ?f)^-1)^-1] ] => change ((equiv_fun f)^-1)^-1 with (equiv_fun f) | [ |- context[equiv_fun (equiv_compose' ?g ?f) ?a] ] => change (equiv_fun (equiv_compose' g f) a) with (g (f a)) | [ |- context[equiv_fun (equiv_compose ?g ?f) ?a] ] => change (equiv_fun (equiv_compose g f) a) with (g (f a)) | [ |- context[equiv_fun (equiv_inverse ?f) ?a] ] => change (equiv_fun (equiv_inverse f) a) with (f^-1 a) | [ |- context[equiv_fun (equiv_compose' ?g ?f)] ] => change (equiv_fun (equiv_compose' g f)) with (g o f) | [ |- context[equiv_fun (equiv_compose ?g ?f)] ] => change (equiv_fun (equiv_compose g f)) with (g o f) | [ |- context[equiv_fun (equiv_inverse ?f)] ] => change (equiv_fun (equiv_inverse f)) with (f^-1) end. Ltac decomposing_intros := let x := fresh in intros x; hnf in x; cbn in x; try lazymatch type of x with | ?a = ?b => idtac | forall y:?A, ?B => idtac | Contr ?A => revert x; match goal with |- (forall y, ?P y) => snrefine (Contr_ind A P _) end | _ => elim x; clear x end; try decomposing_intros. Ltac multi_assumption := multimatch goal with [ H : ?A |- _ ] => exact H end. Ltac build_record := cbn; multi_assumption + (unshelve econstructor; build_record). Ltac make_equiv := snrefine (equiv_adjointify _ _ _ _); [ decomposing_intros; build_record | decomposing_intros; build_record | decomposing_intros; exact idpath | decomposing_intros; exact idpath ]. Ltac make_equiv_without_adjointification := snrefine (Build_Equiv _ _ _ _); [ decomposing_intros; build_record | snrefine (Build_IsEquiv _ _ _ _ _ _ _); [ decomposing_intros; build_record | decomposing_intros; exact idpath | decomposing_intros; exact idpath | decomposing_intros; exact idpath ] ]. snrefine (equiv_adjointify _ _ _ _). - intros x; cbn in x. elim x; clear x. intros x; cbn in x. elim x; clear x. intros a; cbn in a. intros b; cbn in b. intros x; cbn in x. elim x; clear x. intros c; cbn in c. intros d; cbn in d. cbn; unshelve econstructor. { cbn; exact a. } { cbn; unshelve econstructor. { cbn; unshelve econstructor. { cbn; exact b. } { cbn; exact c. } } { cbn; exact d. } } - intros x; cbn in x. elim x; clear x. intros a; cbn in a. intros x; cbn in x. elim x; clear x. intros x; cbn in x. elim x; clear x. intros b; cbn in b. intros c; cbn in c. intros d; cbn in d. cbn; unshelve econstructor. { cbn; unshelve econstructor. { cbn; exact a. } { cbn; exact b. } } { cbn; unshelve econstructor. { cbn; exact c. } { cbn; exact d. } } - intros x; cbn in x. elim x; clear x. intros a; cbn in a. intros x; cbn in x. elim x; clear x. intros x; cbn in x. elim x; clear x. intros b; cbn in b. intros c; cbn in c. intros d; cbn in d. cbn; exact idpath. - intros x; cbn in x. elim x; clear x. intros x; cbn in x. elim x; clear x. intros a; cbn in a. intros b; cbn in b. intros x; cbn in x. elim x; clear x. intros c; cbn in c. intros d; cbn in d. cbn; exact idpath. Defined.
Require Import