- Section ArrowInLanguage.
- Context {MF}{mn:MonoidalCat TypesL (fun x => (fst_obj _ _ x),,(snd_obj _ _ x)) MF []} (CC:CartesianCat mn).
- Context {Kehom}(K:@ECategory _ _ TypesL _ mn [] mn TypesL Kehom).
- Context {bc:BinoidalCat (Underlying K) (@T_Branch _)}.
- Context (pmc:@PreMonoidalCat _ _ _ _ bc (@one _ _ _ (car_terminal(CartesianCat:=CC)))).
- Definition ArrowInProgrammingLanguage := @FreydCategory _ _ _ _ _ _ mn _ _ _ _ pmc.
- End ArrowInLanguage.