Lemma is_precategory_base_precategory_data : is_precategory (base_precategory_data C D). Proof. apply make_is_precategory. - intros F₀ G₀. cbn. intros γ. apply funextsec. intros x. apply id_left. - intros F₀ G₀. cbn. intros γ. apply funextsec. intros x. apply id_right. - intros F₀ G₀ H₀ K₀. cbn. intros γ θ μ. apply funextsec. intros x. apply assoc. - intros F₀ G₀ H₀ K₀. cbn. intros γ θ μ. apply funextsec. intros x. apply assoc'. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.