Proof:Assume HC.
Apply MetaCat_E Obj Hom id comp HC to the current goal.
Assume HC1: ∀X : set, Obj X → Hom X X (id X).
Assume HC2: ∀X Y Z : set, ∀f g : set, Obj X → Obj Y → Obj Z → Hom X Y f → Hom Y Z g → Hom X Z (comp X Y Z g f).
Assume HC3: ∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X X Y f (id X) = f.
Assume HC4: ∀X Y : set, ∀f : set, Obj X → Obj Y → Hom X Y f → comp X Y Y (id Y) f = f.
Assume HC5: ∀X Y Z W : set, ∀f g h : set, Obj X → Obj Y → Obj Z → Obj W → Hom X Y f → Hom Y Z g → Hom Z W h → comp X Y W (comp Y Z W h g) f = comp X Z W h (comp X Y Z g f).
Let quot, canonmap and fac be given.
Let prod, pi0, pi1 and pair be given.
Let X, Y and Z be given.
Assume HX: Obj X.
Assume HY: Obj Y.
Assume HZ: Obj Z.
Let f and g be given.
Assume Hf: Hom X Z f.
Assume Hg: Hom Y Z g.
Set pi0f to be the term comp (prod X Y) X Z f (pi0 X Y).
Set pi1g to be the term comp (prod X Y) Y Z g (pi1 X Y).
Set P to be the term quot (prod X Y) Z pi0f pi1g.
Set pi0P to be the term comp P (prod X Y) X (pi0 X Y) (canonmap (prod X Y) Z pi0f pi1g).
Set pi1P to be the term comp P (prod X Y) Y (pi1 X Y) (canonmap (prod X Y) Z pi0f pi1g).
Set pairP to be the term (λW : set ⇒ λh k : set ⇒ fac (prod X Y) Z pi0f pi1g W (pair X Y W h k)).
Apply HP X Y HX HY to the current goal.
Assume HP1.
Apply HP1 to the current goal.
Assume HP1.
Apply HP1 to the current goal.
Assume HP1.
Apply HP1 to the current goal.
Assume HP1.
Apply HP1 to the current goal.
Assume _ _.
Assume HP1: Obj (prod X Y).
Assume HP2: Hom (prod X Y) X (pi0 X Y).
Assume HP3: Hom (prod X Y) Y (pi1 X Y).
Assume HP4: ∀W : set, Obj W → ∀h k : set, Hom W X h → Hom W Y k → Hom W (prod X Y) (pair X Y W h k) ∧ comp W (prod X Y) X (pi0 X Y) (pair X Y W h k) = h ∧ comp W (prod X Y) Y (pi1 X Y) (pair X Y W h k) = k ∧ ∀u : set, Hom W (prod X Y) u → comp W (prod X Y) X (pi0 X Y) u = h → comp W (prod X Y) Y (pi1 X Y) u = k → u = pair X Y W h k.
We prove the intermediate claim Lpi0f: Hom (prod X Y) Z pi0f.
An exact proof term for the current goal is HC2 (prod X Y) X Z (pi0 X Y) f HP1 HX HZ HP2 Hf.
We prove the intermediate claim Lpi1g: Hom (prod X Y) Z pi1g.
An exact proof term for the current goal is HC2 (prod X Y) Y Z (pi1 X Y) g HP1 HY HZ HP3 Hg.
Apply HE (prod X Y) Z HP1 HZ pi0f pi1g Lpi0f Lpi1g to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume HE1.
Apply HE1 to the current goal.
Assume _ _ _ _.
Assume HE1: Obj P.
Assume HE2: Hom P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g).
Assume HE3: comp P (prod X Y) Z pi0f (canonmap (prod X Y) Z pi0f pi1g) = comp P (prod X Y) Z pi1g (canonmap (prod X Y) Z pi0f pi1g).
Assume HE4: ∀W : set, Obj W → ∀h : set, Hom W (prod X Y) h → comp W (prod X Y) Z pi0f h = comp W (prod X Y) Z pi1g h → Hom W P (fac (prod X Y) Z pi0f pi1g W h) ∧ comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) (fac (prod X Y) Z pi0f pi1g W h) = h ∧ ∀u : set, Hom W P u → comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u = h → u = fac (prod X Y) Z pi0f pi1g W h.
We prove the intermediate claim Lpi0P: Hom P X pi0P.
An exact proof term for the current goal is HC2 P (prod X Y) X (canonmap (prod X Y) Z pi0f pi1g) (pi0 X Y) HE1 HP1 HX HE2 HP2.
We prove the intermediate claim Lpi1P: Hom P Y pi1P.
An exact proof term for the current goal is HC2 P (prod X Y) Y (canonmap (prod X Y) Z pi0f pi1g) (pi1 X Y) HE1 HP1 HY HE2 HP3.
We will
prove pullback_p Obj Hom id comp X Y Z f g P pi0P pi1P pairP.
We will prove Obj X ∧ Obj Y ∧ Obj Z ∧ Hom X Z f ∧ Hom Y Z g ∧ Obj P ∧ Hom P X pi0P ∧ Hom P Y pi1P ∧ comp P X Z f pi0P = comp P Y Z g pi1P ∧ ∀W : set, Obj W → ∀h : set, Hom W X h → ∀k : set, Hom W Y k → comp W X Z f h = comp W Y Z g k → Hom W P (pairP W h k) ∧ comp W P X pi0P (pairP W h k) = h ∧ comp W P Y pi1P (pairP W h k) = k ∧ ∀u : set, Hom W P u → comp W P X pi0P u = h → comp W P Y pi1P u = k → u = pairP W h k.
Apply and10I to the current goal.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is HZ.
An exact proof term for the current goal is Hf.
An exact proof term for the current goal is Hg.
We will prove Obj P.
An exact proof term for the current goal is HE1.
We will prove Hom P X pi0P.
An exact proof term for the current goal is Lpi0P.
We will prove Hom P Y pi1P.
An exact proof term for the current goal is Lpi1P.
We will prove comp P X Z f pi0P = comp P Y Z g pi1P.
We will prove comp P X Z f (comp P (prod X Y) X (pi0 X Y) (canonmap (prod X Y) Z pi0f pi1g)) = comp P Y Z g (comp P (prod X Y) Y (pi1 X Y) (canonmap (prod X Y) Z pi0f pi1g)).
Use transitivity with comp P (prod X Y) Z pi0f (canonmap (prod X Y) Z pi0f pi1g), and comp P (prod X Y) Z pi1g (canonmap (prod X Y) Z pi0f pi1g).
Use symmetry.
Apply HC5 to the current goal.
An exact proof term for the current goal is HE1.
An exact proof term for the current goal is HP1.
An exact proof term for the current goal is HX.
An exact proof term for the current goal is HZ.
An exact proof term for the current goal is HE2.
An exact proof term for the current goal is HP2.
An exact proof term for the current goal is Hf.
We will prove comp P (prod X Y) Z pi0f (canonmap (prod X Y) Z pi0f pi1g) = comp P (prod X Y) Z pi1g (canonmap (prod X Y) Z pi0f pi1g).
An exact proof term for the current goal is HE3.
Apply HC5 to the current goal.
An exact proof term for the current goal is HE1.
An exact proof term for the current goal is HP1.
An exact proof term for the current goal is HY.
An exact proof term for the current goal is HZ.
An exact proof term for the current goal is HE2.
An exact proof term for the current goal is HP3.
An exact proof term for the current goal is Hg.
Let W be given.
Assume HW: Obj W.
Let h be given.
Assume Hh: Hom W X h.
Let k be given.
Assume Hk: Hom W Y k.
Assume Hhk: comp W X Z f h = comp W Y Z g k.
Apply HP4 W HW h k Hh Hk to the current goal.
Assume HP4a.
Apply HP4a to the current goal.
Assume HP4a.
Apply HP4a to the current goal.
Assume HP4a: Hom W (prod X Y) (pair X Y W h k).
Assume HP4b: comp W (prod X Y) X (pi0 X Y) (pair X Y W h k) = h.
Assume HP4c: comp W (prod X Y) Y (pi1 X Y) (pair X Y W h k) = k.
Assume HP4d: ∀u : set, Hom W (prod X Y) u → comp W (prod X Y) X (pi0 X Y) u = h → comp W (prod X Y) Y (pi1 X Y) u = k → u = pair X Y W h k.
We prove the intermediate claim LP1: comp W (prod X Y) Z pi0f (pair X Y W h k) = comp W (prod X Y) Z pi1g (pair X Y W h k).
Use transitivity with comp W X Z f (comp W (prod X Y) X (pi0 X Y) (pair X Y W h k)), and comp W Y Z g (comp W (prod X Y) Y (pi1 X Y) (pair X Y W h k)).
An exact proof term for the current goal is HC5 W (prod X Y) X Z (pair X Y W h k) (pi0 X Y) f HW HP1 HX HZ HP4a HP2 Hf.
We will prove comp W X Z f (comp W (prod X Y) X (pi0 X Y) (pair X Y W h k)) = comp W Y Z g (comp W (prod X Y) Y (pi1 X Y) (pair X Y W h k)).
rewrite the current goal using HP4b (from left to right).
rewrite the current goal using HP4c (from left to right).
We will prove comp W X Z f h = comp W Y Z g k.
An exact proof term for the current goal is Hhk.
Use symmetry.
An exact proof term for the current goal is HC5 W (prod X Y) Y Z (pair X Y W h k) (pi1 X Y) g HW HP1 HY HZ HP4a HP3 Hg.
Apply HE4 W HW (pair X Y W h k) HP4a LP1 to the current goal.
Assume HE4a.
Apply HE4a to the current goal.
Assume HE4a: Hom W P (fac (prod X Y) Z pi0f pi1g W (pair X Y W h k)).
Assume HE4b: comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) (fac (prod X Y) Z pi0f pi1g W (pair X Y W h k)) = pair X Y W h k.
Assume HE4c: ∀u : set, Hom W P u → comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u = pair X Y W h k → u = fac (prod X Y) Z pi0f pi1g W (pair X Y W h k).
We prove the intermediate claim Lhk: Hom W P (pairP W h k).
An exact proof term for the current goal is HE4a.
Apply and4I to the current goal.
We will prove Hom W P (pairP W h k).
An exact proof term for the current goal is Lhk.
We will prove comp W P X pi0P (pairP W h k) = h.
Use transitivity with and comp W (prod X Y) X (pi0 X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) (fac (prod X Y) Z pi0f pi1g W (pair X Y W h k))).
An exact proof term for the current goal is HC5 W P (prod X Y) X (pairP W h k) (canonmap (prod X Y) Z pi0f pi1g) (pi0 X Y) HW HE1 HP1 HX HE4a HE2 HP2.
rewrite the current goal using HE4b (from left to right).
We will prove comp W (prod X Y) X (pi0 X Y) (pair X Y W h k) = h.
An exact proof term for the current goal is HP4b.
We will prove comp W P Y pi1P (pairP W h k) = k.
Use transitivity with and comp W (prod X Y) Y (pi1 X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) (fac (prod X Y) Z pi0f pi1g W (pair X Y W h k))).
An exact proof term for the current goal is HC5 W P (prod X Y) Y (pairP W h k) (canonmap (prod X Y) Z pi0f pi1g) (pi1 X Y) HW HE1 HP1 HY HE4a HE2 HP3.
rewrite the current goal using HE4b (from left to right).
We will prove comp W (prod X Y) Y (pi1 X Y) (pair X Y W h k) = k.
An exact proof term for the current goal is HP4c.
Let u be given.
Assume Hu: Hom W P u.
Assume Huh: comp W P X pi0P u = h.
Assume Huk: comp W P Y pi1P u = k.
We will prove u = pairP W h k.
We will prove u = fac (prod X Y) Z pi0f pi1g W (pair X Y W h k).
Apply HE4c u Hu to the current goal.
We will prove comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u = pair X Y W h k.
Apply HP4d (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u) to the current goal.
We will prove Hom W (prod X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u).
An exact proof term for the current goal is HC2 W P (prod X Y) u (canonmap (prod X Y) Z pi0f pi1g) HW HE1 HP1 Hu HE2.
We will prove comp W (prod X Y) X (pi0 X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u) = h.
rewrite the current goal using HC5 W P (prod X Y) X u (canonmap (prod X Y) Z pi0f pi1g) (pi0 X Y) HW HE1 HP1 HX Hu HE2 HP2 (from right to left).
We will prove comp W P X (comp P (prod X Y) X (pi0 X Y) (canonmap (prod X Y) Z pi0f pi1g)) u = h.
An exact proof term for the current goal is Huh.
We will prove comp W (prod X Y) Y (pi1 X Y) (comp W P (prod X Y) (canonmap (prod X Y) Z pi0f pi1g) u) = k.
rewrite the current goal using HC5 W P (prod X Y) Y u (canonmap (prod X Y) Z pi0f pi1g) (pi1 X Y) HW HE1 HP1 HY Hu HE2 HP3 (from right to left).
We will prove comp W P Y (comp P (prod X Y) Y (pi1 X Y) (canonmap (prod X Y) Z pi0f pi1g)) u = k.
An exact proof term for the current goal is Huk.
∎