forked from dagurtomas/LeanCondensed
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathLeanCondensed.lean
More file actions
17 lines (17 loc) · 832 Bytes
/
Copy pathLeanCondensed.lean
File metadata and controls
17 lines (17 loc) · 832 Bytes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
import LeanCondensed.Mathlib.CategoryTheory.Countable
import LeanCondensed.Mathlib.CategoryTheory.Functor.EpiMono
import LeanCondensed.Mathlib.CategoryTheory.Sites.DirectImage
import LeanCondensed.Mathlib.Condensed.Adjunctions
import LeanCondensed.Mathlib.Condensed.Light.Limits
import LeanCondensed.Mathlib.Condensed.Light.Monoidal
import LeanCondensed.Mathlib.Topology.Category.CompHausLike.Limits
import LeanCondensed.Projects.Epi
import LeanCondensed.Projects.FreeCondensed
import LeanCondensed.Projects.IsLocalizedMonoidal
import LeanCondensed.Projects.LightProfiniteInjective
import LeanCondensed.Projects.LightSolid
import LeanCondensed.Projects.MonoidalLinear
import LeanCondensed.Projects.PreservesCoprod
import LeanCondensed.Projects.Proj
import LeanCondensed.Projects.Sequence
import LeanCondensed.Projects.SheafMonoidal