Fibered Products |
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.
End
Fibprod.