| Commit message (Collapse) | Author | Files | Lines |
|
|
|
|
|
|
|
Definition of function composition and properties.
|
|
Definition of function composition and properties.
|
|
natural number predecessor function.
|
|
|
|
|
|
|
|
|
|
derivation of "A:U" from "a:A".
|
|
|
|
|
|
be needed or useful later. Added [comp] attribute to be used by simplification met methods.
|
|
|
|
|
|
|
|
|
|
formulation in the HoTT book.
|
|
|