# Contents

## Idea

In the general context of foundations of mathematics in practical foundations (following a term introduced in (Taylor)) the emphasis is on conceptually natural formalizations that concentrate the essence of practice and in turn use the result to guide practice (Lawvere), as in (Eilenberg-Steenrod, Harper).

Formal systems of interest here are natural deduction in type theories, which allow natural expressions for central concepts in mathematics (notably via their categorical semantics and the conceptual strength of category theory).

## References

• Paul Taylor, Practical Foundations of Mathematics, Cambridge University Press (web)

Under computational trinitarianism this corresponds to a practical foundation in programming, laid out in

A foundation for algebraic topology is this practical spirit is laid out in

Revised on October 12, 2012 16:50:37 by Urs Schreiber (164.15.117.235)