Switch to: References

Add citations

You must login to add citations.
  1. Coherence in cartesian closed categories and the generality of proofs.M. E. Szabo - 1989 - Studia Logica 48 (3):285 - 297.
    We introduce the notion of an alphabetic trace of a cut-free intuitionistic prepositional proof and show that it serves to characterize the equality of arrows in cartesian closed categories. We also show that alphabetic traces improve on the notion of the generality of proofs proposed in the literature. The main theorem of the paper yields a new and considerably simpler solution of the coherence problem for cartesian closed categories than those in [11, 14].
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Functional completeness of cartesian categories.J. Lambek - 1974 - Annals of Mathematical Logic 6 (3):259.
  • Bicartesian coherence.Kosta Došen & Zoran Petrić - 2002 - Studia Logica 71 (3):331 - 353.
    Coherence is demonstrated for categories with binary products and sums, but without the terminal and the initial object, and without distribution. This coherence amounts to the existence of a faithful functor from a free category with binary products and sums to the category of relations on finite ordinals. This result is obtained with the help of proof-theoretic normalizing techniques. When the terminal object is present, coherence may still be proved if of binary sums we keep just their bifunctorial properties. It (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   7 citations