Maths - Category Theory - Substitution

Imagine we have a property (a predicate) P that is true for all values of x property diagram
We can substitute y for x where y is a function of x: property substitution diagram
  set substitution diagram

 

Πx:T -->
<-- (-)×T
Σx:T -->

As a sort of intuitive justification for this:

If we have a total function:

f: x -> y

Then we are saying 'y' exists for all 'x'.

https://ncatlab.org/nlab/show/substitution

Substitute Variables and Literals

In type theory the deconstruct + construct (compute) allows us to substitute one variable for another.

Can we substitute between variables and literal values?

If we start with a variable we can always go to a literal value (there exists) but all literal values must apply (for all) before we can convert to a variable.

The following diagram is my attempt to draw this as fibre bundles:

See Bartosz Milewski on his blog here.

existentialthere exists,sum Σ left adjoint

weakening
(adding an extra assumption)

weakening left adjoint universalfor all, product Π

Substitute Variables and Expressions (Terms)

We have seen interesting structure when we substitute between variables and literals, now lets try substituting between variables and expressions.

In Type Theory

Use 'context extension' instead of substitution.

https://ncatlab.org/nlab/show/context+extension

In Category Theory

Pullback

Substitution of a term into a predicate is pullback, but substitution of a term into a term is composition.

Or if you are a type theorist:

Substitution of a term into a dependent type is pullback, but substitution of a term into a term is composition.

http://math.andrej.com/2012/09/28/substitution-is-pullback/

substitution diagram

Discussed more on these pages:


metadata block
see also:

 

Adjunctions from Morphisms

Other Pages on this site

  • Category of graphs described on page here.
  • Implementing Graphs in FriCas program is discussed on page here.
  • Implementing Posets in FriCas program is discussed on page here.
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Conceptual Mathematics - This is a book about category theory that does not assume an extensive knowledge over a wide area of mathematics. The style of the book is a bit quirky though.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2024 Martin John Baker - All rights reserved - privacy policy.