# Library ConCaT.CATEGORY_THEORY.LIMITS.Pullbacks1

Require Export Limit.
Require Export PULB.
Require Export Pullbacks.

Set Implicit Arguments.
Unset Strict Implicit.

Section Fpullback_limit_def.

Variables (C : Category) (G : Functor PULB C).

SubClass Fpullback1 := Limit G.

Variable l : Fpullback1.

Definition Fibred1_prod := Lim l.

Definition Fibred1_p : Fibred1_prod --> G P1 := Limiting_cone l P1.

Definition Fibred1_q : Fibred1_prod --> G P3 := Limiting_cone l P3.

Lemma Prf_pb1_law1 :
Pullback_law1 (FMor G F12) (FMor G F32) Fibred1_p Fibred1_q.
Proof.
unfold Pullback_law1, Pullback_eq1 in |- *.
apply Trans with (Limiting_cone l P2).
apply Sym.
apply (Eq_cone (Limiting_cone l) F12).
apply (Eq_cone (Limiting_cone l) F32).
Qed.

Section pb1_diese_def.

Variables (r : C) (t1 : r --> G P1) (t2 : r --> G P3).

Hypothesis H : Pullback_eq1 (FMor G F12) (FMor G F32) t1 t2.

Definition Pulb_tau (a : PULB) :=
match a as a' return (Carrier (r --> G a')) with
| P1 => t1
| P2 => t1 o FMor G F12
| P3 => t2
end.

Lemma Pulb_cone_law : Cone_law Pulb_tau.
Proof.
unfold Cone_law in |- *; intros x x1 t.
elim t; simpl in |- *; unfold FMor at 1 in |- *; simpl in |- *.
apply Trans with (t1 o Id (G P1)).
apply Idr.
apply Comp_l; apply (FId1 G P1).
apply Trans with ((t1 o FMor G F12) o Id (G P2)).
apply Idr.
apply Comp_l; apply (FId1 G P2).
apply Trans with (t2 o Id (G P3)).
apply Idr.
apply Comp_l; apply (FId1 G P3).
apply Refl.
apply H.
Qed.

Definition Pulb_cone : Cone r G := Pulb_cone_law.

Definition Pb1_diese : r --> Fibred1_prod := Lim_diese l Pulb_cone.

End pb1_diese_def.

Lemma Prf_pb1_law2 : Pullback_law2 Fibred1_p Pb1_diese.
Proof.
unfold Pullback_law2, Pullback_eq1, Pullback_eq2 in |- *; intros r t1 t2 H.
apply Sym; apply (Prf_limit1 l (Pulb_cone H) P1).
Qed.

Lemma Prf_pb1_law3 : Pullback_law3 Fibred1_q Pb1_diese.
Proof.
unfold Pullback_law3, Pullback_eq1, Pullback_eq2 in |- *; intros r t1 t2 H.
apply Sym; apply (Prf_limit1 l (Pulb_cone H) P3).
Qed.

Lemma Prf_pb1_law4 : Pullback_law4 Fibred1_p Fibred1_q Pb1_diese.
Proof.
unfold Pullback_law4, Pullback_eq1, Pullback_eq2 in |- *;
intros r t1 t2 H h H1 H2.
unfold Pb1_diese in |- *.
apply (Prf_limit2 l).
unfold Limit_eq in |- *; simpl in |- *.
intro x; elim x; simpl in |- *.
apply Sym; exact H1.
apply Trans with (h o Fibred1_p o FMor G F12).
apply Comp_l; apply (Eq_cone (Limiting_cone l) F12).
apply Trans with ((h o Fibred1_p) o FMor G F12).
apply Ass.
apply Comp_r.
apply Sym; exact H1.
apply Sym; exact H2.
Qed.

Canonical Structure Pullback1_to_Pullback :=
Build_Pullback Prf_pb1_law1 Prf_pb1_law2 Prf_pb1_law3 Prf_pb1_law4.

End Fpullback_limit_def.

Coercion Pullback1_to_Pullback : Fpullback1 >-> Pullback.

Section pullback_limit_def.

Variables (C : Category) (a b c : C) (f : a --> b) (g : c --> b).

Definition Fpulb_ob (x : PULB) :=
match x return (Ob C) with
| P1 => a
| P2 => b
| P3 => c
end.

Definition Fpulb_mor (x y : PULB) (h : PULB_mor_setoid x y) :=
match
h in (PULB_mor x' y') return (Carrier (Fpulb_ob x' --> Fpulb_ob y'))
with
| IP1 => Id a
| IP2 => Id b
| IP3 => Id c
| F12 => f
| F32 => g
end.

