{"push_id":2611856888,"size":10,"distinct_size":10,"ref":"refs/heads/wip-image","head":"4762f886fe3b78f52d86f60640d4490545399976","before":"67459a37342090b9a90727b3e8639db1bd66baba","commits":[{"sha":"931e7b7d5f0697b3e66375e8b4f18280735ddbbb","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add reflexivity, symmetry and transitivity for Homotopy","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/931e7b7d5f0697b3e66375e8b4f18280735ddbbb"},{"sha":"6ac9a821e0837b6bff9f171f0f0095ed1df759b1","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add lemma isEquiv (PathP A x y) (transp A x ≡ y) fromPathP","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/6ac9a821e0837b6bff9f171f0f0095ed1df759b1"},{"sha":"66b22e78f57f8346c530b045528061c60a4b95a0","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add Lemma 2.11.2 (transp (λ i → χ i ≡ ψ i) p ≡ χ⁻¹ ◾ p ◾ ψ)","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/66b22e78f57f8346c530b045528061c60a4b95a0"},{"sha":"a2d25ecc03b6bc61ed2aa5323bfee701a22e6ec6","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add Lemma 4.9.2 (A ≃ B → (X → A) ≃ (X → B))","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/a2d25ecc03b6bc61ed2aa5323bfee701a22e6ec6"},{"sha":"4c7c517ca0dfda825f6f174ebd391ba7973ff7c3","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add (part of) Exercise 2.17 (iii) (Σ preserves equivalence in left argument)","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/4c7c517ca0dfda825f6f174ebd391ba7973ff7c3"},{"sha":"2cd422c60e6b57b1acfa0fbf7690312290031668","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add lemma Σ A Σ B C ≃ Σ B Σ A C","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/2cd422c60e6b57b1acfa0fbf7690312290031668"},{"sha":"b92323a6f8bddf599fb651bad53104b6492dffb9","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add proof of Lemma 4.8.2 (A ≃ Σ B (fiber f))","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/b92323a6f8bddf599fb651bad53104b6492dffb9"},{"sha":"15565d900c1951ffa1b1d06c3ee22575b3128cfe","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add Definition 2.1 in Rijke17 (Join of maps)","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/15565d900c1951ffa1b1d06c3ee22575b3128cfe"},{"sha":"66290609d2045f3c3e91e15054ea52c5fcb2fa97","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add lemma isPullBack (p , q , H) ≃ isEquiv ⟨p , q , H⟩","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/66290609d2045f3c3e91e15054ea52c5fcb2fa97"},{"sha":"4762f886fe3b78f52d86f60640d4490545399976","author":{"name":"Fabian","email":"82296eb15e8045a1d569dd3417ad2c54f4c3eb07@gmail.com"},"message":"Add lemma isPullBack (p , q , H) ≃ ∀ a. fiber p a ≃ fiber g (f a)","distinct":true,"url":"https://api.github.com/repos/bafain/cubical-demo/commits/4762f886fe3b78f52d86f60640d4490545399976"}]}
{"actor":{"display_login":"bafain"}}