fact: Definition Comp_PA_mor (x y z : PA_ob) (f : PA_mor x y) := match f in (PA_mor p p0) return (PA_mor p0 z -> PA_mor p z) with | PA_I1 => match z as p return (PA_mor PA1 p -> PA_mor PA1 p) with | PA1 => fun _ => PA_I1 | PA2 => fun g => g end | PA_I2 => match z as p return (PA_mor PA2 p -> PA_mor PA2 p) with | PA1 => fun g => PA_21_rect (fun _ => PA_mor PA2 PA1) g | PA2 => fun _ => PA_I2 end | PA_f x => match z as p return (I -> PA_mor PA2 p -> PA_mor PA1 p) with | PA1 => fun _ g => PA_21_rect (fun _ => PA_mor PA1 PA1) g | PA2 => fun i _ => PA_f i end x end.
imports: BasicTypes Category