fact: Definition Comp_PULB_mor (a b c : PULB_ob) (f : PULB_mor_setoid a b) := match f in (PULB_mor p p0) return (PULB_mor_setoid p0 c -> PULB_mor_setoid p c) with | IP1 => match c as p return (PULB_mor P1 p -> PULB_mor P1 p) with | P1 => fun _ => IP1 | P2 => fun _ => F12 | P3 => fun g => PULB_13_rect (fun _ : PULB_mor P1 P3 => PULB_mor P1 P3) g end | IP2 => match c as p return (PULB_mor P2 p -> PULB_mor P2 p) with | P1 => fun g => PULB_21_rect (fun _ : PULB_mor P2 P1 => PULB_mor P2 P1) g | P2 => fun _ => IP2 | P3 => fun g => PULB_23_rect (fun _ : PULB_mor P2 P3 => PULB_mor P2 P3) g end | IP3 => match c as p return (PULB_mor P3 p -> PULB_mor P3 p) with | P1 => fun g => PULB_31_rect (fun _ : PULB_mor P3 P1 => PULB_mor P3 P1) g | P2 => fun _ => F32 | P3 => fun _ => IP3 end | F12 => match c as p return (PULB_mor P2 p -> PULB_mor P1 p) with | P1 => fun g => PULB_21_rect (fun _ : PULB_mor P2 P1 => PULB_mor P1 P1) g | P2 => fun _ => F12 | P3 => fun g => PULB_23_rect (fun _ : PULB_mor P2 P3 => PULB_mor P1 P3) g end | F32 => match c as p return (PULB_mor P2 p -> PULB_mor P3 p) with | P1 => fun g => PULB_21_rect (fun _ : PULB_mor P2 P1 => PULB_mor P3 P1) g | P2 => fun _ => F32 | P3 => fun g => PULB_23_rect (fun _ : PULB_mor P2 P3 => PULB_mor P3 P3) g end end.
imports: Category BasicTypes