OAI/GroupTheory/SimpleAmenable/Simplicial/IntervalFunctor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.IntervalBar.Diagram.reindexMonoidal line 16
2. def OAI.IntervalBar.Diagram.mapεHom line 65
3. def OAI.IntervalBar.Diagram.mapμHom line 76
4. instance OAI.IntervalBar.Diagram.mapMonoidal line 96
5. instance OAI.IntervalBar.Diagram.reindexBraided line 116
6. instance OAI.IntervalBar.Diagram.mapBraided line 123
7. instance OAI.IntervalBar.Diagram.evalBraided line 129
8. lemma OAI.IntervalBar.Diagram.ext_heq line 149
9. lemma OAI.IntervalBar.Diagram.eqToHom_app line 153
10. lemma OAI.IntervalBar.Diagram.mapObj_id line 157
11. lemma OAI.IntervalBar.Diagram.map_id line 168
12. lemma OAI.IntervalBar.Diagram.mapObj_comp line 177
13. lemma OAI.IntervalBar.Diagram.map_comp line 189
14. lemma OAI.IntervalBar.Diagram.reindex_map line 201