Showing changes from revision #3 to #4:
Added | Removed | Changed
Idea
Definition
Given a type , a judgment , terms and , and an identity , there are transport functions and , such that for all , the fiber of at is contractible, and for all , the fiber of at is contractible.