{"push_id":856589913,"size":2,"distinct_size":2,"ref":"refs/heads/postponing-use-of-funextempty","head":"8f3f1a2bc9ae6fa0597688ac176b600f7beda654","before":"647ac1381412ea88d99abddea8eab1ffd19170d9","commits":[{"sha":"131206f5e59b71c187e37b75e5f95c353533cfb1","author":{"email":"2591e5f46f28d303f9dc027d475a5c60d8dea17a@math.uiuc.edu","name":"Daniel R. Grayson"},"message":"add two lemmas about cancellation of paths\n\nLemma pathscomp_cancel_left {X:UU} {x y z:X} (p:x=y) (r s:y=z) : p@r=p@s -> r=s.\nLemma pathscomp_cancel_right {X:UU} {x y z:X} (p q:x=y) (s:y=z) : p@s=q@s -> p=q.","distinct":true,"url":"https://api.github.com/repos/DanGrayson/UniMath/commits/131206f5e59b71c187e37b75e5f95c353533cfb1"},{"sha":"8f3f1a2bc9ae6fa0597688ac176b600f7beda654","author":{"email":"2591e5f46f28d303f9dc027d475a5c60d8dea17a@math.uiuc.edu","name":"Daniel R. Grayson"},"message":"simplify","distinct":true,"url":"https://api.github.com/repos/DanGrayson/UniMath/commits/8f3f1a2bc9ae6fa0597688ac176b600f7beda654"}]}