Lemma fully_faithful_reflects_all_limits (fff : fully_faithful F) : reflects_all_limits. Proof. intros g d L cc isLimConeImL. unfold isLimCone in *. intros L' cc'. unfold fully_faithful in fff. apply (@iscontrweqf (∑ x : D ⟦ F L', F L ⟧, ∏ v : vertex g, x · coneOut (mapcone F d cc) v = coneOut (mapcone F d cc') v)). - apply (@weqcomp _ (∑ x : C ⟦ L', L ⟧, ∏ v : vertex g, # F x · coneOut (mapcone F d cc) v = coneOut (mapcone F d cc') v)). + apply invweq. apply (weqfp (weq_from_fully_faithful fff _ _) (λ f, ∏ v, f · coneOut (mapcone F d cc) v = coneOut (mapcone F d cc') v)). + apply weqfibtototal; intro f. apply weqonsecfibers; intro v. unfold mapcone; cbn. apply invweq. apply fully_faithful_commutative_triangle_weq. assumption. - apply isLimConeImL. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Import UniMath.CategoryTheory.opp_precat.