Definition PullbackCone {C:category} {a b c:C} (f:a-->c) (g:b-->c) : C^op ⟶ SET. Proof. intros. unshelve refine (makeFunctor_op _ _ _ _). - intros t. unshelve refine (_,,_). + exact (∑ (p: t --> a × t --> b), f ∘ pr1 p = g ∘ pr2 p). + abstract (apply isaset_total2; [ apply isasetdirprod; apply homset_property | intro; apply isasetaprop; apply homset_property]) using _L_. - intros t u p w; simpl in *. exists (pr1 (pr1 w) ∘ p,, pr2 (pr1 w) ∘ p). abstract ( simpl; rewrite <- 2? assoc; apply maponpaths; exact (pr2 w)) using _M_. - abstract (intros t; simpl; apply funextsec; intro w; induction w as [w eq]; induction w as [p q]; simpl in *; unshelve refine (two_arg_paths_f _ _); [ rewrite 2? id_left; reflexivity | apply proofirrelevance; apply homset_property]) using _N_. - abstract ( intros r s t p q; simpl in *; apply funextsec; intro w; unshelve refine (total2_paths2_f _ _); [ simpl; rewrite 2? assoc; reflexivity | apply proofirrelevance; apply homset_property]) using _P_. 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.