Definition base_precategory_data (C D:precategory_data) : precategory_data := make_precategory_data (base_precategory_ob_mor C D) (λ (F₀ : C → D) (x : C), identity (F₀ x)) (λ (F₀ G₀ H₀ : C → D) (FG : ∏ x : C, D ⟦ F₀ x, G₀ x ⟧) (GH : ∏ x : C, D ⟦ G₀ x, H₀ x ⟧) (x : C), FG x · GH x).
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.