OAI/GroupTheory/SimpleAmenable/Simplicial/StageRefinementMonoidal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.refineFiber_sum_inl line 20
2. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.refineFiber_sum_inr line 24
3. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.refineEvaluationIso_enum line 28
4. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.Stage.refineEvaluationIso_monoidal line 35
5. lemma OAI.IntervalBar.Diagram.monoidalNatTrans_eta line 78
6. def OAI.IntervalBar.Diagram.mapNatTrans line 83
7. instance OAI.IntervalBar.Diagram.mapNatTrans_monoidal line 99
8. lemma OAI.NerveHomotopy.functor_map_heq line 119
9. lemma OAI.NerveHomotopy.comp_heq line 120
10. lemma OAI.NerveHomotopy.cylinder_natural line 128