(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Categories.
Require Export Parts.
(** Title "Sub-category." *)
Section Subcategory_def.
Variable C : category.
Variable C' : Type.
Variable i : C' -> C.
Variable homC' : forall a b : C', subtype_image (Hom (i a) (i b)).

Definition subcat_Hom (a b : C') := homC' a b:Setoid.
Variable
  CompC' :
    forall a b c : C', subcat_Hom b c -> subcat_Hom a b -> subcat_Hom a c.
Variable idC' : forall a : C', subcat_Hom a a.
Hypothesis
  idC'ok : forall a : C', Equal (subtype_image_inj (idC' a)) (Hom_id (i a)).
Hypothesis
  CompC'_ok :
    forall (a b c : C') (g : subcat_Hom b c) (f : subcat_Hom a b),
    Equal (subtype_image_inj (CompC' g f))
      (comp_hom (subtype_image_inj g) (subtype_image_inj f)).

Definition subcat_Hom_comp :
  forall a b c : C',
  MAP (cart (subcat_Hom b c) (subcat_Hom a b)) (subcat_Hom a c).
(* Goal: forall a b c : C', Carrier (MAP (cart (subcat_Hom b c) (subcat_Hom a b)) (subcat_Hom a c)) *)
intros a b c; try assumption.
apply
 (Build_Map (A:=cart (subcat_Hom b c) (subcat_Hom a b)) (B:=
    subcat_Hom a c)
    (Ap:=fun x : cart (subcat_Hom b c) (subcat_Hom a b) =>
         CompC' (proj1 x) (proj2 x))).
(* Goal: @Hom_comp_unit_r C' subcat_Hom subcat_Hom_comp idC' *)
red in |- *.
(* Goal: forall (x y : Carrier (cart (subcat_Hom b c) (subcat_Hom a b))) (_ : @Equal (cart (subcat_Hom b c) (subcat_Hom a b)) x y), @Equal (subcat_Hom a c) (@CompC' a b c (@proj1 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x)) (@CompC' a b c (@proj1 (subcat_Hom b c) (subcat_Hom a b) y) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y)) *)
intros x y H'; try assumption.
(* Goal: forall (a b : C') (f : Carrier (subcat_Hom a b)), @Equal (subcat_Hom a b) (@Ap (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (@Build_Map (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (fun x : Carrier (cart (subcat_Hom a b) (subcat_Hom a a)) => @CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (fun (x y : Carrier (cart (subcat_Hom a b) (subcat_Hom a a))) (H' : @Equal (cart (subcat_Hom a b) (subcat_Hom a a)) x y) => @Trans (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@CompC'_ok a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (@Trans (@Hom C (i a) (i b)) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@comp_hom_compatible C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y)) (@proj1_comp (subcat_Hom a b) (subcat_Hom a a) x y H') (@proj2_comp (subcat_Hom a b) (subcat_Hom a a) x y H')) (@Sym (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@CompC'_ok a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y)))))) (@couple (subcat_Hom a b) (subcat_Hom a a) f (idC' a))) f *)
simpl in |- *.
(* Goal: forall (a b : C') (f : @subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)), @subtype_image_equal (@Hom C (i a) (i b)) (@subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b)) (@CompC' a a b f (idC' a)) f *)
unfold subtype_image_equal in |- *.
apply
 Trans
  with (comp_hom (subtype_image_inj (proj1 x)) (subtype_image_inj (proj2 x)));
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
 auto with algebra.
apply
 Trans
  with (comp_hom (subtype_image_inj (proj1 y)) (subtype_image_inj (proj2 y)));
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
 auto with algebra.
(* Goal: @Equal (@Hom C (i a) (i c)) (@comp_hom C (i a) (i b) (i c) (@subtype_image_inj (@Hom C (i b) (i c)) (homC' b c) (@proj1 (subcat_Hom b c) (subcat_Hom a b) x)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x))) (@comp_hom C (i a) (i b) (i c) (@subtype_image_inj (@Hom C (i b) (i c)) (homC' b c) (@proj1 (subcat_Hom b c) (subcat_Hom a b) y)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y))) *)
apply comp_hom_compatible.
(* Goal: @Equal (@Hom C (i b) (i c)) (@subtype_image_inj (@Hom C (i b) (i c)) (homC' b c) (@proj1 (subcat_Hom b c) (subcat_Hom a b) x)) (@subtype_image_inj (@Hom C (i b) (i c)) (homC' b c) (@proj1 (subcat_Hom b c) (subcat_Hom a b) y)) *)
(* Goal: @Equal (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y)) *)
cut (Equal (proj1 x) (proj1 y)).
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
auto with algebra.
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
auto with algebra.
(* Goal: @Equal (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y)) *)
cut (Equal (proj2 x) (proj2 y)).
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
auto with algebra.
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
auto with algebra.
Defined.

Definition subcat : category.
apply
 (Build_category (Ob:=C') (Hom:=subcat_Hom) (Hom_comp:=subcat_Hom_comp)
    (Hom_id:=idC')).
(* Goal: @Hom_comp_unit_r C' subcat_Hom subcat_Hom_comp idC' *)
red in |- *.
(* Goal: forall (a b : C') (f : Carrier (subcat_Hom a b)), @Equal (subcat_Hom a b) (@Ap (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (subcat_Hom_comp a a b) (@couple (subcat_Hom a b) (subcat_Hom a a) f (idC' a))) f *)
unfold subcat_Hom_comp in |- *.
(* Goal: forall (a b : C') (f : Carrier (subcat_Hom a b)), @Equal (subcat_Hom a b) (@Ap (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (@Build_Map (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (fun x : Carrier (cart (subcat_Hom a b) (subcat_Hom a a)) => @CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (fun (x y : Carrier (cart (subcat_Hom a b) (subcat_Hom a a))) (H' : @Equal (cart (subcat_Hom a b) (subcat_Hom a a)) x y) => @Trans (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@CompC'_ok a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (@Trans (@Hom C (i a) (i b)) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@comp_hom_compatible C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y)) (@proj1_comp (subcat_Hom a b) (subcat_Hom a a) x y H') (@proj2_comp (subcat_Hom a b) (subcat_Hom a a) x y H')) (@Sym (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@CompC'_ok a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y)))))) (@couple (subcat_Hom a b) (subcat_Hom a a) f (idC' a))) f *)
simpl in |- *.
(* Goal: forall (a b : C') (f : @subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)), @subtype_image_equal (@Hom C (i a) (i b)) (@subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b)) (@CompC' a a b f (idC' a)) f *)
unfold subtype_image_equal in |- *.
(* Goal: forall (a b c d : C') (f : @subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)) (g : @subtype_image_carrier (@Hom C (i b) (i c)) (homC' b c)) (h : @subtype_image_carrier (@Hom C (i c) (i d)) (homC' c d)), @Equal (@Hom C (i a) (i d)) (@subtype_image_inj (@Hom C (i a) (i d)) (homC' a d) (@CompC' a b d (@CompC' b c d h g) f)) (@subtype_image_inj (@Hom C (i a) (i d)) (homC' a d) (@CompC' a c d h (@CompC' a b c g f))) *)
(* Goal: @Hom_comp_unit_l C' subcat_Hom subcat_Hom_comp idC' *)
(* Goal: @Hom_comp_unit_r C' subcat_Hom subcat_Hom_comp idC' *)
intros a b c d f g h; try assumption.
apply
 Trans with (comp_hom (subtype_image_inj (CompC' h g)) (subtype_image_inj f));
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
 auto with algebra.
apply
 Trans
  with
    (comp_hom (comp_hom (subtype_image_inj h) (subtype_image_inj g))
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
       (subtype_image_inj f)); auto with algebra.
apply
 Trans with (comp_hom (subtype_image_inj h) (subtype_image_inj (CompC' g f)));
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
 auto with algebra.
apply
 Trans
  with
    (comp_hom (subtype_image_inj h)
       (comp_hom (subtype_image_inj g) (subtype_image_inj f)));
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
 auto with algebra.
(* Goal: @Hom_comp_unit_r C' subcat_Hom subcat_Hom_comp idC' *)
red in |- *.
(* Goal: forall (a b : C') (f : Carrier (subcat_Hom a b)), @Equal (subcat_Hom a b) (@Ap (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (subcat_Hom_comp a a b) (@couple (subcat_Hom a b) (subcat_Hom a a) f (idC' a))) f *)
unfold subcat_Hom_comp in |- *.
(* Goal: forall (a b : C') (f : Carrier (subcat_Hom a b)), @Equal (subcat_Hom a b) (@Ap (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (@Build_Map (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (fun x : Carrier (cart (subcat_Hom a b) (subcat_Hom a a)) => @CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (fun (x y : Carrier (cart (subcat_Hom a b) (subcat_Hom a a))) (H' : @Equal (cart (subcat_Hom a b) (subcat_Hom a a)) x y) => @Trans (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@CompC'_ok a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (@Trans (@Hom C (i a) (i b)) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@comp_hom_compatible C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y)) (@proj1_comp (subcat_Hom a b) (subcat_Hom a a) x y H') (@proj2_comp (subcat_Hom a b) (subcat_Hom a a) x y H')) (@Sym (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@CompC'_ok a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y)))))) (@couple (subcat_Hom a b) (subcat_Hom a a) f (idC' a))) f *)
simpl in |- *.
(* Goal: forall (a b : C') (f : @subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)), @subtype_image_equal (@Hom C (i a) (i b)) (@subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b)) (@CompC' a a b f (idC' a)) f *)
unfold subtype_image_equal in |- *.
(* Goal: forall (a b : C') (f : @subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)), @Equal (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b f (idC' a))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) f) *)
intros a b f; try assumption.
apply
 Trans with (comp_hom (subtype_image_inj (idC' b)) (subtype_image_inj f));
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
 auto with algebra.
apply Trans with (comp_hom (Hom_id (i b)) (subtype_image_inj f));
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
 auto with algebra.
(* Goal: @Hom_comp_unit_r C' subcat_Hom subcat_Hom_comp idC' *)
red in |- *.
(* Goal: forall (a b : C') (f : Carrier (subcat_Hom a b)), @Equal (subcat_Hom a b) (@Ap (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (subcat_Hom_comp a a b) (@couple (subcat_Hom a b) (subcat_Hom a a) f (idC' a))) f *)
unfold subcat_Hom_comp in |- *.
(* Goal: forall (a b : C') (f : Carrier (subcat_Hom a b)), @Equal (subcat_Hom a b) (@Ap (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (@Build_Map (cart (subcat_Hom a b) (subcat_Hom a a)) (subcat_Hom a b) (fun x : Carrier (cart (subcat_Hom a b) (subcat_Hom a a)) => @CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (fun (x y : Carrier (cart (subcat_Hom a b) (subcat_Hom a a))) (H' : @Equal (cart (subcat_Hom a b) (subcat_Hom a a)) x y) => @Trans (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@CompC'_ok a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) x) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (@Trans (@Hom C (i a) (i b)) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@comp_hom_compatible C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) x)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y)) (@proj1_comp (subcat_Hom a b) (subcat_Hom a a) x y H') (@proj2_comp (subcat_Hom a b) (subcat_Hom a a) x y H')) (@Sym (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@comp_hom C (i a) (i a) (i b) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@proj1 (subcat_Hom a b) (subcat_Hom a a) y)) (@subtype_image_inj (@Hom C (i a) (i a)) (homC' a a) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y))) (@CompC'_ok a a b (@proj1 (subcat_Hom a b) (subcat_Hom a a) y) (@proj2 (subcat_Hom a b) (subcat_Hom a a) y)))))) (@couple (subcat_Hom a b) (subcat_Hom a a) f (idC' a))) f *)
simpl in |- *.
(* Goal: forall (a b : C') (f : @subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)), @subtype_image_equal (@Hom C (i a) (i b)) (@subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b)) (@CompC' a a b f (idC' a)) f *)
unfold subtype_image_equal in |- *.
(* Goal: forall (a b : C') (f : @subtype_image_carrier (@Hom C (i a) (i b)) (homC' a b)), @Equal (@Hom C (i a) (i b)) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) (@CompC' a a b f (idC' a))) (@subtype_image_inj (@Hom C (i a) (i b)) (homC' a b) f) *)
intros a b f; try assumption.
apply
 Trans with (comp_hom (subtype_image_inj f) (subtype_image_inj (idC' a)));
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
 auto with algebra.
apply Trans with (comp_hom (subtype_image_inj f) (Hom_id (i a)));
(* Goal: @Equal (subcat_Hom a b) (@proj2 (subcat_Hom b c) (subcat_Hom a b) x) (@proj2 (subcat_Hom b c) (subcat_Hom a b) y) *)
 auto with algebra.
Defined.
End Subcategory_def.