Theorem 5.8.2 from the book: characterizations of identity types #3039
Annotations
1 error
|
Run coq-community/docker-coq-action@v1:
contrib/HoTTBook.v#L783
The reference HoTT.PathAny.contr_pfammap_identitysystem was not found
in the current environment.
Command exited with non-zero status 1
|
Loading