proposition: Lemma FT_tau_cone_law : Cone_law (F:=(FT_E o_F FT_Q) o_F G) FT_tau_i.
proof: Proof. unfold Cone_law in |- *; simpl in |- *; unfold FT_tau_i, FMor in |- *; simpl in |- *. intros i j h. elim h; intros g H; exact H. Qed.
imports: FSC_inc Comma_proj FAFT_SSC2 Th_Adjoint Pres_Limits Pullbacks1