Sketches

Sketches are a diagrammatic formalism for specifying logical theories, originating with Ehresmann. Sketches with finite products correspond to algebraic theories and sketches with finite limits correspond to essentially algebraic theories.

Literature

Books and surveys

Sketches feature prominently in the works of Barr and Wells:

  • Barr & Wells, 1985: Toposes, triples, and theories (pdf)
  • Barr & Wells, 1995: Category theory for computing science (pdf)
  • Wells, 1993: Sketches: outline with references (pdf)
  • Barr, 1999: Notes on sketches (pdf)

Other book treatments:

  • Johnstone, 2002: Sketches of an elephant, Chapter D2: Sketches

History and philosophy of sketches:

  • Marquis, 2009: From a geometrical point of view: A study of the history and philosophy of category theory (doi), Section 6.7: Graphical syntax: sketches
  • Halimi, 2012: Diagrams as sketches (doi, jstor )

Extensions

Sketches have been generalized in various directions, including to enriched categories and symmetric monoidal categories.

  • Makkai, 1997: Generalized sketches as a framework for completeness theorems (parts I, II, III)
  • Borceux, Quinteiro, Rosicky, 1998: A theory of enriched sketches (pdf)
  • Hyland & Power, 2004: Symmetric monoidal sketches and categories of wirings (doi, pdf)
    • Hyland & Power, 2000: Symmetric monoidal sketches (doi)
  • Bagchi & Wells, 2008: Graph-based logic and sketches (arxiv)
    • Monograph based on 1995 and 1996 papers by authors
    • Proposes a generalization of sketches called “forms”

Applications