Definition dialgebra_to_slice_adj_equiv : adj_equivalence_of_cats dialgebra_to_slice. Proof. simple refine ((_ ,, ((_ ,, _) ,, _ ,, _)) ,, _ ,, _). - exact slice_to_dialgebra. - exact dialgebra_to_slice_unit. - exact dialgebra_to_slice_counit. - abstract (intros f ; use subtypePath ; [ intro ; apply homset_property | ] ; cbn ; apply id_left). - abstract (intros f ; use subtypePath ; [ intro ; apply homset_property | ] ; cbn ; apply id_left). - intro f. use is_z_iso_dialgebra. cbn. apply is_z_isomorphism_identity. - intro f. use z_iso_to_slice_precat_z_iso. cbn. apply is_z_isomorphism_identity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.DialgebraEnriched. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Terminal. Import MonoidalNotations.