Y Z W : baut_bool_pairing_ZZ_Z_symm_map Y Z W o baut_bool_pairing_ZZ_Z_symm_map Z Y W == idmap. Proof. intros e. apply path_equiv, path_arrow; intros z. apply path_equiv, path_arrow; intros y. reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness. Require Import Universes.BAut. Require Import Pointed.Core.