proposition: Lemma fiprod_hypothesis_vee_fimaps : forall c, is_cone c -> cone_source c = vee_cat -> fiprod_hypothesis (cone_target c) (veefirst c) (veesecond c) (fimap1 c) (fimap2 c).
proof: Proof. ir. util (fiprod_hypothesis_fimaps (a:= cone_target c) (u:= veefirst c) (v:= veesecond c) (c:=c)). uf veefirst. uf veesecond. uf cone_target. ap functor_vee_hypothesis. app socle_axioms. am. am. uf cone_target. uf veefirst. uf veesecond. ap functor_vee_eq. app socle_axioms. am. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal