Require cat_over_.
Require product_.

Implicit Arguments On.

Module Fibprod_.

Export Cat_.
Export Cat_Over_.
Export Product_.

Section Fibprod.

Variable A:Cat.

Definition Fibprod [x,y,s:A; hx:(mor x s); hy:(mor y s)] : Type :=
 (Product (make_over hx) (make_over hy)).

Definition has_fibprod : Type := (x,y,s:A; hx:(mor x s); hy:(mor y s))
 (Fibprod hx hy).

End Fibprod.

Section Pullback.

Variable A:Cat; x,y,s:A; hx:(mor x s); hy:(mor y s).
Variable u:(Fibprod hx hy).

Definition pullback : (mor u (make_over hx)) := (proj1 u).

Definition pullback_mor : (mor u (make_over hy)) := (proj2 u).

Lemma pullback_eq :
 (oo hx (fct (base s) pullback))==(oo hy (fct (base s) pullback_mor)).
Proof.
  NewDestruct pullback.
  NewDestruct pullback_mor.
  Simpl in f e f0 e0.
  Simpl.
  Transitivity (fct (base s) (final (final_over s) u));
    NewDestruct u; NewDestruct product_obj0; Auto.
Qed.

End Pullback.

Section Base_Change.

Variable A:Cat; x,y,s:A; hx:(mor x s); hy:(mor y s).
Variable u:(Fibprod hx hy).

Definition base_change : (cat_over x).
Proof.
  Split with (base s u).
  Exact (fct (base s) (proj1 u)).
Defined.

End Base_Change.