Last active
April 23, 2024 12:17
-
-
Save SkySkimmer/5d9eda76b016404b82239bbe352a9c6d to your computer and use it in GitHub Desktop.
HoTT theories/ vo file sizes before / after using callback to substitute univ instances in VM (in bytes)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 90136317 total | |
| 7585417 ./Spaces/Torus/TorusEquivCircles.vo | |
| 4570944 ./Pointed/Core.vo | |
| 4353756 ./Homotopy/CayleyDickson.vo | |
| 3429253 ./Colimits/Sequential.vo | |
| 3414226 ./Spaces/Spheres.vo | |
| 3363757 ./Colimits/Colimit_Flattening.vo | |
| 3004861 ./Cubical/PathCube.vo | |
| 2570380 ./Homotopy/Syllepsis.vo | |
| 1323781 ./Algebra/Groups/FreeProduct.vo | |
| 1238239 ./WildCat/DisplayedEquiv.vo | |
| 1173863 ./Classes/implementations/natpair_integers.vo | |
| 1164920 ./Colimits/GraphQuotient.vo | |
| 1103345 ./Homotopy/Smash.vo | |
| 1076920 ./Homotopy/Wedge.vo | |
| 907364 ./WildCat/Products.vo | |
| 889045 ./Homotopy/Join/JoinAssoc.vo | |
| 880128 ./Homotopy/Join/TriJoin.vo | |
| 784200 ./Colimits/Colimit_Pushout_Flattening.vo | |
| 750565 ./Spaces/TwoSphere.vo | |
| 743685 ./Categories.vo | |
| 666311 ./Algebra/AbSES/PullbackFiberSequence.vo | |
| 655501 ./Modalities/ReflectiveSubuniverse.vo | |
| 627625 ./Homotopy/ClassifyingSpace.vo | |
| 605280 ./Colimits/Colimit_Pushout.vo | |
| 585821 ./Homotopy/ExactSequence.vo | |
| 584437 ./Modalities/Lex.vo | |
| 583492 ./Pointed/Loops.vo | |
| 550193 ./Basics/PathGroupoids.vo | |
| 544371 ./Algebra/AbSES/Core.vo | |
| 535509 ./Algebra/Groups/FreeGroup.vo | |
| 517475 ./Homotopy/BlakersMassey.vo | |
| 508965 ./Algebra/AbGroups/Abelianization.vo | |
| 502584 ./Algebra/AbSES/Pushout.vo | |
| 490853 ./Algebra/Groups/GroupCoeq.vo | |
| 478141 ./Spaces/No.vo | |
| 465995 ./Spaces/Card.vo | |
| 461229 ./Categories/Comma.vo | |
| 454757 ./Limits/Pullback.vo | |
| 433587 ./Categories/Grothendieck/ToSet/Morphisms.vo | |
| 421319 ./Colimits/Pushout.vo | |
| 411436 ./Modalities/Meet.vo | |
| 404210 ./PropResizing/Nat.vo | |
| 382090 ./Types/Sum.vo | |
| 379659 ./Types/Universe.vo | |
| 367967 ./WildCat/Equiv.vo | |
| 361088 ./Extensions.vo | |
| 360210 ./Algebra/Rings/Ideal.vo | |
| 356776 ./Homotopy/Freudenthal.vo | |
| 349921 ./Homotopy/Join/Core.vo | |
| 343356 ./Classes/theory/premetric.vo | |
| 342342 ./Categories/Category/Paths.vo | |
| 341729 ./Spaces/BAut/Bool.vo | |
| 329824 ./Colimits/Quotient.vo | |
| 329605 ./HIT/V.vo | |
| 316506 ./Classes/theory/rationals.vo | |
| 311713 ./Spaces/No/Addition.vo | |
| 310537 ./WildCat/Sum.vo | |
| 306007 ./Categories/LaxComma/CoreLaws.vo | |
| 305842 ./Spaces/Universe.vo | |
| 304635 ./Pointed/pSusp.vo | |
| 304179 ./Algebra/AbSES/Pullback.vo | |
| 303548 ./Spaces/Finite/Finite.vo | |
| 297255 ./Algebra/AbSES/SixTerm.vo | |
| 285437 ./Classes/interfaces/abstract_algebra.vo | |
| 282627 ./Spaces/No/Core.vo | |
| 275731 ./Types/Paths.vo | |
| 267824 ./WildCat/Adjoint.vo | |
| 266896 ./Sets/Hartogs.vo | |
| 266266 ./WildCat/Displayed.vo | |
| 262684 ./Pointed/pMap.vo | |
| 261615 ./Categories/Category/Sigma/Univalent.vo | |
| 261591 ./Homotopy/Suspension.vo | |
| 253013 ./Homotopy/Hopf.vo | |
| 250096 ./Homotopy/HomotopyGroup.vo | |
| 249027 ./Categories/Category.vo | |
| 248376 ./Idempotents.vo | |
| 239306 ./Algebra/Groups/GrpPullback.vo | |
| 238763 ./Homotopy/HSpace/Pointwise.vo | |
| 237151 ./Modalities/Modality.vo | |
| 234458 ./Tactics/EquivalenceInduction.vo | |
| 230934 ./Cubical/PathSquare.vo | |
| 230255 ./Colimits/Colimit.vo | |
| 218497 ./Types/Sigma.vo | |
| 217955 ./Types/IWType.vo | |
| 217893 ./Algebra/AbSES/BaerSum.vo | |
| 216542 ./Spaces/BAut.vo | |
| 211440 ./Analysis/Locator.vo | |
| 210442 ./Colimits/CoeqUnivProp.vo | |
| 207523 ./Categories/Functor/Paths.vo | |
| 206459 ./WildCat/Yoneda.vo | |
| 201591 ./Homotopy/HSpace/Moduli.vo | |
| 200186 ./Diagrams/Cocone.vo | |
| 200003 ./Algebra/Groups/Group.vo | |
| 196309 ./Sets/Ordinals.vo | |
| 196304 ./Algebra/Rings/Ring.vo | |
| 194695 ./WildCat/Core.vo | |
| 194673 ./Colimits/Coeq.vo | |
| 193728 ./Algebra/Rings/Module.vo | |
| 189638 ./Types/Prod.vo | |
| 184257 ./Modalities/Descent.vo | |
| 181659 ./Diagrams/CommutativeSquares.vo | |
| 165424 ./Algebra/AbGroups/AbPushout.vo | |
| 165027 ./HIT/Flattening.vo | |
| 164829 ./Colimits/Colimit_Sigma.vo | |
| 162227 ./Algebra/Groups/Subgroup.vo | |
| 161025 ./HFiber.vo | |
| 158377 ./Algebra/Rings/QuotientRing.vo | |
| 155888 ./Cubical/DPathCube.vo | |
| 155411 ./Homotopy/HSpaceS1.vo | |
| 155066 ./Classes/orders/semirings.vo | |
| 151005 ./Classes/theory/ua_third_isomorphism.vo | |
| 148800 ./Categories/Pseudofunctor/RewriteLaws.vo | |
| 146041 ./Diagrams/Cone.vo | |
| 140763 ./Basics/Equivalences.vo | |
| 140732 ./Algebra/Rings/ChineseRemainder.vo | |
| 138263 ./Pointed/pFiber.vo | |
| 137944 ./Colimits/MappingCylinder.vo | |
| 137487 ./Categories/Category/Morphisms.vo | |
| 136974 ./WildCat/Bifunctor.vo | |
| 132810 ./Spaces/Nat/Arithmetic.vo | |
| 132597 ./Spaces/Circle.vo | |
| 130198 ./Algebra/Groups/Presentation.vo | |
| 129113 ./Categories/InitialTerminalCategory/Pseudofunctors.vo | |
| 128792 ./Categories/Adjoint.vo | |
| 127699 ./Metatheory/UnivalenceVarieties.vo | |
| 127066 ./Algebra/Groups/QuotientGroup.vo | |
| 126709 ./Factorization.vo | |
| 125941 ./Classes/implementations/field_of_fractions.vo | |
| 125736 ./Spaces/Finite/FinSeq.vo | |
| 123993 ./Algebra/Universal/Algebra.vo | |
| 121124 ./WildCat/NatTrans.vo | |
| 120911 ./Algebra/AbSES/Ext.vo | |
| 118711 ./Categories/Adjoint/Pointwise.vo | |
| 117187 ./Classes/interfaces/canonical_names.vo | |
| 115723 ./Homotopy/Cover.vo | |
| 115472 ./Spaces/Int/Spec.vo | |
| 114386 ./Classes/implementations/binary_naturals.vo | |
| 113661 ./WildCat/FunctorCat.vo | |
| 112571 ./ObjectClassifier.vo | |
| 112559 ./Categories/Comma/Core.vo | |
| 111802 ./Algebra/Rings/CRing.vo | |
| 111374 ./Algebra/AbGroups/AbelianGroup.vo | |
| 111256 ./Categories/Pseudofunctor.vo | |
| 110589 ./Homotopy/SuccessorStructure.vo | |
| 110291 ./Classes/interfaces/orders.vo | |
| 107570 ./Algebra/AbGroups/Biproduct.vo | |
| 106092 ./Basics/Tactics.vo | |
| 105429 ./WildCat/TwoOneCat.vo | |
| 104883 ./Classes/theory/rings.vo | |
| 104493 ./Categories/Adjoint/HomCoercions.vo | |
| 104253 ./Cubical/DPath.vo | |
| 103778 ./Spaces/BAut/Cantor.vo | |
| 103205 ./Algebra/ooGroup.vo | |
| 101864 ./Categories/Adjoint/Functorial/Laws.vo | |
| 100842 ./Types/Forall.vo | |
| 99659 ./Diagrams/Diagram.vo | |
| 98115 ./Spaces/Nat/Core.vo | |
| 96747 ./Classes/tactics/ring_quote.vo | |
| 95819 ./WildCat/Square.vo | |
| 95755 ./Spaces/Finite/Fin.vo | |
| 94508 ./Colimits/Colimit_Coequalizer.vo | |
| 93106 ./Classes/implementations/peano_naturals.vo | |
| 90491 ./Classes/theory/ua_second_isomorphism.vo | |
| 90187 ./Categories/Comma/Functorial.vo | |
| 90075 ./HIT/quotient.vo | |
| 88420 ./WildCat/Prod.vo | |
| 85871 ./Categories/LaxComma/CoreParts.vo | |
| 85464 ./Categories/Functor.vo | |
| 85130 ./Classes/theory/ua_quotient_algebra.vo | |
| 84668 ./Spaces/List/Theory.vo | |
| 84084 ./Categories/LaxComma/Core.vo | |
| 82226 ./Categories/Category/Sigma.vo | |
| 81864 ./Algebra/Universal/TermAlgebra.vo | |
| 80512 ./Basics/Overture.vo | |
| 80460 ./Modalities/Localization.vo | |
| 79333 ./WildCat/Coproducts.vo | |
| 77294 ./Cubical/DPathSquare.vo | |
| 76951 ./Classes/orders/orders.vo | |
| 75662 ./Pointed/pTrunc.vo | |
| 75144 ./Algebra/Rings/Z.vo | |
| 73411 ./Classes/tactics/ring_pol.vo | |
| 72776 ./Homotopy/WhiteheadsPrinciple.vo | |
| 70947 ./Categories/Structure.vo | |
| 70157 ./Classes/orders/lattices.vo | |
| 67719 ./Classes/orders/rings.vo | |
| 65882 ./Categories/ExponentialLaws/Law2/Law.vo | |
| 65774 ./Basics/Trunc.vo | |
| 65718 ./Classes/theory/ua_homomorphism.vo | |
| 65428 ./Categories/Comma/ProjectionFunctors.vo | |
| 64723 ./Modalities/Topological.vo | |
| 64591 ./Classes/theory/ua_first_isomorphism.vo | |
| 64084 ./Types/Equiv.vo | |
| 63974 ./Tactics.vo | |
| 63826 ./WildCat/EquivGpd.vo | |
| 63198 ./DProp.vo | |
| 63068 ./Classes/theory/naturals.vo | |
| 62170 ./Projective.vo | |
| 61789 ./Categories/PseudonaturalTransformation/Core.vo | |
| 61429 ./Homotopy/Join/JoinSusp.vo | |
| 60225 ./Categories/NaturalTransformation.vo | |
| 60223 ./Colimits/Quotient/Choice.vo | |
| 60129 ./Truncations/Connectedness.vo | |
| 59993 ./Classes/theory/fields.vo | |
| 59869 ./WildCat/Universe.vo | |
| 59649 ./Modalities/Separated.vo | |
| 58957 ./WildCat/ZeroGroupoid.vo | |
| 58877 ./Pointed/pSect.vo | |
| 58549 ./HIT/epi.vo | |
| 58185 ./Spaces/BAut/Rigid.vo | |
| 57935 ./Types/Arrow.vo | |
| 57748 ./Classes/interfaces/ua_algebra.vo | |
| 57722 ./Classes/theory/integers.vo | |
| 57074 ./Categories/Adjoint/UnitCounitCoercions.vo | |
| 56588 ./Categories/Structure/IdentityPrinciple.vo | |
| 56540 ./Sets/GCHtoAC.vo | |
| 56173 ./Limits/Limit.vo | |
| 56005 ./EquivGroupoids.vo | |
| 55943 ./WildCat/PointedCat.vo | |
| 55454 ./Classes/orders/nat_int.vo | |
| 54683 ./Classes/theory/int_abs.vo | |
| 53970 ./Algebra/Universal/Operation.vo | |
| 53907 ./Spaces/Torus/Torus.vo | |
| 53656 ./Basics/Notations.vo | |
| 53483 ./Algebra/AbGroups/AbHom.vo | |
| 53215 ./Categories/UniversalProperties.vo | |
| 53005 ./Categories/Comma/InducedFunctors.vo | |
| 52811 ./Homotopy/HSpace/Core.vo | |
| 52809 ./Categories/Grothendieck/PseudofunctorToCat.vo | |
| 52748 ./Pointed/pEquiv.vo | |
| 52244 ./Classes/orders/maps.vo | |
| 51765 ./Algebra/AbSES/DirectSum.vo | |
| 51628 ./Categories/ExponentialLaws/Law4/Law.vo | |
| 51103 ./Modalities/Fracture.vo | |
| 50824 ./Modalities/Accessible.vo | |
| 50608 ./Homotopy/Bouquet.vo | |
| 49708 ./Truncations/Core.vo | |
| 49107 ./Classes/interfaces/cauchy.vo | |
| 48849 ./Algebra/Universal/Homomorphism.vo | |
| 47119 ./Algebra/Groups/Lagrange.vo | |
| 47087 ./Categories/ExponentialLaws/Law3/Law.vo | |
| 46753 ./Spaces/Finite/FinNat.vo | |
| 46450 ./Algebra/AbGroups/Centralizer.vo | |
| 46253 ./Classes/theory/dec_fields.vo | |
| 46116 ./Classes/theory/groups.vo | |
| 45386 ./Homotopy/EMSpace.vo | |
| 45370 ./Categories/ExponentialLaws/Law4/Functors.vo | |
| 45334 ./Categories/Yoneda.vo | |
| 44724 ./Categories/Functor/Attributes.vo | |
| 44580 ./WildCat/Monoidal.vo | |
| 44396 ./Tactics/RewriteModuloAssociativity.vo | |
| 43778 ./Categories/NaturalTransformation/Isomorphisms.vo | |
| 43448 ./Categories/Functor/Pointwise/Properties.vo | |
| 42671 ./Spaces/Pos/Core.vo | |
| 42522 ./Spaces/Int/LoopExp.vo | |
| 42512 ./Categories/Functor/Sum.vo | |
| 42493 ./Classes/theory/lattices.vo | |
| 41271 ./Spaces/Finite/FinInduction.vo | |
| 40986 ./Classes/theory/ua_isomorphic.vo | |
| 40844 ./Categories/Adjoint/Composition/AssociativityLaw.vo | |
| 40709 ./TruncType.vo | |
| 40555 ./Categories/Monoidal/MonoidalCategory.vo | |
| 40442 ./Algebra/Groups/Image.vo | |
| 40169 ./Equiv/PathSplit.vo | |
| 40014 ./Categories/Adjoint/Composition/IdentityLaws.vo | |
| 39638 ./Categories/ProductLaws.vo | |
| 38664 ./Categories/Grothendieck/ToSet.vo | |
| 38275 ./Modalities/CoreflectiveSubuniverse.vo | |
| 38022 ./Algebra/AbGroups/AbPullback.vo | |
| 37909 ./Classes/theory/ua_subalgebra.vo | |
| 37863 ./WildCat/Opposite.vo | |
| 37470 ./Categories/NaturalTransformation/Composition/Laws.vo | |
| 37449 ./Homotopy/PinSn.vo | |
| 37417 ./Types/Bool.vo | |
| 37311 ./Categories/PseudonaturalTransformation.vo | |
| 37260 ./Classes/theory/apartness.vo | |
| 37105 ./Spaces/No/Negation.vo | |
| 36899 ./HoTT.vo | |
| 36641 ./Categories/Pseudofunctor/FromFunctor.vo | |
| 36419 ./Homotopy/HSpace/Coherent.vo | |
| 36057 ./Categories/Pseudofunctor/Identity.vo | |
| 36028 ./Classes/theory/nat_distance.vo | |
| 36002 ./Categories/Functor/Composition/Laws.vo | |
| 35805 ./Categories/Functor/Prod/Universal.vo | |
| 35397 ./Categories/NaturalTransformation/Composition/Core.vo | |
| 35158 ./HSet.vo | |
| 35071 ./Classes/theory/ua_prod_algebra.vo | |
| 35017 ./Categories/Structure/Core.vo | |
| 34641 ./Algebra/Groups/Kernel.vo | |
| 34590 ./Algebra/Groups/ShortExactSequence.vo | |
| 34421 ./WildCat/Paths.vo | |
| 34062 ./Categories/ExponentialLaws/Law4.vo | |
| 33936 ./Modalities/Closed.vo | |
| 33851 ./Constant.vo | |
| 33809 ./Categories/FunctorCategory/Morphisms.vo | |
| 33413 ./Classes/implementations/bool.vo | |
| 33130 ./Categories/Functor/Composition.vo | |
| 33123 ./Classes/tactics/ring_tac.vo | |
| 32730 ./Categories/HomotopyPreCategory.vo | |
| 32403 ./Categories/SetCategory/Morphisms.vo | |
| 32323 ./Classes/isomorphisms/rings.vo | |
| 32281 ./Categories/Pseudofunctor/Core.vo | |
| 31711 ./Categories/Adjoint/UniversalMorphisms/Core.vo | |
| 31306 ./Categories/Category/Sum.vo | |
| 31247 ./Categories/Adjoint/Composition/Core.vo | |
| 31103 ./Classes/orders/naturals.vo | |
| 30867 ./Types/WType.vo | |
| 30847 ./Classes/implementations/pointwise.vo | |
| 30792 ./Categories/Category/Sigma/OnMorphisms.vo | |
| 30454 ./Spaces/Torus/TorusHomotopy.vo | |
| 30262 ./Algebra/AbGroups/Cyclic.vo | |
| 30007 ./Categories/Limits/Core.vo | |
| 29820 ./Categories/Functor/Pointwise.vo | |
| 29748 ./Categories/SemiSimplicialSets.vo | |
| 29199 ./Basics/Decidable.vo | |
| 29145 ./Pointed/pModality.vo | |
| 29055 ./Spaces/Pos/Spec.vo | |
| 28918 ./Modalities/Open.vo | |
| 28717 ./Classes/interfaces/integers.vo | |
| 28595 ./Categories/LaxComma.vo | |
| 28384 ./Spaces/List/Paths.vo | |
| 28382 ./Categories/NaturalTransformation/Paths.vo | |
| 27931 ./Categories/InitialTerminalCategory/Functors.vo | |
| 27617 ./Classes/implementations/hprop_lattice.vo | |
| 27333 ./Categories/Grothendieck/ToSet/Univalent.vo | |
| 26885 ./Classes/interfaces/ua_congruence.vo | |
| 26855 ./Categories/Functor/Prod.vo | |
| 26518 ./Algebra/Universal/Congruence.vo | |
| 26379 ./Categories/ExponentialLaws/Law0.vo | |
| 26311 ./Categories/ExponentialLaws/Law1/Law.vo | |
| 26310 ./Spaces/Int/Core.vo | |
| 26082 ./Classes/categories/ua_category.vo | |
| 26041 ./Basics/Hexadecimal.vo | |
| 25888 ./Diagrams/ConstantDiagram.vo | |
| 25763 ./Sets/GCH.vo | |
| 25471 ./Classes/orders/integers.vo | |
| 25471 ./Classes/implementations/ne_list.vo | |
| 25140 ./Metatheory/FunextVarieties.vo | |
| 25029 ./Categories/Grothendieck/ToSet/Core.vo | |
| 24987 ./Categories/Adjoint/Functorial/Parts.vo | |
| 24956 ./Classes/orders/fields.vo | |
| 24876 ./Categories/Limits.vo | |
| 24849 ./Categories/Adjoint/Functorial/Core.vo | |
| 24358 ./Categories/FunctorCategory.vo | |
| 24308 ./HIT/FreeIntQuotient.vo | |
| 24191 ./Classes/orders/dec_fields.vo | |
| 24135 ./BoundedSearch.vo | |
| 23757 ./Sets/AC.vo | |
| 23748 ./Categories/ExponentialLaws/Law1/Functors.vo | |
| 23622 ./Categories/Adjoint/UnitCounit.vo | |
| 23449 ./Spaces/BAut/Bool/IncoherentIdempotent.vo | |
| 23190 ./Categories/NaturalTransformation/Composition.vo | |
| 23016 ./Categories/ExponentialLaws/Law2.vo | |
| 23000 ./Classes/interfaces/rationals.vo | |
| 22572 ./HProp.vo | |
| 22570 ./Categories/Functor/Pointwise/Core.vo | |
| 22000 ./Spectra/Spectrum.vo | |
| 21709 ./Categories/Functor/Composition/Functorial/Attributes.vo | |
| 21707 ./Classes/interfaces/naturals.vo | |
| 21701 ./Categories/Adjoint/Composition.vo | |
| 21664 ./Algebra/AbGroups/AbProjective.vo | |
| 21534 ./Basics/Decimal.vo | |
| 21473 ./Categories/ExponentialLaws/Tactics.vo | |
| 21173 ./Categories/NaturalTransformation/Identity.vo | |
| 21133 ./Categories/Adjoint/Paths.vo | |
| 20895 ./Categories/Functor/Composition/Functorial/Core.vo | |
| 20703 ./Categories/NaturalTransformation/Core.vo | |
| 20669 ./Categories/Functor/Composition/Functorial.vo | |
| 20459 ./Homotopy/EncodeDecode.vo | |
| 20281 ./Categories/CategoryOfSections/Core.vo | |
| 20153 ./Modalities/Nullification.vo | |
| 19779 ./Categories/DualFunctor.vo | |
| 19447 ./Basics/Contractible.vo | |
| 19370 ./Categories/Adjoint/UniversalMorphisms.vo | |
| 19102 ./Categories/Category/Core.vo | |
| 18986 ./Categories/SetCategory.vo | |
| 18546 ./Categories/KanExtensions.vo | |
| 18321 ./Spaces/List/Core.vo | |
| 18278 ./Equiv/Relational.vo | |
| 18042 ./Metatheory/PropTrunc.vo | |
| 17824 ./Categories/ExponentialLaws/Law1.vo | |
| 17754 ./Classes/orders/sum.vo | |
| 17719 ./Algebra/AbGroups/Z.vo | |
| 17712 ./Categories/Utf8.vo | |
| 17704 ./Categories/Functor/Prod/Core.vo | |
| 17626 ./Utf8.vo | |
| 17519 ./Categories/CategoryOfSections.vo | |
| 17228 ./Categories/Adjoint/Composition/LawsTactic.vo | |
| 16971 ./Classes/theory/additional_operations.vo | |
| 16952 ./Categories/InitialTerminalCategory/NaturalTransformations.vo | |
| 16879 ./Categories/ExponentialLaws/Law2/Functors.vo | |
| 16730 ./Algebra/ooAction.vo | |
| 16650 ./Categories/Notations.vo | |
| 16575 ./Algebra/Aut.vo | |
| 16340 ./HIT/Interval.vo | |
| 16289 ./PathAny.vo | |
| 16274 ./Algebra/AbSES.vo | |
| 16083 ./Categories/NaturalTransformation/Pointwise.vo | |
| 15929 ./Algebra/Rings.vo | |
| 15822 ./WildCat/Induced.vo | |
| 15807 ./Metatheory/UnivalenceImpliesFunext.vo | |
| 15740 ./Classes/implementations/assume_rationals.vo | |
| 15685 ./Categories/Category/Sigma/Core.vo | |
| 15643 ./Classes/orders/archimedean.vo | |
| 15641 ./Categories/Limits/Functors.vo | |
| 15617 ./Categories/ExponentialLaws/Law3/Functors.vo | |
| 15596 ./Types/Unit.vo | |
| 15596 ./Categories/KanExtensions/Functors.vo | |
| 15474 ./Classes/interfaces/ua_setalgebra.vo | |
| 15330 ./Diagrams/ParallelPair.vo | |
| 15311 ./Sets/Powers.vo | |
| 15251 ./Categories/Category/Sigma/OnObjects.vo | |
| 15179 ./Algebra/AbGroups.vo | |
| 15125 ./Categories/ChainCategory.vo | |
| 14989 ./Categories/NaturalTransformation/Prod.vo | |
| 14774 ./Categories/LaxComma/Notations.vo | |
| 14731 ./Categories/FundamentalPreGroupoidCategory.vo | |
| 14436 ./Categories/KanExtensions/Core.vo | |
| 14385 ./Categories/NaturalTransformation/Utf8.vo | |
| 14208 ./Classes/interfaces/archimedean.vo | |
| 14177 ./Categories/Functor/Prod/Functorial.vo | |
| 14161 ./Categories/Adjoint/Hom.vo | |
| 14010 ./Spaces/Nat/Paths.vo | |
| 13971 ./Categories/ExponentialLaws/Law3.vo | |
| 13942 ./Categories/Functor/Utf8.vo | |
| 13913 ./Categories/FunctorCategory/Utf8.vo | |
| 13910 ./WildCat/Sigma.vo | |
| 13884 ./WildCat/EmptyCat.vo | |
| 13532 ./Algebra/Groups.vo | |
| 13495 ./Truncations/SeparatedTrunc.vo | |
| 13342 ./Categories/HomFunctor.vo | |
| 13303 ./Categories/GroupoidCategory/Core.vo | |
| 13297 ./Categories/Category/Prod.vo | |
| 13220 ./Categories/Comma/Projection.vo | |
| 13150 ./Categories/SimplicialSets.vo | |
| 13145 ./Diagrams/DDiagram.vo | |
| 13077 ./Colimits/SpanPushout.vo | |
| 13027 ./Categories/InitialTerminalCategory/Core.vo | |
| 13014 ./Homotopy/EvaluationFibration.vo | |
| 12866 ./NullHomotopy.vo | |
| 12497 ./Basics/Nat.vo | |
| 12359 ./Functorish.vo | |
| 12217 ./Categories/Category/Objects.vo | |
| 12185 ./Categories/Cat.vo | |
| 12135 ./Categories/FunctorCategory/Functorial.vo | |
| 12063 ./Categories/IndiscreteCategory.vo | |
| 11970 ./HIT/surjective_factor.vo | |
| 11959 ./Categories/Functor/Notations.vo | |
| 11901 ./Categories/Functor/Core.vo | |
| 11826 ./Diagrams/Sequence.vo | |
| 11744 ./Categories/Cat/Core.vo | |
| 11545 ./WildCat/Forall.vo | |
| 11401 ./Classes/interfaces/monad.vo | |
| 11350 ./Categories/InitialTerminalCategory.vo | |
| 11336 ./Categories/GroupoidCategory.vo | |
| 11280 ./Homotopy/Join.vo | |
| 10834 ./Categories/LaxComma/Utf8.vo | |
| 10820 ./Colimits/Colimit_Prod.vo | |
| 10816 ./PropResizing/ImpredicativeTruncation.vo | |
| 10801 ./Categories/NaturalTransformation/Sum.vo | |
| 10787 ./Spaces/Cantor.vo | |
| 10725 ./HIT/iso.vo | |
| 10647 ./Classes/implementations/family_prod.vo | |
| 10577 ./Equiv/BiInv.vo | |
| 10537 ./Spaces/Int/Equiv.vo | |
| 10507 ./Homotopy/HSpace.vo | |
| 10475 ./Metatheory/TruncImpliesFunext.vo | |
| 10464 ./Classes/interfaces/round.vo | |
| 10413 ./Diagrams/Span.vo | |
| 10371 ./Categories/GroupoidCategory/Morphisms.vo | |
| 9993 ./Categories/NatCategory.vo | |
| 9898 ./Categories/SetCategory/Functors/SetProp.vo | |
| 9882 ./Categories/Cat/Morphisms.vo | |
| 9859 ./Categories/Comma/Dual.vo | |
| 9819 ./Pointed.vo | |
| 9629 ./HIT/unique_choice.vo | |
| 9545 ./Categories/Grothendieck/ToCat.vo | |
| 9478 ./Modalities/Notnot.vo | |
| 9372 ./Categories/DependentProduct.vo | |
| 9356 ./Categories/NaturalTransformation/Composition/Functorial.vo | |
| 9135 ./Basics/Utf8.vo | |
| 9034 ./Categories/ExponentialLaws.vo | |
| 8956 ./Categories/FunctorCategory/Dual.vo | |
| 8911 ./Categories/Category/Pi.vo | |
| 8908 ./Categories/Profunctor.vo | |
| 8837 ./Algebra/Congruence.vo | |
| 8628 ./ExcludedMiddle.vo | |
| 8481 ./Categories/GroupoidCategory/Dual.vo | |
| 8458 ./Categories/Profunctor/Representable.vo | |
| 8438 ./Categories/FunctorCategory/Core.vo | |
| 8417 ./Types/Empty.vo | |
| 8414 ./Categories/Functor/Composition/Core.vo | |
| 8396 ./Modalities/Identity.vo | |
| 8320 ./Categories/Category/Utf8.vo | |
| 8252 ./HIT/SetCone.vo | |
| 8190 ./Categories/Category/Univalent.vo | |
| 7951 ./Basics/Datatypes.vo | |
| 7903 ./Categories/Grothendieck.vo | |
| 7898 ./Limits/Equalizer.vo | |
| 7889 ./Tactics/BinderApply.vo | |
| 7776 ./Categories/Adjoint/Utf8.vo | |
| 7626 ./Categories/SetCategory/Core.vo | |
| 7447 ./Categories/Adjoint/Dual.vo | |
| 7409 ./Categories/CategoryOfGroupoids.vo | |
| 7236 ./Categories/SetCategory/Functors.vo | |
| 7234 ./Spaces/Finite.vo | |
| 7051 ./Categories/NaturalTransformation/Notations.vo | |
| 6903 ./Categories/Adjoint/Notations.vo | |
| 6694 ./Basics/Numeral.vo | |
| 6517 ./Categories/Category/Dual.vo | |
| 6469 ./Categories/InitialTerminalCategory/Notations.vo | |
| 6454 ./Categories/Adjoint/Functorial.vo | |
| 6377 ./Categories/Comma/Utf8.vo | |
| 6181 ./Categories/Adjoint/Identity.vo | |
| 6156 ./Categories/Profunctor/Core.vo | |
| 6016 ./Truncations.vo | |
| 6001 ./Categories/Category/Notations.vo | |
| 5997 ./Categories/Profunctor/Identity.vo | |
| 5853 ./Categories/NaturalTransformation/Dual.vo | |
| 5848 ./WildCat.vo | |
| 5842 ./Spaces/Nat.vo | |
| 5669 ./Tactics/EvalIn.vo | |
| 5387 ./Categories/Functor/Dual.vo | |
| 5365 ./Categories/Profunctor/Utf8.vo | |
| 5286 ./Categories/FunctorCategory/Notations.vo | |
| 5074 ./Categories/Profunctor/Notations.vo | |
| 5071 ./Metatheory/Core.vo | |
| 4958 ./Categories/Comma/Notations.vo | |
| 4882 ./WildCat/UnitCat.vo | |
| 4881 ./Metatheory/IntervalImpliesFunext.vo | |
| 4654 ./Categories/Category/Subcategory.vo | |
| 4591 ./Spaces/Finite/Tactics.vo | |
| 4574 ./Categories/Category/Subcategory/Full.vo | |
| 4381 ./Categories/Adjoint/Core.vo | |
| 4306 ./Categories/DiscreteCategory.vo | |
| 4302 ./Categories/Structure/Utf8.vo | |
| 4196 ./Categories/Category/Subcategory/Wide.vo | |
| 4171 ./Categories/Category/Strict.vo | |
| 3906 ./PropResizing/PropResizing.vo | |
| 3680 ./Basics/Logic.vo | |
| 3419 ./Spaces/Int.vo | |
| 3384 ./Categories/Structure/Notations.vo | |
| 3294 ./Types.vo | |
| 3151 ./Diagrams/Graph.vo | |
| 2972 ./Axioms/Univalence.vo | |
| 2950 ./Cubical.vo | |
| 2935 ./Utf8Minimal.vo | |
| 2923 ./Misc.vo | |
| 2533 ./Categories/Functor/Identity.vo | |
| 2178 ./Spaces/Pos.vo | |
| 2155 ./Basics.vo | |
| 1897 ./Tactics/Nameless.vo | |
| 1412 ./Axioms/Funext.vo |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 141343499 total | |
| 17326771 ./Spaces/Torus/TorusEquivCircles.vo | |
| 8674223 ./Colimits/Colimit_Flattening.vo | |
| 8415300 ./Homotopy/CayleyDickson.vo | |
| 6677664 ./Pointed/Core.vo | |
| 6005350 ./Colimits/Sequential.vo | |
| 5920301 ./Spaces/Spheres.vo | |
| 3028206 ./Cubical/PathCube.vo | |
| 2573706 ./Homotopy/Syllepsis.vo | |
| 2310567 ./Algebra/Groups/FreeProduct.vo | |
| 2046239 ./Colimits/GraphQuotient.vo | |
| 2036877 ./WildCat/DisplayedEquiv.vo | |
| 2017052 ./Homotopy/Join/JoinAssoc.vo | |
| 1678966 ./Homotopy/Smash.vo | |
| 1539563 ./Colimits/Colimit_Pushout.vo | |
| 1427854 ./WildCat/Products.vo | |
| 1339824 ./Homotopy/Join/TriJoin.vo | |
| 1255264 ./Colimits/Colimit_Pushout_Flattening.vo | |
| 1183611 ./Classes/implementations/natpair_integers.vo | |
| 1180263 ./Spaces/No/Addition.vo | |
| 1167725 ./Homotopy/ClassifyingSpace.vo | |
| 1147650 ./Homotopy/Wedge.vo | |
| 1127466 ./Algebra/AbSES/PullbackFiberSequence.vo | |
| 1104211 ./Spaces/TwoSphere.vo | |
| 1006840 ./Modalities/Lex.vo | |
| 905422 ./Algebra/Groups/FreeGroup.vo | |
| 901137 ./Pointed/Loops.vo | |
| 893611 ./Homotopy/BlakersMassey.vo | |
| 867663 ./Modalities/ReflectiveSubuniverse.vo | |
| 862277 ./Homotopy/ExactSequence.vo | |
| 786195 ./Algebra/Groups/GroupCoeq.vo | |
| 768510 ./Spaces/BAut/Bool.vo | |
| 754929 ./Algebra/AbSES/Pushout.vo | |
| 742924 ./Algebra/AbSES/Core.vo | |
| 737324 ./Categories.vo | |
| 727438 ./Algebra/AbGroups/Abelianization.vo | |
| 717102 ./Modalities/Meet.vo | |
| 693545 ./PropResizing/Nat.vo | |
| 679353 ./Spaces/Card.vo | |
| 678488 ./Colimits/Pushout.vo | |
| 646614 ./Homotopy/Freudenthal.vo | |
| 631371 ./Algebra/Rings/ChineseRemainder.vo | |
| 605739 ./Limits/Pullback.vo | |
| 604827 ./Types/Universe.vo | |
| 601976 ./Sets/Hartogs.vo | |
| 586740 ./Basics/PathGroupoids.vo | |
| 583691 ./Categories/Grothendieck/ToSet/Morphisms.vo | |
| 570091 ./Homotopy/Join/Core.vo | |
| 548328 ./Colimits/Quotient.vo | |
| 536209 ./Extensions.vo | |
| 535739 ./WildCat/Sum.vo | |
| 531353 ./WildCat/Equiv.vo | |
| 530106 ./Types/Sum.vo | |
| 524621 ./Spaces/Universe.vo | |
| 507695 ./Pointed/pSusp.vo | |
| 507158 ./Algebra/AbSES/SixTerm.vo | |
| 500664 ./Algebra/Rings/Ideal.vo | |
| 481384 ./Spaces/Finite/Finite.vo | |
| 479545 ./HIT/V.vo | |
| 475192 ./Spaces/No.vo | |
| 456276 ./Algebra/AbSES/Pullback.vo | |
| 455571 ./Categories/Comma.vo | |
| 454544 ./Spaces/Finite/FinSeq.vo | |
| 428008 ./WildCat/Adjoint.vo | |
| 423570 ./Homotopy/Hopf.vo | |
| 412434 ./Homotopy/Suspension.vo | |
| 407843 ./Categories/Category/Paths.vo | |
| 391216 ./Pointed/pMap.vo | |
| 377351 ./Homotopy/HSpace/Pointwise.vo | |
| 375744 ./Homotopy/HomotopyGroup.vo | |
| 374760 ./Colimits/Colimit.vo | |
| 361460 ./Tactics/EquivalenceInduction.vo | |
| 348469 ./Algebra/AbSES/BaerSum.vo | |
| 345101 ./Classes/theory/premetric.vo | |
| 339134 ./Spaces/No/Core.vo | |
| 335100 ./Spaces/BAut.vo | |
| 332913 ./WildCat/Yoneda.vo | |
| 325338 ./Categories/LaxComma/CoreLaws.vo | |
| 322003 ./Classes/theory/rationals.vo | |
| 321856 ./Categories/Category/Sigma/Univalent.vo | |
| 318361 ./Classes/interfaces/abstract_algebra.vo | |
| 316138 ./Algebra/Groups/GrpPullback.vo | |
| 314903 ./Colimits/CoeqUnivProp.vo | |
| 310242 ./Modalities/Modality.vo | |
| 297374 ./Idempotents.vo | |
| 296442 ./Categories/Functor/Paths.vo | |
| 291918 ./Types/IWType.vo | |
| 291543 ./Types/Paths.vo | |
| 286043 ./WildCat/Displayed.vo | |
| 277313 ./Categories/InitialTerminalCategory/Pseudofunctors.vo | |
| 268218 ./Algebra/Rings/QuotientRing.vo | |
| 266235 ./Homotopy/HSpace/Moduli.vo | |
| 265302 ./Types/Sigma.vo | |
| 263363 ./Algebra/Rings/Module.vo | |
| 259262 ./Algebra/Rings/Ring.vo | |
| 256227 ./Cubical/PathSquare.vo | |
| 255771 ./Algebra/AbGroups/AbPushout.vo | |
| 251902 ./Diagrams/Cocone.vo | |
| 250299 ./Homotopy/HSpaceS1.vo | |
| 249061 ./Categories/Pseudofunctor/RewriteLaws.vo | |
| 245853 ./Categories/Category.vo | |
| 241890 ./HIT/Flattening.vo | |
| 239593 ./Modalities/Descent.vo | |
| 239170 ./Sets/Ordinals.vo | |
| 239063 ./Types/Prod.vo | |
| 237643 ./Analysis/Locator.vo | |
| 237360 ./Algebra/Groups/Group.vo | |
| 236530 ./Classes/theory/ua_third_isomorphism.vo | |
| 236170 ./Colimits/Coeq.vo | |
| 231146 ./Colimits/MappingCylinder.vo | |
| 226473 ./Diagrams/CommutativeSquares.vo | |
| 220429 ./Colimits/Colimit_Sigma.vo | |
| 220075 ./Spaces/Circle.vo | |
| 217028 ./Categories/Adjoint/HomCoercions.vo | |
| 216708 ./Spaces/BAut/Cantor.vo | |
| 208634 ./HFiber.vo | |
| 205336 ./Algebra/Universal/Algebra.vo | |
| 204363 ./WildCat/Core.vo | |
| 204034 ./Algebra/Groups/Presentation.vo | |
| 200011 ./Pointed/pFiber.vo | |
| 199425 ./Algebra/Groups/Subgroup.vo | |
| 187306 ./Categories/Adjoint/Functorial/Laws.vo | |
| 184190 ./Diagrams/Cone.vo | |
| 182995 ./Categories/Adjoint/Pointwise.vo | |
| 181779 ./Metatheory/UnivalenceVarieties.vo | |
| 179344 ./Algebra/AbSES/Ext.vo | |
| 173812 ./Algebra/Groups/QuotientGroup.vo | |
| 168488 ./Algebra/Rings/CRing.vo | |
| 165060 ./Cubical/DPathCube.vo | |
| 161786 ./Homotopy/Cover.vo | |
| 159829 ./Basics/Equivalences.vo | |
| 155244 ./Classes/orders/semirings.vo | |
| 154655 ./WildCat/Bifunctor.vo | |
| 151403 ./ObjectClassifier.vo | |
| 148976 ./Factorization.vo | |
| 148954 ./Colimits/Colimit_Coequalizer.vo | |
| 148818 ./Algebra/AbGroups/Biproduct.vo | |
| 143510 ./WildCat/NatTrans.vo | |
| 139922 ./WildCat/FunctorCat.vo | |
| 139628 ./Categories/Category/Morphisms.vo | |
| 137176 ./Algebra/AbGroups/AbelianGroup.vo | |
| 132973 ./Spaces/Nat/Arithmetic.vo | |
| 128141 ./Classes/implementations/field_of_fractions.vo | |
| 123921 ./Algebra/ooGroup.vo | |
| 123376 ./Homotopy/SuccessorStructure.vo | |
| 123064 ./Classes/theory/ua_second_isomorphism.vo | |
| 122145 ./Categories/Adjoint.vo | |
| 121869 ./Types/Forall.vo | |
| 120775 ./WildCat/TwoOneCat.vo | |
| 119799 ./Classes/interfaces/canonical_names.vo | |
| 119198 ./Categories/Comma/Core.vo | |
| 119005 ./Cubical/DPath.vo | |
| 117649 ./Diagrams/Diagram.vo | |
| 117592 ./Classes/implementations/binary_naturals.vo | |
| 115880 ./HIT/quotient.vo | |
| 115472 ./Spaces/Int/Spec.vo | |
| 113428 ./Classes/theory/ua_quotient_algebra.vo | |
| 112844 ./WildCat/Square.vo | |
| 111212 ./Homotopy/Join/JoinSusp.vo | |
| 110650 ./Categories/Comma/Functorial.vo | |
| 110400 ./Classes/interfaces/orders.vo | |
| 107469 ./Classes/theory/rings.vo | |
| 106759 ./Categories/Pseudofunctor.vo | |
| 106092 ./Basics/Tactics.vo | |
| 102864 ./Categories/LaxComma/CoreParts.vo | |
| 101620 ./Categories/LaxComma/Core.vo | |
| 100943 ./Algebra/Groups/Lagrange.vo | |
| 100316 ./WildCat/Prod.vo | |
| 100207 ./Pointed/pTrunc.vo | |
| 99822 ./Homotopy/WhiteheadsPrinciple.vo | |
| 99052 ./Classes/tactics/ring_quote.vo | |
| 98502 ./Spaces/Nat/Core.vo | |
| 97078 ./Categories/Comma/ProjectionFunctors.vo | |
| 96506 ./Categories/SemiSimplicialSets.vo | |
| 96140 ./Spaces/Finite/Fin.vo | |
| 95495 ./Classes/implementations/peano_naturals.vo | |
| 94035 ./WildCat/Coproducts.vo | |
| 92855 ./Algebra/Universal/TermAlgebra.vo | |
| 90983 ./Modalities/Localization.vo | |
| 90878 ./Spaces/List/Theory.vo | |
| 89770 ./WildCat/ZeroGroupoid.vo | |
| 89652 ./Pointed/pSect.vo | |
| 86421 ./Modalities/Topological.vo | |
| 86415 ./Cubical/DPathSquare.vo | |
| 84320 ./Spaces/BAut/Rigid.vo | |
| 83672 ./Limits/Limit.vo | |
| 83524 ./Pointed/pEquiv.vo | |
| 83234 ./Spaces/Torus/Torus.vo | |
| 82780 ./Categories/Functor.vo | |
| 82660 ./Homotopy/Bouquet.vo | |
| 82261 ./Basics/Overture.vo | |
| 81992 ./Categories/Structure/IdentityPrinciple.vo | |
| 81185 ./Algebra/Rings/Z.vo | |
| 80424 ./Categories/Category/Sigma.vo | |
| 80308 ./Classes/orders/orders.vo | |
| 80016 ./Projective.vo | |
| 79701 ./Types/Equiv.vo | |
| 78681 ./EquivGroupoids.vo | |
| 76585 ./DProp.vo | |
| 76231 ./Categories/ExponentialLaws/Law2/Law.vo | |
| 76015 ./Classes/interfaces/ua_algebra.vo | |
| 75573 ./Classes/tactics/ring_pol.vo | |
| 75039 ./Classes/theory/ua_first_isomorphism.vo | |
| 72521 ./Modalities/Separated.vo | |
| 72426 ./WildCat/EquivGpd.vo | |
| 72259 ./Truncations/Connectedness.vo | |
| 72164 ./Classes/theory/ua_homomorphism.vo | |
| 70157 ./Classes/orders/lattices.vo | |
| 69988 ./HIT/epi.vo | |
| 69956 ./Categories/Structure.vo | |
| 69599 ./Algebra/AbGroups/AbHom.vo | |
| 68881 ./WildCat/Universe.vo | |
| 68609 ./WildCat/PointedCat.vo | |
| 68257 ./Classes/orders/rings.vo | |
| 67971 ./Basics/Trunc.vo | |
| 67298 ./Categories/Comma/InducedFunctors.vo | |
| 67282 ./Colimits/Quotient/Choice.vo | |
| 66976 ./Tactics.vo | |
| 66837 ./Categories/UniversalProperties.vo | |
| 66110 ./Types/Arrow.vo | |
| 65925 ./Algebra/AbSES/DirectSum.vo | |
| 64087 ./Classes/theory/naturals.vo | |
| 63990 ./Spaces/Finite/FinInduction.vo | |
| 63676 ./Categories/Adjoint/UnitCounitCoercions.vo | |
| 62025 ./Modalities/Fracture.vo | |
| 61789 ./Categories/PseudonaturalTransformation/Core.vo | |
| 61095 ./Homotopy/HSpace/Core.vo | |
| 60847 ./Categories/ProductLaws.vo | |
| 60445 ./Classes/theory/fields.vo | |
| 60231 ./Modalities/Accessible.vo | |
| 59578 ./Truncations/Core.vo | |
| 58780 ./Spaces/Finite/FinNat.vo | |
| 58740 ./Classes/theory/integers.vo | |
| 58308 ./Categories/NaturalTransformation.vo | |
| 57782 ./Categories/Pseudofunctor/Identity.vo | |
| 57743 ./Classes/theory/ua_isomorphic.vo | |
| 56737 ./Sets/GCHtoAC.vo | |
| 56526 ./Categories/ExponentialLaws/Law4/Law.vo | |
| 55987 ./Homotopy/EMSpace.vo | |
| 55630 ./Algebra/Universal/Operation.vo | |
| 55454 ./Classes/orders/nat_int.vo | |
| 55444 ./Algebra/Universal/Homomorphism.vo | |
| 55198 ./Categories/Yoneda.vo | |
| 55134 ./Categories/Grothendieck/PseudofunctorToCat.vo | |
| 55078 ./Categories/Functor/Pointwise/Properties.vo | |
| 54683 ./Classes/theory/int_abs.vo | |
| 53656 ./Basics/Notations.vo | |
| 53224 ./Categories/NaturalTransformation/Isomorphisms.vo | |
| 52636 ./Algebra/AbGroups/Centralizer.vo | |
| 52244 ./Classes/orders/maps.vo | |
| 51961 ./Classes/interfaces/cauchy.vo | |
| 51186 ./Homotopy/PinSn.vo | |
| 50803 ./Categories/Functor/Attributes.vo | |
| 50425 ./Categories/ExponentialLaws/Law4/Functors.vo | |
| 50377 ./Algebra/AbGroups/AbPullback.vo | |
| 50174 ./Equiv/PathSplit.vo | |
| 49712 ./Categories/Adjoint/Composition/Core.vo | |
| 49142 ./Categories/ExponentialLaws/Law3/Law.vo | |
| 49043 ./Spaces/Int/LoopExp.vo | |
| 48796 ./Algebra/Groups/Image.vo | |
| 48018 ./Classes/theory/groups.vo | |
| 47948 ./Modalities/CoreflectiveSubuniverse.vo | |
| 47682 ./Categories/Functor/Prod/Universal.vo | |
| 47117 ./Classes/theory/nat_distance.vo | |
| 46965 ./Algebra/Groups/ShortExactSequence.vo | |
| 46633 ./Categories/Adjoint/Functorial/Parts.vo | |
| 46276 ./Classes/theory/dec_fields.vo | |
| 46181 ./Classes/implementations/bool.vo | |
| 46112 ./WildCat/Monoidal.vo | |
| 46001 ./TruncType.vo | |
| 45374 ./Modalities/Closed.vo | |
| 45366 ./Categories/Limits/Core.vo | |
| 44396 ./Tactics/RewriteModuloAssociativity.vo | |
| 44245 ./Categories/Monoidal/MonoidalCategory.vo | |
| 43858 ./Types/Bool.vo | |
| 43617 ./Categories/Adjoint/Functorial/Core.vo | |
| 43401 ./Categories/Functor/Sum.vo | |
| 43294 ./Homotopy/HSpace/Coherent.vo | |
| 43187 ./Algebra/Groups/Kernel.vo | |
| 42929 ./Categories/NaturalTransformation/Composition/Laws.vo | |
| 42671 ./Spaces/Pos/Core.vo | |
| 42601 ./Classes/theory/lattices.vo | |
| 42386 ./Classes/theory/ua_prod_algebra.vo | |
| 41880 ./HSet.vo | |
| 41874 ./Types/WType.vo | |
| 41830 ./Classes/theory/ua_subalgebra.vo | |
| 41283 ./Spaces/No/Negation.vo | |
| 41207 ./Categories/HomotopyPreCategory.vo | |
| 40844 ./Categories/Adjoint/Composition/AssociativityLaw.vo | |
| 40647 ./Constant.vo | |
| 40247 ./Categories/Adjoint/UniversalMorphisms/Core.vo | |
| 40182 ./Categories/Grothendieck/ToSet/Univalent.vo | |
| 40014 ./Categories/Adjoint/Composition/IdentityLaws.vo | |
| 39973 ./Categories/FunctorCategory/Morphisms.vo | |
| 39460 ./WildCat/Opposite.vo | |
| 39259 ./Categories/Pseudofunctor/FromFunctor.vo | |
| 39234 ./Categories/Functor/Composition/Laws.vo | |
| 38713 ./Categories/ExponentialLaws/Law0.vo | |
| 38490 ./Categories/Grothendieck/ToSet.vo | |
| 37368 ./Classes/theory/apartness.vo | |
| 37311 ./Categories/PseudonaturalTransformation.vo | |
| 37093 ./Spaces/Torus/TorusHomotopy.vo | |
| 36899 ./HoTT.vo | |
| 36848 ./Categories/Structure/Core.vo | |
| 36656 ./Classes/categories/ua_category.vo | |
| 36529 ./Categories/NaturalTransformation/Composition/Core.vo | |
| 35610 ./WildCat/Paths.vo | |
| 35335 ./Algebra/AbGroups/Cyclic.vo | |
| 34912 ./Spaces/BAut/Bool/IncoherentIdempotent.vo | |
| 34698 ./Pointed/pModality.vo | |
| 34286 ./Categories/SetCategory/Morphisms.vo | |
| 33732 ./Modalities/Open.vo | |
| 33589 ./Classes/implementations/hprop_lattice.vo | |
| 33518 ./Categories/InitialTerminalCategory/Functors.vo | |
| 33247 ./Classes/isomorphisms/rings.vo | |
| 33123 ./Classes/tactics/ring_tac.vo | |
| 33022 ./Categories/ExponentialLaws/Law4.vo | |
| 32452 ./Classes/implementations/pointwise.vo | |
| 32281 ./Categories/Pseudofunctor/Core.vo | |
| 32119 ./Categories/Functor/Composition.vo | |
| 32104 ./Categories/Category/Sum.vo | |
| 31597 ./Categories/Category/Sigma/OnMorphisms.vo | |
| 31103 ./Classes/orders/naturals.vo | |
| 31002 ./Metatheory/FunextVarieties.vo | |
| 30993 ./Basics/Decidable.vo | |
| 30464 ./Spaces/List/Paths.vo | |
| 30132 ./Categories/NaturalTransformation/Paths.vo | |
| 30085 ./Diagrams/ConstantDiagram.vo | |
| 29652 ./Categories/ExponentialLaws/Law3/Functors.vo | |
| 29419 ./Categories/ExponentialLaws/Law1/Functors.vo | |
| 29405 ./BoundedSearch.vo | |
| 29266 ./Classes/interfaces/integers.vo | |
| 29055 ./Spaces/Pos/Spec.vo | |
| 28948 ./Classes/interfaces/ua_congruence.vo | |
| 28702 ./Algebra/Universal/Congruence.vo | |
| 27752 ./Categories/Functor/Pointwise.vo | |
| 27195 ./Categories/Functor/Composition/Functorial/Core.vo | |
| 27141 ./Categories/ExponentialLaws/Law1/Law.vo | |
| 26832 ./Categories/LaxComma.vo | |
| 26565 ./Categories/Adjoint/UnitCounit.vo | |
| 26554 ./Categories/Grothendieck/ToSet/Core.vo | |
| 26466 ./Basics/Hexadecimal.vo | |
| 26402 ./Sets/GCH.vo | |
| 26310 ./Spaces/Int/Core.vo | |
| 25969 ./Categories/Functor/Prod.vo | |
| 25921 ./Classes/implementations/ne_list.vo | |
| 25471 ./Classes/orders/integers.vo | |
| 25383 ./Algebra/AbGroups/AbProjective.vo | |
| 25057 ./Categories/Functor/Pointwise/Core.vo | |
| 24996 ./HProp.vo | |
| 24956 ./Classes/orders/fields.vo | |
| 24450 ./Spectra/Spectrum.vo | |
| 24435 ./Categories/Limits.vo | |
| 24308 ./HIT/FreeIntQuotient.vo | |
| 24191 ./Classes/orders/dec_fields.vo | |
| 23951 ./Sets/AC.vo | |
| 23831 ./Categories/FunctorCategory.vo | |
| 23423 ./Modalities/Nullification.vo | |
| 23339 ./Classes/interfaces/rationals.vo | |
| 23091 ./Categories/NaturalTransformation/Identity.vo | |
| 22353 ./Homotopy/EncodeDecode.vo | |
| 22338 ./Categories/NaturalTransformation/Composition.vo | |
| 22034 ./Categories/ExponentialLaws/Law2.vo | |
| 21976 ./Classes/interfaces/naturals.vo | |
| 21959 ./Basics/Decimal.vo | |
| 21856 ./HIT/Interval.vo | |
| 21709 ./Categories/Functor/Composition/Functorial/Attributes.vo | |
| 21473 ./Categories/ExponentialLaws/Tactics.vo | |
| 21324 ./Metatheory/PropTrunc.vo | |
| 21262 ./Basics/Contractible.vo | |
| 21133 ./Categories/Adjoint/Paths.vo | |
| 21095 ./Categories/NaturalTransformation/Core.vo | |
| 21022 ./Categories/CategoryOfSections/Core.vo | |
| 20844 ./Categories/Adjoint/Composition.vo | |
| 20746 ./Categories/ChainCategory.vo | |
| 20733 ./Equiv/Relational.vo | |
| 20273 ./Categories/Functor/Composition/Functorial.vo | |
| 20221 ./Categories/SimplicialSets.vo | |
| 20127 ./Categories/ExponentialLaws/Law2/Functors.vo | |
| 19866 ./Categories/DualFunctor.vo | |
| 19581 ./Categories/Limits/Functors.vo | |
| 19542 ./WildCat/EmptyCat.vo | |
| 19387 ./Categories/Category/Core.vo | |
| 19007 ./Categories/Functor/Prod/Core.vo | |
| 18947 ./Metatheory/UnivalenceImpliesFunext.vo | |
| 18926 ./Categories/KanExtensions/Functors.vo | |
| 18924 ./Categories/Adjoint/UniversalMorphisms.vo | |
| 18891 ./Algebra/AbGroups/Z.vo | |
| 18867 ./Spaces/List/Core.vo | |
| 18628 ./Categories/SetCategory.vo | |
| 18583 ./Categories/NaturalTransformation/Pointwise.vo | |
| 18030 ./PathAny.vo | |
| 17926 ./Categories/KanExtensions.vo | |
| 17855 ./Classes/orders/sum.vo | |
| 17790 ./Diagrams/ParallelPair.vo | |
| 17712 ./Categories/Utf8.vo | |
| 17626 ./Utf8.vo | |
| 17581 ./Categories/InitialTerminalCategory/NaturalTransformations.vo | |
| 17450 ./Categories/CategoryOfSections.vo | |
| 17410 ./Categories/ExponentialLaws/Law1.vo | |
| 17228 ./Categories/Adjoint/Composition/LawsTactic.vo | |
| 17202 ./Classes/interfaces/ua_setalgebra.vo | |
| 17030 ./Classes/theory/additional_operations.vo | |
| 16754 ./Algebra/ooAction.vo | |
| 16650 ./Categories/Notations.vo | |
| 16599 ./Algebra/Aut.vo | |
| 16419 ./Categories/Category/Sigma/Core.vo | |
| 16388 ./Colimits/SpanPushout.vo | |
| 16348 ./Categories/KanExtensions/Core.vo | |
| 16274 ./Algebra/AbSES.vo | |
| 16204 ./Types/Unit.vo | |
| 16182 ./Classes/orders/archimedean.vo | |
| 16054 ./WildCat/Induced.vo | |
| 16018 ./Categories/Functor/Prod/Functorial.vo | |
| 15957 ./Sets/Powers.vo | |
| 15929 ./Algebra/Rings.vo | |
| 15740 ./Classes/implementations/assume_rationals.vo | |
| 15634 ./Categories/Category/Sigma/OnObjects.vo | |
| 15384 ./Categories/NaturalTransformation/Prod.vo | |
| 15179 ./Algebra/AbGroups.vo | |
| 15137 ./Classes/interfaces/archimedean.vo | |
| 14996 ./Categories/FundamentalPreGroupoidCategory.vo | |
| 14953 ./Categories/FunctorCategory/Functorial.vo | |
| 14774 ./Categories/LaxComma/Notations.vo | |
| 14527 ./WildCat/Sigma.vo | |
| 14385 ./Categories/NaturalTransformation/Utf8.vo | |
| 14212 ./Categories/HomFunctor.vo | |
| 14205 ./NullHomotopy.vo | |
| 14161 ./Categories/Adjoint/Hom.vo | |
| 14010 ./Spaces/Nat/Paths.vo | |
| 13942 ./Categories/Functor/Utf8.vo | |
| 13913 ./Categories/FunctorCategory/Utf8.vo | |
| 13897 ./Categories/GroupoidCategory/Core.vo | |
| 13886 ./Truncations/SeparatedTrunc.vo | |
| 13839 ./Functorish.vo | |
| 13785 ./Categories/Category/Prod.vo | |
| 13540 ./Categories/ExponentialLaws/Law3.vo | |
| 13532 ./Algebra/Groups.vo | |
| 13522 ./Categories/Cat/Core.vo | |
| 13461 ./Diagrams/DDiagram.vo | |
| 13236 ./Homotopy/EvaluationFibration.vo | |
| 13235 ./Spaces/Cantor.vo | |
| 13220 ./Categories/Comma/Projection.vo | |
| 13209 ./Categories/InitialTerminalCategory/Core.vo | |
| 13147 ./Colimits/Colimit_Prod.vo | |
| 13018 ./Diagrams/Sequence.vo | |
| 12497 ./Basics/Nat.vo | |
| 12439 ./HIT/surjective_factor.vo | |
| 12367 ./Categories/Category/Objects.vo | |
| 12264 ./Categories/IndiscreteCategory.vo | |
| 12158 ./PropResizing/ImpredicativeTruncation.vo | |
| 12068 ./Categories/Cat.vo | |
| 12037 ./Classes/implementations/family_prod.vo | |
| 12004 ./WildCat/Forall.vo | |
| 11959 ./Categories/Functor/Notations.vo | |
| 11901 ./Categories/Functor/Core.vo | |
| 11679 ./HIT/iso.vo | |
| 11582 ./Categories/NaturalTransformation/Sum.vo | |
| 11403 ./Equiv/BiInv.vo | |
| 11401 ./Classes/interfaces/monad.vo | |
| 11296 ./Categories/InitialTerminalCategory.vo | |
| 11282 ./Categories/GroupoidCategory.vo | |
| 11280 ./Homotopy/Join.vo | |
| 11191 ./Modalities/Notnot.vo | |
| 11101 ./Metatheory/TruncImpliesFunext.vo | |
| 11018 ./Diagrams/Span.vo | |
| 10834 ./Categories/LaxComma/Utf8.vo | |
| 10707 ./Categories/Profunctor/Representable.vo | |
| 10625 ./Classes/interfaces/round.vo | |
| 10625 ./Categories/NaturalTransformation/Composition/Functorial.vo | |
| 10537 ./Spaces/Int/Equiv.vo | |
| 10507 ./Homotopy/HSpace.vo | |
| 10371 ./Categories/GroupoidCategory/Morphisms.vo | |
| 10287 ./Categories/SetCategory/Functors/SetProp.vo | |
| 10156 ./Categories/NatCategory.vo | |
| 10119 ./Categories/DependentProduct.vo | |
| 10053 ./Categories/Grothendieck/ToCat.vo | |
| 9882 ./Categories/Cat/Morphisms.vo | |
| 9859 ./Categories/Comma/Dual.vo | |
| 9819 ./Pointed.vo | |
| 9733 ./HIT/unique_choice.vo | |
| 9315 ./Categories/FunctorCategory/Core.vo | |
| 9244 ./Categories/Category/Pi.vo | |
| 9135 ./Basics/Utf8.vo | |
| 9121 ./Categories/FunctorCategory/Dual.vo | |
| 9034 ./Categories/ExponentialLaws.vo | |
| 8920 ./Modalities/Identity.vo | |
| 8899 ./ExcludedMiddle.vo | |
| 8837 ./Algebra/Congruence.vo | |
| 8701 ./Categories/Profunctor.vo | |
| 8647 ./Categories/Functor/Composition/Core.vo | |
| 8615 ./HIT/SetCone.vo | |
| 8581 ./Limits/Equalizer.vo | |
| 8573 ./Types/Empty.vo | |
| 8481 ./Categories/GroupoidCategory/Dual.vo | |
| 8320 ./Categories/Category/Utf8.vo | |
| 8190 ./Categories/Category/Univalent.vo | |
| 8077 ./Categories/Adjoint/Dual.vo | |
| 7998 ./Basics/Datatypes.vo | |
| 7903 ./Categories/Grothendieck.vo | |
| 7889 ./Tactics/BinderApply.vo | |
| 7837 ./Categories/CategoryOfGroupoids.vo | |
| 7794 ./Categories/SetCategory/Core.vo | |
| 7776 ./Categories/Adjoint/Utf8.vo | |
| 7234 ./Spaces/Finite.vo | |
| 7161 ./Categories/SetCategory/Functors.vo | |
| 7051 ./Categories/NaturalTransformation/Notations.vo | |
| 6903 ./Categories/Adjoint/Notations.vo | |
| 6779 ./Categories/Adjoint/Identity.vo | |
| 6694 ./Basics/Numeral.vo | |
| 6517 ./Categories/Category/Dual.vo | |
| 6469 ./Categories/InitialTerminalCategory/Notations.vo | |
| 6454 ./Categories/Adjoint/Functorial.vo | |
| 6438 ./Categories/Profunctor/Core.vo | |
| 6377 ./Categories/Comma/Utf8.vo | |
| 6052 ./Categories/Profunctor/Identity.vo | |
| 6016 ./Truncations.vo | |
| 6001 ./Categories/Category/Notations.vo | |
| 5853 ./Categories/NaturalTransformation/Dual.vo | |
| 5848 ./WildCat.vo | |
| 5842 ./Spaces/Nat.vo | |
| 5669 ./Tactics/EvalIn.vo | |
| 5387 ./Categories/Functor/Dual.vo | |
| 5365 ./Categories/Profunctor/Utf8.vo | |
| 5286 ./Categories/FunctorCategory/Notations.vo | |
| 5283 ./Metatheory/Core.vo | |
| 5105 ./Metatheory/IntervalImpliesFunext.vo | |
| 5074 ./Categories/Profunctor/Notations.vo | |
| 5009 ./WildCat/UnitCat.vo | |
| 4958 ./Categories/Comma/Notations.vo | |
| 4654 ./Categories/Category/Subcategory.vo | |
| 4591 ./Spaces/Finite/Tactics.vo | |
| 4574 ./Categories/Category/Subcategory/Full.vo | |
| 4381 ./Categories/Adjoint/Core.vo | |
| 4306 ./Categories/DiscreteCategory.vo | |
| 4302 ./Categories/Structure/Utf8.vo | |
| 4196 ./Categories/Category/Subcategory/Wide.vo | |
| 4171 ./Categories/Category/Strict.vo | |
| 3906 ./PropResizing/PropResizing.vo | |
| 3680 ./Basics/Logic.vo | |
| 3419 ./Spaces/Int.vo | |
| 3384 ./Categories/Structure/Notations.vo | |
| 3294 ./Types.vo | |
| 3151 ./Diagrams/Graph.vo | |
| 2972 ./Axioms/Univalence.vo | |
| 2950 ./Cubical.vo | |
| 2935 ./Utf8Minimal.vo | |
| 2923 ./Misc.vo | |
| 2533 ./Categories/Functor/Identity.vo | |
| 2178 ./Spaces/Pos.vo | |
| 2155 ./Basics.vo | |
| 1897 ./Tactics/Nameless.vo | |
| 1412 ./Axioms/Funext.vo |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 43848878 total | |
| 2308968 ./Spaces/Torus/TorusEquivCircles.vo | |
| 1482258 ./Pointed/Core.vo | |
| 1337987 ./Homotopy/CayleyDickson.vo | |
| 1178536 ./Homotopy/Syllepsis.vo | |
| 1145295 ./Classes/implementations/natpair_integers.vo | |
| 1093804 ./Colimits/Sequential.vo | |
| 1070420 ./Cubical/PathCube.vo | |
| 1065044 ./Spaces/Spheres.vo | |
| 963335 ./Colimits/Colimit_Flattening.vo | |
| 743685 ./Categories.vo | |
| 478141 ./Spaces/No.vo | |
| 461229 ./Categories/Comma.vo | |
| 460714 ./Homotopy/Join/TriJoin.vo | |
| 460349 ./Algebra/Groups/FreeProduct.vo | |
| 452021 ./WildCat/DisplayedEquiv.vo | |
| 383128 ./Modalities/ReflectiveSubuniverse.vo | |
| 358362 ./Colimits/GraphQuotient.vo | |
| 350968 ./Homotopy/Smash.vo | |
| 347862 ./Homotopy/Wedge.vo | |
| 345398 ./Homotopy/Join/JoinAssoc.vo | |
| 333180 ./Classes/theory/premetric.vo | |
| 311460 ./WildCat/Products.vo | |
| 304109 ./Classes/theory/rationals.vo | |
| 294320 ./Categories/LaxComma/CoreLaws.vo | |
| 277179 ./Basics/PathGroupoids.vo | |
| 263137 ./Homotopy/BlakersMassey.vo | |
| 258966 ./Colimits/Colimit_Pushout_Flattening.vo | |
| 251477 ./Algebra/AbSES/PullbackFiberSequence.vo | |
| 249517 ./Algebra/AbSES/Core.vo | |
| 249027 ./Categories/Category.vo | |
| 245831 ./Homotopy/ClassifyingSpace.vo | |
| 245531 ./Spaces/BAut/Bool.vo | |
| 241646 ./Homotopy/ExactSequence.vo | |
| 226524 ./Spaces/TwoSphere.vo | |
| 223287 ./Classes/interfaces/abstract_algebra.vo | |
| 223111 ./Algebra/Rings/Ideal.vo | |
| 222812 ./Spaces/No/Core.vo | |
| 219178 ./Modalities/Lex.vo | |
| 217617 ./Pointed/Loops.vo | |
| 213459 ./Algebra/AbSES/Pushout.vo | |
| 208052 ./Algebra/Groups/FreeGroup.vo | |
| 207194 ./Categories/Category/Paths.vo | |
| 207176 ./PropResizing/Nat.vo | |
| 206483 ./WildCat/Displayed.vo | |
| 205886 ./Colimits/Colimit_Pushout.vo | |
| 200240 ./Analysis/Locator.vo | |
| 199404 ./Limits/Pullback.vo | |
| 194276 ./Types/Sum.vo | |
| 191708 ./Colimits/Pushout.vo | |
| 188833 ./Homotopy/Join/Core.vo | |
| 187251 ./WildCat/Equiv.vo | |
| 183986 ./Spaces/Finite/Finite.vo | |
| 177761 ./Algebra/AbGroups/Abelianization.vo | |
| 167318 ./HIT/V.vo | |
| 165696 ./Spaces/Card.vo | |
| 164896 ./Idempotents.vo | |
| 164581 ./Spaces/No/Addition.vo | |
| 163232 ./Extensions.vo | |
| 162498 ./Modalities/Meet.vo | |
| 156313 ./Sets/Ordinals.vo | |
| 154952 ./Classes/orders/semirings.vo | |
| 153681 ./Algebra/Groups/GroupCoeq.vo | |
| 153549 ./Algebra/AbSES/Pullback.vo | |
| 153273 ./Types/Universe.vo | |
| 149731 ./WildCat/Core.vo | |
| 136572 ./WildCat/Adjoint.vo | |
| 135167 ./Pointed/pSusp.vo | |
| 132968 ./Types/Paths.vo | |
| 132278 ./Algebra/Groups/Group.vo | |
| 130555 ./Types/Sigma.vo | |
| 129453 ./Colimits/Quotient.vo | |
| 128792 ./Categories/Adjoint.vo | |
| 128616 ./Algebra/AbSES/SixTerm.vo | |
| 128365 ./Categories/Category/Morphisms.vo | |
| 127151 ./Colimits/Coeq.vo | |
| 123702 ./Homotopy/Suspension.vo | |
| 123249 ./WildCat/Yoneda.vo | |
| 122719 ./Sets/Hartogs.vo | |
| 122683 ./Categories/Grothendieck/ToSet/Morphisms.vo | |
| 122405 ./Tactics/EquivalenceInduction.vo | |
| 120829 ./Spaces/Universe.vo | |
| 119870 ./Homotopy/Freudenthal.vo | |
| 119804 ./Cubical/PathSquare.vo | |
| 118383 ./Categories/Category/Sigma/Univalent.vo | |
| 118119 ./Modalities/Modality.vo | |
| 115694 ./Classes/implementations/field_of_fractions.vo | |
| 115012 ./Homotopy/HomotopyGroup.vo | |
| 114841 ./Algebra/Rings/Ring.vo | |
| 112311 ./Algebra/Rings/Module.vo | |
| 111256 ./Categories/Pseudofunctor.vo | |
| 111054 ./WildCat/Sum.vo | |
| 110064 ./Types/IWType.vo | |
| 107031 ./Classes/interfaces/orders.vo | |
| 106609 ./Classes/implementations/binary_naturals.vo | |
| 106494 ./Classes/interfaces/canonical_names.vo | |
| 105445 ./Basics/Tactics.vo | |
| 105038 ./Algebra/Groups/GrpPullback.vo | |
| 104002 ./Pointed/pMap.vo | |
| 102880 ./Categories/Adjoint/Pointwise.vo | |
| 101481 ./Homotopy/Hopf.vo | |
| 100738 ./Spaces/BAut.vo | |
| 100121 ./Modalities/Descent.vo | |
| 99663 ./Spaces/Finite/FinSeq.vo | |
| 97609 ./Colimits/Colimit.vo | |
| 95562 ./Algebra/Groups/Subgroup.vo | |
| 94771 ./Algebra/AbSES/BaerSum.vo | |
| 93909 ./Types/Prod.vo | |
| 91165 ./Categories/Functor/Paths.vo | |
| 90684 ./Diagrams/Cocone.vo | |
| 90460 ./WildCat/Bifunctor.vo | |
| 89182 ./Spaces/Nat/Arithmetic.vo | |
| 88378 ./Homotopy/HSpace/Pointwise.vo | |
| 87467 ./Classes/theory/rings.vo | |
| 87351 ./Factorization.vo | |
| 86585 ./Basics/Equivalences.vo | |
| 85471 ./Classes/implementations/peano_naturals.vo | |
| 85464 ./Categories/Functor.vo | |
| 83419 ./Homotopy/HSpace/Moduli.vo | |
| 82775 ./Classes/theory/ua_third_isomorphism.vo | |
| 82226 ./Categories/Category/Sigma.vo | |
| 81802 ./Categories/LaxComma/Core.vo | |
| 81347 ./Classes/tactics/ring_quote.vo | |
| 81000 ./Categories/Comma/Functorial.vo | |
| 78669 ./HFiber.vo | |
| 78370 ./Algebra/Rings/QuotientRing.vo | |
| 78354 ./WildCat/NatTrans.vo | |
| 77958 ./Pointed/pFiber.vo | |
| 75697 ./Algebra/AbGroups/AbPushout.vo | |
| 75673 ./Algebra/Groups/QuotientGroup.vo | |
| 75179 ./Categories/Adjoint/Functorial/Laws.vo | |
| 74655 ./Algebra/ooGroup.vo | |
| 74578 ./Diagrams/Cone.vo | |
| 74541 ./Algebra/Rings/ChineseRemainder.vo | |
| 74296 ./WildCat/FunctorCat.vo | |
| 73736 ./Classes/orders/orders.vo | |
| 73642 ./Categories/Comma/Core.vo | |
| 73530 ./Cubical/DPathCube.vo | |
| 71937 ./Classes/theory/ua_second_isomorphism.vo | |
| 71760 ./Categories/Pseudofunctor/RewriteLaws.vo | |
| 71203 ./Categories/LaxComma/CoreParts.vo | |
| 70947 ./Categories/Structure.vo | |
| 70312 ./Colimits/CoeqUnivProp.vo | |
| 69229 ./Basics/Overture.vo | |
| 69215 ./Classes/orders/lattices.vo | |
| 68841 ./HIT/Flattening.vo | |
| 68177 ./WildCat/Prod.vo | |
| 68169 ./Colimits/Colimit_Sigma.vo | |
| 67897 ./Algebra/Groups/Presentation.vo | |
| 67347 ./Classes/orders/rings.vo | |
| 67255 ./Algebra/Rings/CRing.vo | |
| 66467 ./Homotopy/HSpaceS1.vo | |
| 66128 ./Algebra/Universal/TermAlgebra.vo | |
| 65394 ./Spaces/Nat/Core.vo | |
| 65054 ./Classes/tactics/ring_pol.vo | |
| 64947 ./Algebra/AbSES/Ext.vo | |
| 64824 ./Homotopy/SuccessorStructure.vo | |
| 64792 ./Spaces/Circle.vo | |
| 64599 ./WildCat/TwoOneCat.vo | |
| 64566 ./Algebra/AbGroups/AbelianGroup.vo | |
| 63367 ./ObjectClassifier.vo | |
| 63356 ./Categories/Adjoint/HomCoercions.vo | |
| 62592 ./Categories/ExponentialLaws/Law2/Law.vo | |
| 62491 ./Spaces/Int/Spec.vo | |
| 62201 ./Cubical/DPath.vo | |
| 61806 ./Algebra/AbGroups/Biproduct.vo | |
| 61804 ./WildCat/Coproducts.vo | |
| 61778 ./Classes/theory/naturals.vo | |
| 61504 ./Categories/PseudonaturalTransformation/Core.vo | |
| 61119 ./Classes/theory/ua_quotient_algebra.vo | |
| 60225 ./Categories/NaturalTransformation.vo | |
| 60074 ./Spaces/Finite/Fin.vo | |
| 59272 ./Types/Forall.vo | |
| 59026 ./Classes/theory/fields.vo | |
| 58897 ./Colimits/MappingCylinder.vo | |
| 58064 ./Spaces/BAut/Cantor.vo | |
| 57405 ./Tactics.vo | |
| 57198 ./Modalities/Localization.vo | |
| 57058 ./Diagrams/CommutativeSquares.vo | |
| 56965 ./Classes/theory/ua_first_isomorphism.vo | |
| 56838 ./Categories/Comma/ProjectionFunctors.vo | |
| 56258 ./Sets/GCHtoAC.vo | |
| 56072 ./Classes/theory/ua_homomorphism.vo | |
| 56072 ./Classes/theory/integers.vo | |
| 55947 ./Algebra/Universal/Algebra.vo | |
| 55942 ./Categories/InitialTerminalCategory/Pseudofunctors.vo | |
| 55809 ./Algebra/Rings/Z.vo | |
| 55454 ./Classes/orders/nat_int.vo | |
| 54683 ./Classes/theory/int_abs.vo | |
| 54630 ./HIT/quotient.vo | |
| 54033 ./Diagrams/Diagram.vo | |
| 53656 ./Basics/Notations.vo | |
| 53146 ./WildCat/Square.vo | |
| 52013 ./Classes/orders/maps.vo | |
| 51921 ./Colimits/Quotient/Choice.vo | |
| 51249 ./Metatheory/UnivalenceVarieties.vo | |
| 50657 ./Homotopy/Cover.vo | |
| 50410 ./Categories/ExponentialLaws/Law4/Law.vo | |
| 50216 ./Categories/Grothendieck/PseudofunctorToCat.vo | |
| 48422 ./Algebra/Universal/Operation.vo | |
| 47762 ./WildCat/EquivGpd.vo | |
| 47601 ./DProp.vo | |
| 46445 ./Categories/ExponentialLaws/Law3/Law.vo | |
| 46192 ./Classes/theory/dec_fields.vo | |
| 45959 ./Pointed/pTrunc.vo | |
| 45009 ./Cubical/DPathSquare.vo | |
| 44977 ./Classes/interfaces/cauchy.vo | |
| 44793 ./Categories/Comma/InducedFunctors.vo | |
| 44469 ./Basics/Trunc.vo | |
| 44356 ./Tactics/RewriteModuloAssociativity.vo | |
| 43745 ./Algebra/Universal/Homomorphism.vo | |
| 43413 ./Modalities/Separated.vo | |
| 42800 ./Truncations/Connectedness.vo | |
| 42743 ./WildCat/Universe.vo | |
| 42667 ./Categories/ExponentialLaws/Law4/Functors.vo | |
| 42131 ./Categories/Yoneda.vo | |
| 41888 ./Classes/theory/lattices.vo | |
| 41638 ./Homotopy/WhiteheadsPrinciple.vo | |
| 41132 ./Categories/Functor/Attributes.vo | |
| 40844 ./Categories/Adjoint/Composition/AssociativityLaw.vo | |
| 40651 ./HIT/epi.vo | |
| 40279 ./Types/Equiv.vo | |
| 40127 ./Types/Arrow.vo | |
| 40025 ./Categories/Functor/Sum.vo | |
| 40014 ./Categories/Adjoint/Composition/IdentityLaws.vo | |
| 39841 ./Modalities/Topological.vo | |
| 39704 ./Limits/Limit.vo | |
| 39674 ./Categories/Functor/Pointwise/Properties.vo | |
| 39654 ./WildCat/Monoidal.vo | |
| 39451 ./Categories/UniversalProperties.vo | |
| 39067 ./Modalities/Fracture.vo | |
| 38947 ./Classes/theory/groups.vo | |
| 38899 ./Homotopy/HSpace/Core.vo | |
| 38664 ./Categories/Grothendieck/ToSet.vo | |
| 38521 ./Truncations/Core.vo | |
| 38352 ./Algebra/AbGroups/AbHom.vo | |
| 38156 ./Colimits/Colimit_Coequalizer.vo | |
| 38081 ./Categories/Adjoint/UnitCounitCoercions.vo | |
| 37311 ./Categories/PseudonaturalTransformation.vo | |
| 37282 ./Categories/NaturalTransformation/Isomorphisms.vo | |
| 37003 ./Classes/theory/apartness.vo | |
| 36899 ./HoTT.vo | |
| 36882 ./WildCat/ZeroGroupoid.vo | |
| 36804 ./Homotopy/Bouquet.vo | |
| 36540 ./Modalities/Accessible.vo | |
| 36125 ./Categories/Monoidal/MonoidalCategory.vo | |
| 36043 ./Spaces/BAut/Rigid.vo | |
| 35987 ./Classes/interfaces/ua_algebra.vo | |
| 35708 ./Spaces/List/Theory.vo | |
| 35351 ./Projective.vo | |
| 35148 ./Algebra/AbSES/DirectSum.vo | |
| 35009 ./WildCat/PointedCat.vo | |
| 34895 ./Homotopy/EMSpace.vo | |
| 34820 ./Categories/Functor/Composition/Laws.vo | |
| 34785 ./Algebra/Groups/Lagrange.vo | |
| 34767 ./EquivGroupoids.vo | |
| 34638 ./Categories/NaturalTransformation/Composition/Laws.vo | |
| 34062 ./Categories/ExponentialLaws/Law4.vo | |
| 33645 ./TruncType.vo | |
| 33472 ./WildCat/Opposite.vo | |
| 33130 ./Categories/Functor/Composition.vo | |
| 33067 ./Categories/ProductLaws.vo | |
| 33037 ./Classes/tactics/ring_tac.vo | |
| 33004 ./Homotopy/Join/JoinSusp.vo | |
| 32896 ./Categories/Structure/IdentityPrinciple.vo | |
| 32669 ./Classes/theory/ua_subalgebra.vo | |
| 32438 ./Categories/Pseudofunctor/FromFunctor.vo | |
| 31862 ./Categories/Pseudofunctor/Core.vo | |
| 31712 ./Pointed/pEquiv.vo | |
| 31276 ./Classes/theory/ua_isomorphic.vo | |
| 31184 ./Categories/Functor/Prod/Universal.vo | |
| 31103 ./Classes/orders/naturals.vo | |
| 31070 ./Classes/isomorphisms/rings.vo | |
| 30886 ./Pointed/pSect.vo | |
| 30599 ./Categories/Structure/Core.vo | |
| 30547 ./Spaces/Int/LoopExp.vo | |
| 30286 ./Homotopy/PinSn.vo | |
| 29820 ./Categories/Functor/Pointwise.vo | |
| 28922 ./Categories/Category/Sigma/OnMorphisms.vo | |
| 28813 ./Spaces/Pos/Core.vo | |
| 28720 ./Spaces/Finite/FinNat.vo | |
| 28595 ./Categories/LaxComma.vo | |
| 28466 ./Categories/Pseudofunctor/Identity.vo | |
| 28313 ./Classes/theory/ua_prod_algebra.vo | |
| 27887 ./Categories/Category/Sum.vo | |
| 27528 ./Modalities/CoreflectiveSubuniverse.vo | |
| 27270 ./Algebra/AbGroups/Centralizer.vo | |
| 27247 ./Categories/SetCategory/Morphisms.vo | |
| 27008 ./Categories/FunctorCategory/Morphisms.vo | |
| 26996 ./Spaces/Torus/TorusHomotopy.vo | |
| 26855 ./Categories/Functor/Prod.vo | |
| 26651 ./Classes/interfaces/integers.vo | |
| 26519 ./Categories/Adjoint/UniversalMorphisms/Core.vo | |
| 25693 ./Categories/ExponentialLaws/Law1/Law.vo | |
| 25548 ./Algebra/Groups/Image.vo | |
| 25471 ./Classes/orders/integers.vo | |
| 25412 ./Categories/Limits/Core.vo | |
| 25314 ./Algebra/Groups/ShortExactSequence.vo | |
| 25170 ./Categories/Adjoint/Composition/Core.vo | |
| 24956 ./Classes/orders/fields.vo | |
| 24926 ./Sets/GCH.vo | |
| 24876 ./Categories/Limits.vo | |
| 24824 ./Classes/theory/nat_distance.vo | |
| 24783 ./Spaces/Pos/Spec.vo | |
| 24761 ./Spaces/No/Negation.vo | |
| 24689 ./Homotopy/HSpace/Coherent.vo | |
| 24358 ./Categories/FunctorCategory.vo | |
| 24308 ./HIT/FreeIntQuotient.vo | |
| 24232 ./Algebra/AbGroups/Cyclic.vo | |
| 24191 ./Classes/orders/dec_fields.vo | |
| 24001 ./Types/Bool.vo | |
| 23913 ./Algebra/AbGroups/AbPullback.vo | |
| 23878 ./Spaces/Finite/FinInduction.vo | |
| 23817 ./Classes/interfaces/ua_congruence.vo | |
| 23743 ./Modalities/Closed.vo | |
| 23658 ./Equiv/PathSplit.vo | |
| 23211 ./Constant.vo | |
| 23196 ./Sets/AC.vo | |
| 23190 ./Categories/NaturalTransformation/Composition.vo | |
| 23016 ./Categories/ExponentialLaws/Law2.vo | |
| 22955 ./Algebra/Groups/Kernel.vo | |
| 22869 ./Classes/implementations/pointwise.vo | |
| 22306 ./Basics/Decidable.vo | |
| 22303 ./HSet.vo | |
| 22271 ./Spaces/Torus/Torus.vo | |
| 22099 ./Algebra/Universal/Congruence.vo | |
| 21848 ./Classes/interfaces/rationals.vo | |
| 21709 ./Categories/Functor/Composition/Functorial/Attributes.vo | |
| 21701 ./Categories/Adjoint/Composition.vo | |
| 21699 ./Categories/NaturalTransformation/Paths.vo | |
| 21605 ./Categories/InitialTerminalCategory/Functors.vo | |
| 21473 ./Categories/ExponentialLaws/Tactics.vo | |
| 21219 ./Categories/Grothendieck/ToSet/Core.vo | |
| 21170 ./Categories/Functor/Pointwise/Core.vo | |
| 20863 ./Categories/Adjoint/Paths.vo | |
| 20726 ./Classes/implementations/hprop_lattice.vo | |
| 20669 ./Categories/Functor/Composition/Functorial.vo | |
| 20524 ./Modalities/Open.vo | |
| 20520 ./Categories/Adjoint/UnitCounit.vo | |
| 20378 ./Classes/interfaces/naturals.vo | |
| 20239 ./Categories/ExponentialLaws/Law0.vo | |
| 20207 ./Classes/implementations/ne_list.vo | |
| 19713 ./Categories/ExponentialLaws/Law1/Functors.vo | |
| 19694 ./Classes/categories/ua_category.vo | |
| 19692 ./Spaces/List/Paths.vo | |
| 19563 ./Categories/DualFunctor.vo | |
| 19530 ./Classes/implementations/bool.vo | |
| 19512 ./Spaces/Int/Core.vo | |
| 19386 ./Categories/Functor/Composition/Functorial/Core.vo | |
| 19370 ./Categories/Adjoint/UniversalMorphisms.vo | |
| 19335 ./Categories/CategoryOfSections/Core.vo | |
| 18986 ./Categories/SetCategory.vo | |
| 18828 ./Pointed/pModality.vo | |
| 18762 ./BoundedSearch.vo | |
| 18602 ./Spectra/Spectrum.vo | |
| 18546 ./Categories/KanExtensions.vo | |
| 18241 ./Categories/SemiSimplicialSets.vo | |
| 18042 ./Categories/Adjoint/Functorial/Parts.vo | |
| 17824 ./Categories/ExponentialLaws/Law1.vo | |
| 17807 ./Spaces/BAut/Bool/IncoherentIdempotent.vo | |
| 17712 ./Categories/Utf8.vo | |
| 17626 ./Utf8.vo | |
| 17552 ./Algebra/AbGroups/AbProjective.vo | |
| 17519 ./Categories/CategoryOfSections.vo | |
| 17510 ./Categories/NaturalTransformation/Composition/Core.vo | |
| 17495 ./WildCat/Paths.vo | |
| 17312 ./Categories/Adjoint/Functorial/Core.vo | |
| 17307 ./HProp.vo | |
| 17303 ./Basics/Hexadecimal.vo | |
| 17266 ./Types/WType.vo | |
| 17228 ./Categories/Adjoint/Composition/LawsTactic.vo | |
| 16994 ./Categories/Category/Core.vo | |
| 16787 ./Categories/HomotopyPreCategory.vo | |
| 16650 ./Categories/Notations.vo | |
| 16584 ./Metatheory/FunextVarieties.vo | |
| 16575 ./Algebra/ooAction.vo | |
| 16473 ./Algebra/Aut.vo | |
| 16347 ./Categories/Grothendieck/ToSet/Univalent.vo | |
| 16338 ./Classes/theory/additional_operations.vo | |
| 16274 ./Algebra/AbSES.vo | |
| 16252 ./Homotopy/EncodeDecode.vo | |
| 16150 ./Diagrams/ConstantDiagram.vo | |
| 15952 ./Categories/ExponentialLaws/Law2/Functors.vo | |
| 15929 ./Algebra/Rings.vo | |
| 15885 ./Algebra/AbGroups/Z.vo | |
| 15740 ./Classes/implementations/assume_rationals.vo | |
| 15650 ./Metatheory/PropTrunc.vo | |
| 15416 ./Categories/Functor/Prod/Core.vo | |
| 15401 ./Categories/Limits/Functors.vo | |
| 15251 ./Categories/KanExtensions/Functors.vo | |
| 15179 ./Algebra/AbGroups.vo | |
| 15130 ./Categories/InitialTerminalCategory/NaturalTransformations.vo | |
| 15055 ./Classes/orders/archimedean.vo | |
| 14964 ./Categories/NaturalTransformation/Pointwise.vo | |
| 14865 ./Modalities/Nullification.vo | |
| 14823 ./Basics/Decimal.vo | |
| 14802 ./Categories/NaturalTransformation/Core.vo | |
| 14774 ./Categories/LaxComma/Notations.vo | |
| 14498 ./Classes/orders/sum.vo | |
| 14497 ./Categories/Category/Sigma/Core.vo | |
| 14385 ./Categories/NaturalTransformation/Utf8.vo | |
| 14237 ./Equiv/Relational.vo | |
| 14236 ./Sets/Powers.vo | |
| 14041 ./Categories/Category/Sigma/OnObjects.vo | |
| 14020 ./Categories/Adjoint/Hom.vo | |
| 13971 ./Categories/ExponentialLaws/Law3.vo | |
| 13958 ./Classes/interfaces/ua_setalgebra.vo | |
| 13942 ./Categories/Functor/Utf8.vo | |
| 13913 ./Categories/FunctorCategory/Utf8.vo | |
| 13777 ./Categories/FundamentalPreGroupoidCategory.vo | |
| 13688 ./Categories/KanExtensions/Core.vo | |
| 13619 ./WildCat/Induced.vo | |
| 13604 ./Categories/Functor/Prod/Functorial.vo | |
| 13532 ./Algebra/Groups.vo | |
| 13290 ./Categories/NaturalTransformation/Prod.vo | |
| 13281 ./Basics/Contractible.vo | |
| 13052 ./Classes/interfaces/archimedean.vo | |
| 12965 ./PathAny.vo | |
| 12957 ./Categories/ChainCategory.vo | |
| 12574 ./Categories/Category/Prod.vo | |
| 12453 ./Homotopy/EvaluationFibration.vo | |
| 12361 ./Diagrams/DDiagram.vo | |
| 12319 ./Categories/InitialTerminalCategory/Core.vo | |
| 12313 ./Spaces/List/Core.vo | |
| 12308 ./Categories/Comma/Projection.vo | |
| 12199 ./Categories/HomFunctor.vo | |
| 12185 ./Categories/Cat.vo | |
| 12051 ./Truncations/SeparatedTrunc.vo | |
| 12024 ./Categories/SimplicialSets.vo | |
| 11959 ./Categories/Functor/Notations.vo | |
| 11854 ./Categories/ExponentialLaws/Law3/Functors.vo | |
| 11830 ./Metatheory/UnivalenceImpliesFunext.vo | |
| 11700 ./Categories/Category/Objects.vo | |
| 11628 ./Categories/Functor/Core.vo | |
| 11367 ./Categories/FunctorCategory/Functorial.vo | |
| 11350 ./Categories/InitialTerminalCategory.vo | |
| 11336 ./Categories/GroupoidCategory.vo | |
| 11298 ./HIT/surjective_factor.vo | |
| 11280 ./Homotopy/Join.vo | |
| 11174 ./Classes/interfaces/monad.vo | |
| 11143 ./Types/Unit.vo | |
| 11138 ./Spaces/Nat/Paths.vo | |
| 11082 ./Categories/NaturalTransformation/Identity.vo | |
| 10982 ./Categories/IndiscreteCategory.vo | |
| 10834 ./Categories/LaxComma/Utf8.vo | |
| 10743 ./Categories/Cat/Core.vo | |
| 10667 ./Categories/GroupoidCategory/Core.vo | |
| 10650 ./Colimits/SpanPushout.vo | |
| 10507 ./Homotopy/HSpace.vo | |
| 10334 ./Categories/GroupoidCategory/Morphisms.vo | |
| 10276 ./Functorish.vo | |
| 10267 ./Spaces/Int/Equiv.vo | |
| 10183 ./WildCat/Sigma.vo | |
| 10172 ./Categories/NaturalTransformation/Sum.vo | |
| 10157 ./Classes/interfaces/round.vo | |
| 9882 ./Categories/Cat/Morphisms.vo | |
| 9819 ./Pointed.vo | |
| 9767 ./NullHomotopy.vo | |
| 9710 ./Colimits/Colimit_Prod.vo | |
| 9615 ./Categories/Comma/Dual.vo | |
| 9456 ./HIT/iso.vo | |
| 9440 ./Categories/Grothendieck/ToCat.vo | |
| 9405 ./Categories/NatCategory.vo | |
| 9326 ./WildCat/Forall.vo | |
| 9318 ./Metatheory/TruncImpliesFunext.vo | |
| 9261 ./PropResizing/ImpredicativeTruncation.vo | |
| 9249 ./Diagrams/ParallelPair.vo | |
| 9208 ./HIT/unique_choice.vo | |
| 9201 ./Categories/DependentProduct.vo | |
| 9135 ./Basics/Utf8.vo | |
| 9034 ./Categories/ExponentialLaws.vo | |
| 9029 ./Diagrams/Sequence.vo | |
| 9020 ./Basics/Nat.vo | |
| 8908 ./Categories/Profunctor.vo | |
| 8887 ./Categories/SetCategory/Functors/SetProp.vo | |
| 8752 ./Categories/FunctorCategory/Dual.vo | |
| 8708 ./Algebra/Congruence.vo | |
| 8664 ./Equiv/BiInv.vo | |
| 8618 ./Categories/NaturalTransformation/Composition/Functorial.vo | |
| 8481 ./Categories/GroupoidCategory/Dual.vo | |
| 8333 ./Spaces/Cantor.vo | |
| 8320 ./Categories/Category/Utf8.vo | |
| 8296 ./Categories/Category/Pi.vo | |
| 8253 ./HIT/Interval.vo | |
| 8027 ./Categories/Category/Univalent.vo | |
| 8006 ./Categories/FunctorCategory/Core.vo | |
| 7903 ./Categories/Grothendieck.vo | |
| 7889 ./Tactics/BinderApply.vo | |
| 7869 ./Classes/implementations/family_prod.vo | |
| 7841 ./HIT/SetCone.vo | |
| 7811 ./WildCat/EmptyCat.vo | |
| 7810 ./Categories/Profunctor/Representable.vo | |
| 7776 ./Categories/Adjoint/Utf8.vo | |
| 7632 ./Modalities/Identity.vo | |
| 7566 ./ExcludedMiddle.vo | |
| 7560 ./Modalities/Notnot.vo | |
| 7487 ./Basics/Datatypes.vo | |
| 7406 ./Diagrams/Span.vo | |
| 7236 ./Categories/SetCategory/Functors.vo | |
| 7234 ./Spaces/Finite.vo | |
| 7151 ./Categories/CategoryOfGroupoids.vo | |
| 7065 ./Categories/Adjoint/Dual.vo | |
| 7051 ./Categories/NaturalTransformation/Notations.vo | |
| 6903 ./Categories/Adjoint/Notations.vo | |
| 6776 ./Categories/SetCategory/Core.vo | |
| 6469 ./Categories/InitialTerminalCategory/Notations.vo | |
| 6454 ./Types/Empty.vo | |
| 6454 ./Categories/Adjoint/Functorial.vo | |
| 6389 ./Basics/Numeral.vo | |
| 6377 ./Categories/Comma/Utf8.vo | |
| 6108 ./Limits/Equalizer.vo | |
| 6048 ./Categories/Profunctor/Core.vo | |
| 6023 ./Categories/Category/Dual.vo | |
| 6016 ./Truncations.vo | |
| 6001 ./Categories/Category/Notations.vo | |
| 5948 ./Categories/Profunctor/Identity.vo | |
| 5854 ./Categories/Adjoint/Identity.vo | |
| 5848 ./WildCat.vo | |
| 5842 ./Spaces/Nat.vo | |
| 5696 ./Categories/NaturalTransformation/Dual.vo | |
| 5659 ./Categories/Functor/Composition/Core.vo | |
| 5530 ./Tactics/EvalIn.vo | |
| 5365 ./Categories/Profunctor/Utf8.vo | |
| 5286 ./Categories/FunctorCategory/Notations.vo | |
| 5203 ./Categories/Functor/Dual.vo | |
| 5074 ./Categories/Profunctor/Notations.vo | |
| 4958 ./Categories/Comma/Notations.vo | |
| 4654 ./Categories/Category/Subcategory.vo | |
| 4620 ./Metatheory/IntervalImpliesFunext.vo | |
| 4591 ./Spaces/Finite/Tactics.vo | |
| 4574 ./Categories/Category/Subcategory/Full.vo | |
| 4471 ./Metatheory/Core.vo | |
| 4381 ./Categories/Adjoint/Core.vo | |
| 4338 ./WildCat/UnitCat.vo | |
| 4302 ./Categories/Structure/Utf8.vo | |
| 4245 ./Categories/DiscreteCategory.vo | |
| 4196 ./Categories/Category/Subcategory/Wide.vo | |
| 4008 ./Categories/Category/Strict.vo | |
| 3791 ./PropResizing/PropResizing.vo | |
| 3419 ./Spaces/Int.vo | |
| 3384 ./Categories/Structure/Notations.vo | |
| 3294 ./Types.vo | |
| 3280 ./Basics/Logic.vo | |
| 2988 ./Diagrams/Graph.vo | |
| 2972 ./Axioms/Univalence.vo | |
| 2950 ./Cubical.vo | |
| 2935 ./Utf8Minimal.vo | |
| 2923 ./Misc.vo | |
| 2398 ./Categories/Functor/Identity.vo | |
| 2178 ./Spaces/Pos.vo | |
| 2155 ./Basics.vo | |
| 1897 ./Tactics/Nameless.vo | |
| 1412 ./Axioms/Funext.vo |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment