Practical Foundations of Mathematics

Paul Taylor

VIII. Algebra with Dependent Types

VIII. Algebra with Dependent Types

Practical Foundations of Mathematics   Paul Taylor   Cambridge University Press

Introduction   I   II   III   IV   V   VI   VII   VIII   IX   Bibliography  Index

INTRODUCTION

8.1    THE LANGUAGE

8.2    THE CATEGORY OF CONTEXTS

8.3    DISPLAY CATEGORIES AND EQUALITY TYPES

8.4    INTERPRETATION

EXERCISES  VIII