Definition cone_functor {I C:category} : [I,C] ⟶ [C^op,SET]. Proof. intros. unshelve refine (_,,_). { unshelve refine (_,,_). { intros D. unshelve refine (_,,_). { unshelve refine (_,,_). - intro c. exists (cone (C:=C) c D). abstract ( apply isaset_total2; [ apply impred_isaset; intro i; apply homset_property | intros φ; apply impred_isaset; intro i; apply impred_isaset; intro j; apply impred_isaset; intro e; apply isasetaprop; apply homset_property]) using LLL. - simpl; intros a b f φ. exists (λ i, pr1 φ i ∘ f). abstract ( intros i j e; simpl; rewrite <- assoc; apply maponpaths; apply (pr2 φ)) using _M_. } { abstract (split; [ intro c; simpl; apply funextsec; intro p; apply cone_eq; intro i; simpl; apply id_left | intros a b c f g; simpl; apply funextsec; intro p; apply cone_eq; simpl; intro i; apply pathsinv0, assoc ]) using _N_. } } { intros D D' f; simpl. unshelve refine (_,,_). - simpl. unfold cone. intros c φ. unshelve refine (_,,_). + intros i. exact (pr1 f i ∘ pr1 φ i). + abstract ( simpl; intros i j e; assert (L := pr2 φ i j e); simpl in L; rewrite <- L; rewrite <- assoc; rewrite <- assoc; apply maponpaths; apply pathsinv0; apply nat_trans_ax) using _P_. - abstract (intros a b g; simpl; apply funextsec; intro p; apply cone_eq; intro i; simpl; apply pathsinv0, assoc) using _Q_. } } { abstract (split; [ intros D; simpl; apply nat_trans_eq; [ exact (homset_property SET) | intros c; apply funextsec; intro φ; simpl; apply cone_eq; intro i; apply id_right] | intros D D' D'' p q; apply nat_trans_eq; [ apply homset_property | intro c; apply funextsec; intro K; apply cone_eq; intros i; apply assoc ]]). } Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.