Definition const_bool (t : unit) : UU := bool.
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.