OAI/CategoryTheory/Thomason/
10982 declarations, 0 contain sorry, 0 declared as axioms; 225 files
Folders
- Chains/ 11 files, 278 declarations
- Gray/ 31 files, 1689 declarations
- Simplicial/ 58 files, 3018 declarations
- Strict/ 16 files, 565 declarations
- Transfer/ 21 files, 458 declarations
Files
- AlexanderWhitney.lean 63 declarations
- AtomFibers.lean 37 declarations
- AttachmentComparison.lean 38 declarations
- BarycentricMesh.lean 54 declarations
- BoundaryQuotients.lean 78 declarations
- BoundedCylinders.lean 70 declarations
- CoherentGluing.lean 59 declarations
- Cones.lean 93 declarations
- Construction.lean 3 imports, no declarations
- CoreCouniversality.lean 40 declarations
- Couniversality.lean 33 declarations
- CubicalGeometry.lean 60 declarations
- CubicalRecognition.lean 42 declarations
- CylinderAssociativity.lean 57 declarations
- CylinderFaces.lean 61 declarations
- CylinderInterchange.lean 35 declarations
- CylinderProfiles.lean 72 declarations
- CylinderWeights.lean 85 declarations
- Definitions.lean 110 declarations
- DimensionOne.lean 54 declarations
- DirectedPrisms.lean 64 declarations
- EdgeComparison.lean 56 declarations
- ExtensionAnodyne.lean 51 declarations
- FiberComparisons.lean 53 declarations
- FiberRecognition.lean 38 declarations
- FilteredColimits.lean 62 declarations
- FiniteAttachments.lean 30 declarations
- FiniteChains.lean 32 declarations
- FiniteGluing.lean 42 declarations
- Generators.lean 79 declarations
- Globes.lean 88 declarations
- GlobularComplexes.lean 72 declarations
- GlobularGeneration.lean 71 declarations
- GrayGenerators.lean 78 declarations
- GraySquares.lean 50 declarations
- GreatestAttachments.lean 54 declarations
- HomotopyExtension.lean 53 declarations
- HornRealization.lean 64 declarations
- IntervalAdjunction.lean 13 declarations
- IntervalCategories.lean 67 declarations
- IntervalExtension.lean 55 declarations
- KanQuillen.lean 70 declarations
- KanTowers.lean 70 declarations
- LabelledFibers.lean 78 declarations
- LayeredWhiskers.lean 25 declarations
- Linearization.lean 90 declarations
- ModelClasses.lean 47 declarations
- ModelTransfer.lean 40 declarations
- NormalizedChains.lean 64 declarations
- OrientalCounit.lean 38 declarations
- PartialPrisms.lean 63 declarations
- PartialTables.lean 56 declarations
- PastingInterchange.lean 68 declarations
- Polyhedra.lean 72 declarations
- PosetComparison.lean 61 declarations
- PosetalColimits.lean 69 declarations
- PosetalReduction.lean 42 declarations
- Presentations.lean 50 declarations
- PrismBasis.lean 30 declarations
- ProperTransfer.lean 58 declarations
- RankedAtoms.lean 47 declarations
- RankedExchange.lean 44 declarations
- RankedFaithfulness.lean 22 declarations
- RectangleComposition.lean 63 declarations
- RecursiveCylinders.lean 75 declarations
- RelativeContiguity.lean 58 declarations
- RelativeRepresentation.lean 37 declarations
- Representation.lean 16 declarations
- SieveAttachments.lean 56 declarations
- SimplexAtoms.lean 60 declarations
- SimplexBoxes.lean 76 declarations
- SimplexColimits.lean 47 declarations
- SimplexRanks.lean 43 declarations
- SimplicialApproximation.lean 67 declarations
- SkeletalCategories.lean 85 declarations
- SquareClassification.lean 36 declarations
- StandardComparison.lean 66 declarations
- StationaryCylinders.lean 43 declarations
- StrictCategories.lean 46 declarations
- SubdividedUnit.lean 59 declarations
- SubdivisionFaces.lean 83 declarations
- SubdivisionMaps.lean 78 declarations
- SubdivisionNerves.lean 76 declarations
- SubdivisionPairing.lean 59 declarations
- SubdivisionWeak.lean 87 declarations
- TopSequences.lean 42 declarations
- TwoCellComparison.lean 47 declarations
- TwoCellExchange.lean 52 declarations