Imagine we have a property (a predicate) P that is true for all values of x 
We can substitute y for x where y is a function of x: 
 The universal quantifier is the right adjoint of substitution.
 The existential quantifier is the left adjoint of substitution.
Π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 () but all literal values must apply () 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.
existential,sum Σ  weakening 

weakening  universal, 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. 
Discussed more on these pages:
 More about binding variables and substitution on the type theory pages.
 More about substitution and lambda functions on the page here .