Require cat_.
Require fibprod_.

Implicit Arguments On.

Module Target_.

Export Cat_.

Section Target.

Variable A:Cat; u:A.

Definition Target : Type := (x:A; f:(mor x u)) Prop.

Record Target_Set [a:Target] : Type := target_intro {
  target_src : A;
  target_mor :> (mor target_src u);
  target_prop : (a target_src target_mor)
 }.

Coercion Target_Set : Target >-> SORTCLASS.

Definition is_maximal_target [a:Target] : Prop :=
 (x:A; f:(mor x u)) (a ? f).

End Target.

Hints Unfold is_maximal_target.

Section Target_Transport.

Variable A:Cat; u,v:A; f:(mor u v); a:(Target v).

Definition target_transport : (Target u) :=
 [x:A; g:(mor x u)] (a (oo f g)).

End Target_Transport.

Section Target_Eq.

Variable A:Cat; u:A.

Definition target_sub [a,b:(Target u)] : Prop :=
 (x:A; f:(mor x u); Hf:(a ? f)) (b ? f).

Lemma target_extens : (a,b:(Target u))
 (target_sub a b) -> (target_sub b a) -> a==b.
Proof.
  Hints Resolve prop_uni.
  Unfold target_sub; Intros.
  Apply extensionality with T:=[x:A](f:(mor x u))Prop.
  Auto.
Qed.

End Target_Eq.

Lemma target_transport_trans :
 (A:Cat; u,v,w:A; g:(mor v w); f:(mor u v); a:(Target w))
 (target_transport (oo g f) a)==(target_transport f (target_transport g a)).
Proof.
  Intros; Apply target_extens;
    Unfold target_sub target_transport; Intros; Simpl.
  Rewrite oo_assoc; Auto.
  Rewrite <- oo_assoc; Auto.
Qed.
Hints Resolve target_transport_trans.

Section Target_Composition.

Variable A:Cat; u:A; a:(Target u).
Variable b:(x:A; f:(mor x u); Hf:(a f))(Target x).

Inductive target_comp : (Target u) :=
 | target_comp_intro : (x:A; f:(mor x u); Hf:(a f))
    (y:A; g:(mor y x); Hg:((b Hf) y g))
    (target_comp (oo f g)).

End Target_Composition.

Section Target_Of_Mor.

Variable A:Cat; x,y:A; f:(mor x y).

Inductive target_of_mor : (Target y) :=
 | target_of_mor_intro : (target_of_mor f).

End Target_Of_Mor.

Export Fibprod_.

Section Pullback_Target.

Variable A:Cat; pb:(has_fibprod A).
Variable u:A; a:(Target u); v:A; h:(mor v u).

Inductive pullback_target : (Target v) :=
 | pullback_target_intro :
    (f:a)(pullback_target (fct (base u) (pullback (pb h f)))).

End Pullback_Target.