(e1 e2 : Bool <~> Bool) : e1 o e2 == e2 o e1. Proof. intro b. refine (ap e1 (aut_bool_canonical e2 b) @ _). refine (aut_bool_canonical e1 _ @ _). refine (_ @ ap e2 (aut_bool_canonical e1 b)^). refine (_ @ (aut_bool_canonical e2 _)^). unfold f, g. destruct (e1 true), (e2 true), b; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Equiv.