Lemma Fpulb_map_law : forall x y : PULB_ob, Map_law (Fpulb_mor (x:=x) (y:=y)).
Proof.
unfold Map_law in |- *; intros x y h1.
elim h1; simpl in |- *.
intro h2;
lapply
(PULB_11_ind
(P:=fun t : PULB_mor P1 P1 =>
Equal_PULB_mor IP1 t -> Id a =_S Fpulb_mor t)).
intros H H0; apply (H h2 H0).
intro H; simpl in |- *; apply Refl.
intro h2;
lapply
(PULB_22_ind
(P:=fun t : PULB_mor P2 P2 =>
Equal_PULB_mor IP2 t -> Id b =_S Fpulb_mor t)).
intros H H0; apply (H h2 H0).
intro H; simpl in |- *; apply Refl.
intro h2;
lapply
(PULB_33_ind
(P:=fun t : PULB_mor P3 P3 =>
Equal_PULB_mor IP3 t -> Id c =_S Fpulb_mor t)).
intros H H0; apply (H h2 H0).
intro H; simpl in |- *; apply Refl.
intro h2;
lapply
(PULB_12_ind
(P:=fun t : PULB_mor P1 P2 => Equal_PULB_mor F12 t -> f =_S Fpulb_mor t)).
intros H H0; apply (H h2 H0).
intro H; simpl in |- *; apply Refl.
intro h2;
lapply
(PULB_32_ind
(P:=fun t : PULB_mor P3 P2 => Equal_PULB_mor F32 t -> g =_S Fpulb_mor t)).
intros H H0; apply (H h2 H0).
intro H; simpl in |- *; apply Refl.
Qed.

Canonical Structure Fpulb_map (x y : PULB) :=
Build_Map (Fpulb_map_law (x:=x) (y:=y)).

Lemma Fpulb_comp_law : Fcomp_law Fpulb_map.
Proof.
unfold Fcomp_law in |- *; simpl in |- *; intros x y z h1.
elim h1; simpl in |- *.
elim z; intro h2.
simpl in |- *;
lapply
(PULB_11_ind (P:=fun t : PULB_mor P1 P1 => Id a =_S Id a o Fpulb_mor t)).
intro H; apply (H h2).
simpl in |- *; apply Idr.
simpl in |- *;
lapply (PULB_12_ind (P:=fun t : PULB_mor P1 P2 => f =_S Id a o Fpulb_mor t)).
intro H; apply (H h2).
simpl in |- *; apply Idl1.
apply
(PULB_13_ind
(fun t : PULB_mor P1 P3 =>
Fpulb_mor (Comp_PULB_mor IP1 h2) =_S Id a o Fpulb_mor h2) h2).
elim z; intro h2.
apply
(PULB_21_ind
(fun a : PULB_mor P2 P1 =>
Fpulb_mor (Comp_PULB_mor IP2 h2) =_S Id b o Fpulb_mor h2) h2).
simpl in |- *;
lapply
(PULB_22_ind (P:=fun t : PULB_mor P2 P2 => Id b =_S Id b o Fpulb_mor t)).
intro H; apply (H h2).
simpl in |- *; apply Idr.
apply
(PULB_23_ind
(fun a : PULB_mor P2 P3 =>
Fpulb_mor (Comp_PULB_mor IP2 h2) =_S Id b o Fpulb_mor h2) h2).
elim z; intro h2.
apply
(PULB_31_ind
(fun a : PULB_mor P3 P1 =>
Fpulb_mor (Comp_PULB_mor IP3 h2) =_S Id c o Fpulb_mor h2) h2).
simpl in |- *;
apply (PULB_32_ind (P:=fun a : PULB_mor P3 P2 => g =_S Id c o Fpulb_mor a)).
simpl in |- *; apply Idl1.
simpl in |- *;
lapply
(PULB_33_ind (P:=fun t : PULB_mor P3 P3 => Id c =_S Id c o Fpulb_mor t)).
intro H; apply (H h2).
simpl in |- *; apply Idr.
elim z; intro h2.
apply
(PULB_21_ind
(fun a : PULB_mor P2 P1 =>
Fpulb_mor (Comp_PULB_mor F12 h2) =_S f o Fpulb_mor h2) h2).
simpl in |- *;
lapply (PULB_22_ind (P:=fun t : PULB_mor P2 P2 => f =_S f o Fpulb_mor t)).
intro H; apply (H h2).
simpl in |- *; apply Idr.
apply
(PULB_23_ind
(fun a : PULB_mor P2 P3 =>
Fpulb_mor (Comp_PULB_mor F12 h2) =_S f o Fpulb_mor h2) h2).
elim z; intro h2.
apply
(PULB_21_ind
(fun a : PULB_mor P2 P1 =>
Fpulb_mor (Comp_PULB_mor F32 h2) =_S g o Fpulb_mor h2) h2).
simpl in |- *;
lapply (PULB_22_ind (P:=fun t : PULB_mor P2 P2 => g =_S g o Fpulb_mor t)).
intro H; apply (H h2).
simpl in |- *; apply Idr.
apply
(PULB_23_ind
(fun a : PULB_mor P2 P3 =>
Fpulb_mor (Comp_PULB_mor F32 h2) =_S g o Fpulb_mor h2) h2).
Qed.

Lemma Fpulb_id_law : Fid_law Fpulb_map.
Proof.
unfold Fid_law in |- *; simpl in |- *; intro x.
elim x; simpl in |- *; apply Refl.
Qed.

Canonical Structure Fpulb := Build_Functor Fpulb_comp_law Fpulb_id_law.

SubClass Pullback1 := Fpullback1 Fpulb.

End pullback_limit_def.