proposition: Lemma has_limits_over_finverse_invariance : forall a b c, Category.axioms a -> Category.axioms b -> Category.axioms c -> has_limits_over c a -> (exists f, (exists g, (are_finverse f g & source f = a & target f = b))) -> has_limits_over c b.
proof: Proof. ir. nin H3. nin H3. ee. uhg; ee. ir. uhg; ee. set (k:= fcompose x0 f). uh H3; ee. assert (Functor.axioms k). uf k. ap fcompose_axioms. am. am. rw H11. rw H5. sy; am. assert (source k = c). uf k. rw source_fcompose. am. assert (target k = a). uf k. rw target_fcompose. wr H10. am. assert (fcompose x k = f). uf k. wr fcompose_assoc. rw H12. rw left_fidentity. tv. am. rw H11. rw H5. sy; am. am. am. am. am. rw H11. rw H5. sy; am. uh H2; ee. util (H2 k). am. am. am. uh H18. nin H18. uh H18. ee. sh (cone_pushdown x x1). uhg; ee. apply are_finverse_preserves_limits with x0. am. uhg; ee; am. uf cone_target. rw H19. rw H16. am. rw socle_cone_pushdown. rw H19. am. Qed.
imports: Arith nat_trans