{"push_id":2710574691,"size":90,"distinct_size":90,"ref":"refs/heads/master","head":"36a1ba8e349f2c73a3de8cb0eac6eb5331019dc3","before":"3f8d8cc076c3adc5956653f1d04bd56256b6ec23","commits":[{"sha":"89cd33067fafeb833ca23e844332267685353e1b","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Rename badly chose name: equivalence --> invertible_2cell.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/89cd33067fafeb833ca23e844332267685353e1b"},{"sha":"8ff3e3f7c44febddce764d89e6edc645934319ae","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Work on internal adjunction.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/8ff3e3f7c44febddce764d89e6edc645934319ae"},{"sha":"0b54b89b15887b7f247ac3fcbb453553c242af8a","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Displayed equivalences.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/0b54b89b15887b7f247ac3fcbb453553c242af8a"},{"sha":"fa20cdbd54f3dd26603ef27be07d1fa7a99bc20e","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Bicategories: Definition of local-iso-fibration.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/fa20cdbd54f3dd26603ef27be07d1fa7a99bc20e"},{"sha":"f4e7b3dc21205910a0ba7b33019f3a5b916288c1","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"WIP","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/f4e7b3dc21205910a0ba7b33019f3a5b916288c1"},{"sha":"7f9b9820301d6cda802a6e44896104584dfe28e9","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Fix renaming.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/7f9b9820301d6cda802a6e44896104584dfe28e9"},{"sha":"68a1e99d3f988143a2fb0b8e21bf26ef28e0bbe2","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Work for Local-iso-fibrations.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/68a1e99d3f988143a2fb0b8e21bf26ef28e0bbe2"},{"sha":"918ad1c46404cc14a3626f78d444d2ac23cfc9de","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Definition of univalence.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/918ad1c46404cc14a3626f78d444d2ac23cfc9de"},{"sha":"e3e1cb81ea20ea72ae1e3e2cc949e3156767a639","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Merge remote-tracking branch 'upstream/master' into bicat-local-isofib","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/e3e1cb81ea20ea72ae1e3e2cc949e3156767a639"},{"sha":"917a89b7b64b724a1b0f1a566a3e78375fe51030","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"WIP displayed adjunction.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/917a89b7b64b724a1b0f1a566a3e78375fe51030"},{"sha":"f38487e40291a72d5dd14a963671a5ffcb5c020c","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Ooops","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/f38487e40291a72d5dd14a963671a5ffcb5c020c"},{"sha":"0ef8aba716e4d87a2701843419a65a82e802f579","author":{"name":"Benedikt Ahrens","email":"b7c4baa775b92bf60ed8f6ecd5ac9f457efbb970@gmx.net"},"message":"small reorganization of internal adjunctions","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/0ef8aba716e4d87a2701843419a65a82e802f579"},{"sha":"3386994fceda9c32707a01d458e92671d94e31ec","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Towards displayed univalence_2.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/3386994fceda9c32707a01d458e92671d94e31ec"},{"sha":"592add1eee47429b8050b5279e399d17dc7bade8","author":{"name":"Benedikt Ahrens","email":"b7c4baa775b92bf60ed8f6ecd5ac9f457efbb970@gmx.net"},"message":"disp interal equivalences","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/592add1eee47429b8050b5279e399d17dc7bade8"},{"sha":"fa049fa847276a271397b5d7e3b77a021fb4cb0b","author":{"name":"Benedikt Ahrens","email":"b7c4baa775b92bf60ed8f6ecd5ac9f457efbb970@gmx.net"},"message":"towards disp identity adj equiv","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/fa049fa847276a271397b5d7e3b77a021fb4cb0b"},{"sha":"cfc2171bab95c07623ef41c7a97feaa0c17563ec","author":{"name":"Benedikt Ahrens","email":"b7c4baa775b92bf60ed8f6ecd5ac9f457efbb970@gmx.net"},"message":"start proof of lunitor = runitor","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/cfc2171bab95c07623ef41c7a97feaa0c17563ec"},{"sha":"db1a2212ffb32ae5cd34d84eaada1bde308a2ecd","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Go to dinner!!!","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/db1a2212ffb32ae5cd34d84eaada1bde308a2ecd"},{"sha":"e6592ebc4c53d8d2bfc024028f5cac77ddd01527","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Fix a missing open section.","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/e6592ebc4c53d8d2bfc024028f5cac77ddd01527"},{"sha":"decb0d1f7d8c2c7cf1697a6b9af45ecbf1e429da","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Now load DispUnivalence.v","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/decb0d1f7d8c2c7cf1697a6b9af45ecbf1e429da"},{"sha":"e7462200a8ee1e387d6f89846ca629e08e1f3e99","author":{"name":"Marco Maggesi","email":"4bb006776fa135186cf07d90f4956290eb2c939c@users.noreply.github.com"},"message":"Merge pull request #29 from maggesi/ba-l-r\n\nstart proof of lunitor = runitor","distinct":true,"url":"https://api.github.com/repos/Marmann/UniMath/commits/e7462200a8ee1e387d6f89846ca629e08e1f3e99"}]}
{"actor":{"display_login":"Marmann"}}