proposition: Lemma fully_faithful_reflects_all_limits (fff : fully_faithful F) : reflects_all_limits.
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Limits.Graphs.Colimits