Definition const_bool_eq1 : const_bool = const_bool := invweq (weqtoforallpaths _ _ _) (λ _, bool_eq1).
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.NoInjectivePairing. Require Import UniMath.MoreFoundations.PartD. Require Import UniMath.CategoryTheory.Categories.Type.Core. Require Import UniMath.CategoryTheory.Core.Categories.