generated from pitmonticone/LeanProject
-
Notifications
You must be signed in to change notification settings - Fork 8
/
InfinityCosmos.lean
17 lines (17 loc) · 1.19 KB
/
InfinityCosmos.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
import Mathlib.AlgebraicTopology.Quasicategory.Nerve
import InfinityCosmos.ForMathlib.AlgebraicTopology.Quasicategory.Basic
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplexCategory
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialCategory.Basic
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialCategory.Cotensors
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialCategory.IsConicalTerminal
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialCategory.Limits
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.CoherentIso
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Homotopy
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.Monoidal
import InfinityCosmos.ForMathlib.AlgebraicTopology.SimplicialSet.MorphismProperty
import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.Cotensors
import InfinityCosmos.ForMathlib.CategoryTheory.Enriched.MonoidalProdCat
import InfinityCosmos.ForMathlib.CategoryTheory.MorphismProperty
import InfinityCosmos.ForMathlib.InfinityCosmos.Basic
import InfinityCosmos.ForMathlib.InfinityCosmos.Isofibrations