-
Notifications
You must be signed in to change notification settings - Fork 0
/
UniverseAbstractions.lean
62 lines (58 loc) · 3.28 KB
/
UniverseAbstractions.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
import UniverseAbstractions.Axioms.Universes
import UniverseAbstractions.Axioms.MetaProperties
import UniverseAbstractions.Axioms.MetaRelations
import UniverseAbstractions.Axioms.Universe.Identity
import UniverseAbstractions.Axioms.Universe.Functors
import UniverseAbstractions.Axioms.Universe.FunctorExtensionality
import UniverseAbstractions.Axioms.Universe.Singletons
import UniverseAbstractions.Axioms.Universe.Products
import UniverseAbstractions.Axioms.Universe.Equivalences
import UniverseAbstractions.Axioms.Universe.StandardEquivalences
import UniverseAbstractions.Axioms.Universe.TypeConstructors
import UniverseAbstractions.Axioms.Universe.DependentTypes.Properties
import UniverseAbstractions.Axioms.Universe.DependentTypes.Relations
import UniverseAbstractions.Axioms.Universe.DependentTypes.DependentFunctors
import UniverseAbstractions.Axioms.Universe.DependentTypes.DependentProducts
import UniverseAbstractions.Axioms.Universe.DependentTypes.Independent
import UniverseAbstractions.Axioms.Universe.FunctorialIdentities.IdentityQuantification
import UniverseAbstractions.Axioms.Universe.FunctorialIdentities.UniversalExtensionality
import UniverseAbstractions.Axioms.Universe.FunctorialIdentities.FunctorProperties
import UniverseAbstractions.Lemmas.DerivedFunctors
import UniverseAbstractions.Lemmas.DerivedFunctorExtensionality
import UniverseAbstractions.Lemmas.DerivedSingletonFunctors
import UniverseAbstractions.Lemmas.DerivedProductFunctors
import UniverseAbstractions.Lemmas.FunctorCategory
import UniverseAbstractions.Meta.TypedExpr
import UniverseAbstractions.Meta.Reflect
import UniverseAbstractions.Meta.Tactics.Functoriality
import UniverseAbstractions.Meta.Tactics.Extensionality
import UniverseAbstractions.Instances.Utils.Trivial
import UniverseAbstractions.Instances.Utils.Direct
import UniverseAbstractions.Instances.Utils.Bundled
import UniverseAbstractions.Instances.Unit
import UniverseAbstractions.Instances.Bool
import UniverseAbstractions.Instances.Sort
import UniverseAbstractions.Instances.FunctorUniverse
import UniverseAbstractions.Instances.CoFunctorUniverse
import UniverseAbstractions.Instances.Setoid
import UniverseAbstractions.Instances.BundledSet
import UniverseAbstractions.Instances.Algebra
import UniverseAbstractions.CategoryTheory.Meta
import UniverseAbstractions.CategoryTheory.Basic
import UniverseAbstractions.CategoryTheory.Functors
import UniverseAbstractions.CategoryTheory.NaturalTransformations
import UniverseAbstractions.CategoryTheory.MultiFunctors
import UniverseAbstractions.CategoryTheory.MultiFunctorIsomorphisms
import UniverseAbstractions.CategoryTheory.Functors.Basic
import UniverseAbstractions.CategoryTheory.Functors.Nested
import UniverseAbstractions.CategoryTheory.Functors.FunDef
import UniverseAbstractions.CategoryTheory.FunctorExtensionality
import UniverseAbstractions.CategoryTheory.Singletons
import UniverseAbstractions.CategoryTheory.Products
import UniverseAbstractions.CategoryTheory.Extensional.Meta
import UniverseAbstractions.CategoryTheory.Extensional.Basic
import UniverseAbstractions.CategoryTheory.Utils.Trivial
import UniverseAbstractions.CategoryTheory.HomUniverses.Prop
import UniverseAbstractions.CategoryTheory.HomUniverses.Type
import UniverseAbstractions.CategoryTheory.HomUniverses.Setoid
import UniverseAbstractions.CategoryTheory.Algebra.Basic