fact: 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.
imports: Limit PULB Pullbacks