Skip to content

Instantly share code, notes, and snippets.

@SkySkimmer

SkySkimmer/out.log

Created July 5, 2017 10:32
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save SkySkimmer/7d0da71155be7f1dfaf3a50e7dc64fd0 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save SkySkimmer/7d0da71155be7f1dfaf3a50e7dc64fd0 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
out.log
After | File Name | Before || Change
--------------------------------------------------------------------------------------------
5m00.32s | Total | 5m33.52s || -0m33.20s
--------------------------------------------------------------------------------------------
0m42.07s | Spaces/BAut/Bool | 0m50.32s || -0m08.25s
0m21.63s | Categories/Category/Sigma/Univalent | 0m24.02s || -0m02.39s
0m11.69s | Algebra/ooGroup | 0m14.13s || -0m02.44s
0m08.02s | Spaces/Finite | 0m10.33s || -0m02.31s
0m08.02s | Spaces/BAut/Rigid | 0m09.30s || -0m01.28s
0m07.28s | Spaces/BAut | 0m09.05s || -0m01.77s
0m06.60s | HIT/Colimits/Flattening | 0m08.06s || -0m01.46s
0m05.72s | Spaces/No | 0m06.84s || -0m01.12s
0m11.86s | Comodalities/CoreflectiveSubuniverse | 0m12.16s || -0m00.30s
0m09.93s | contrib/Freudenthal | 0m10.06s || -0m00.13s
0m08.97s | Modalities/ReflectiveSubuniverse | 0m09.96s || -0m00.99s
0m08.10s | Pointed | 0m08.72s || -0m00.62s
0m06.36s | Idempotents | 0m06.39s || -0m00.02s
0m06.20s | Categories/Adjoint/Pointwise | 0m06.27s || -0m00.06s
0m05.56s | Modalities/Lex | 0m05.60s || -0m00.04s
0m05.03s | Modalities/Topological | 0m04.60s || +0m00.43s
0m04.57s | Categories/Adjoint/Functorial/Laws | 0m04.72s || -0m00.14s
0m04.56s | Categories/ExponentialLaws/Law2/Law | 0m04.51s || +0m00.04s
0m03.65s | Categories/ExponentialLaws/Law3/Law | 0m03.65s || +0m00.00s
0m03.61s | Spaces/Universe | 0m04.22s || -0m00.60s
0m03.37s | HIT/V | 0m04.25s || -0m00.87s
0m03.05s | Categories/ExponentialLaws/Law4/Law | 0m03.06s || -0m00.01s
0m02.93s | Modalities/Fracture | 0m03.37s || -0m00.43s
0m02.75s | Modalities/Open | 0m02.70s || +0m00.04s
0m02.63s | HIT/Spheres | 0m03.20s || -0m00.57s
0m02.43s | Categories/Category/Paths | 0m02.54s || -0m00.10s
0m02.42s | HIT/Colimits/Pushout | 0m03.28s || -0m00.85s
0m02.41s | Categories/LaxComma/CoreLaws | 0m02.40s || +0m00.01s
0m02.32s | HIT/FreeIntQuotient | 0m02.73s || -0m00.41s
0m02.31s | Spaces/BAut/Cantor | 0m02.55s || -0m00.23s
0m02.23s | HIT/Coeq | 0m02.27s || -0m00.04s
0m02.09s | PropResizing/Nat | 0m02.14s || -0m00.05s
0m02.01s | contrib/HoTTBookExercises | 0m02.02s || -0m00.01s
0m01.90s | HIT/Suspension | 0m02.14s || -0m00.24s
0m01.86s | Categories/Comma/ProjectionFunctors | 0m01.92s || -0m00.05s
0m01.83s | Factorization | 0m02.24s || -0m00.41s
0m01.70s | Types/Universe | 0m01.66s || +0m00.04s
0m01.69s | Algebra/Aut | 0m02.14s || -0m00.45s
0m01.64s | Spaces/BAut/Bool/IncoherentIdempotent | 0m01.42s || +0m00.21s
0m01.58s | Modalities/Modality | 0m01.86s || -0m00.28s
0m01.55s | HIT/Connectedness | 0m01.92s || -0m00.36s
0m01.45s | Categories/Comma/Functorial | 0m01.61s || -0m00.16s
0m01.31s | Categories/GroupoidCategory/Morphisms | 0m01.15s || +0m00.16s
0m01.26s | contrib/HoTTBook | 0m01.29s || -0m00.03s
0m01.22s | Categories/Grothendieck/ToSet/Morphisms | 0m01.03s || +0m00.18s
0m01.22s | HIT/Truncations | 0m01.54s || -0m00.32s
0m01.18s | Types/Sigma | 0m01.29s || -0m00.11s
0m01.16s | Categories/Functor/Paths | 0m01.36s || -0m00.20s
0m01.13s | Categories/Category/Morphisms | 0m01.43s || -0m00.30s
0m01.12s | HIT/Colimits/Colimit | 0m01.50s || -0m00.37s
0m01.04s | Tactics/EquivalenceInduction | 0m01.18s || -0m00.13s
0m00.98s | Types/Sum | 0m01.06s || -0m00.08s
0m00.93s | HIT/epi | 0m01.13s || -0m00.19s
0m00.86s | Basics/PathGroupoids | 0m00.83s || +0m00.03s
0m00.85s | Categories/ExponentialLaws/Law1/Law | 0m00.87s || -0m00.02s
0m00.84s | HIT/Colimits/Colimit_Sigma | 0m01.11s || -0m00.27s
0m00.83s | Fibrations | 0m00.92s || -0m00.09s
0m00.82s | HIT/Join | 0m00.82s || +0m00.00s
0m00.78s | Modalities/Localization | 0m00.89s || -0m00.10s
0m00.78s | Categories/Grothendieck/ToSet/Univalent | 0m00.72s || +0m00.06s
0m00.78s | Modalities/Closed | 0m00.74s || +0m00.04s
0m00.76s | Categories/Functor/Composition/Functorial/Attributes | 0m00.75s || +0m00.01s
0m00.75s | HIT/Flattening | 0m00.96s || -0m00.20s
0m00.74s | Tests | 0m00.90s || -0m00.16s
0m00.72s | HIT/quotient | 0m00.87s || -0m00.15s
0m00.71s | Modalities/Accessible | 0m00.84s || -0m00.13s
0m00.70s | Categories/Adjoint/Composition/AssociativityLaw | 0m00.70s || +0m00.00s
0m00.69s | HoTT | 0m00.77s || -0m00.08s
0m00.68s | Categories/Grothendieck/PseudofunctorToCat | 0m00.70s || -0m00.01s
0m00.68s | Categories/Functor/Sum | 0m00.65s || +0m00.03s
0m00.67s | Constant | 0m00.61s || +0m00.06s
0m00.66s | Categories/ExponentialLaws/Law4/Functors | 0m00.67s || -0m00.01s
0m00.64s | DProp | 0m00.80s || -0m00.16s
0m00.56s | HIT/TwoSphere | 0m00.75s || -0m00.18s
0m00.55s | Categories/Adjoint/HomCoercions | 0m00.54s || +0m00.01s
0m00.54s | Categories/Pseudofunctor/RewriteLaws | 0m00.53s || +0m00.01s
0m00.51s | Categories/ChainCategory | 0m00.47s || +0m00.04s
0m00.50s | Categories/Functor/Composition/Laws | 0m00.50s || +0m00.00s
0m00.50s | Types/Paths | 0m00.55s || -0m00.05s
0m00.48s | Modalities/Nullification | 0m00.58s || -0m00.09s
0m00.48s | EquivalenceVarieties | 0m00.56s || -0m00.08s
0m00.47s | Categories/Adjoint/Composition/IdentityLaws | 0m00.51s || -0m00.04s
0m00.47s | HIT/Colimits/Coequalizer | 0m00.55s || -0m00.08s
0m00.46s | Categories/Pseudofunctor/FromFunctor | 0m00.46s || +0m00.00s
0m00.46s | Basics/Equivalences | 0m00.39s || +0m00.07s
0m00.46s | Categories/Yoneda | 0m00.49s || -0m00.02s
0m00.46s | Categories/Pseudofunctor/Identity | 0m00.50s || -0m00.03s
0m00.46s | TruncType | 0m00.49s || -0m00.02s
0m00.43s | Categories | 0m00.44s || -0m00.01s
0m00.42s | Categories/UniversalProperties | 0m00.39s || +0m00.02s
0m00.41s | Categories/Comma/InducedFunctors | 0m00.42s || -0m00.01s
0m00.41s | Categories/Functor/Pointwise/Properties | 0m00.42s || -0m00.01s
0m00.41s | Categories/Category/Sigma/OnMorphisms | 0m00.48s || -0m00.07s
0m00.40s | Types/Prod | 0m00.42s || -0m00.01s
0m00.40s | Categories/LaxComma/Core | 0m00.39s || +0m00.01s
0m00.39s | HIT/Pushout | 0m00.43s || -0m00.03s
0m00.38s | Categories/Comma/Core | 0m00.37s || +0m00.01s
0m00.38s | Categories/Comma/Dual | 0m00.39s || -0m00.01s
0m00.36s | Categories/Adjoint/Composition/Core | 0m00.37s || -0m00.01s
0m00.36s | Types/Equiv | 0m00.40s || -0m00.04s
0m00.36s | Categories/Functor/Attributes | 0m00.35s || +0m00.01s
0m00.36s | HIT/Colimits/Diagram | 0m00.36s || +0m00.00s
0m00.35s | Categories/LaxComma/CoreParts | 0m00.37s || -0m00.02s
0m00.34s | Categories/Adjoint/UnitCounitCoercions | 0m00.37s || -0m00.02s
0m00.33s | HIT/Circle | 0m00.44s || -0m00.10s
0m00.31s | Modalities/Identity | 0m00.36s || -0m00.04s
0m00.31s | Extensions | 0m00.32s || -0m00.01s
0m00.31s | Categories/ProductLaws | 0m00.28s || +0m00.02s
0m00.30s | Categories/SetCategory/Morphisms | 0m00.30s || +0m00.00s
0m00.30s | Categories/SemiSimplicialSets | 0m00.30s || +0m00.00s
0m00.29s | Categories/ExponentialLaws/Law0 | 0m00.32s || -0m00.03s
0m00.27s | Categories/SimplicialSets | 0m00.24s || +0m00.03s
0m00.27s | Categories/Functor/Prod/Universal | 0m00.27s || +0m00.00s
0m00.26s | Categories/HomotopyPreCategory | 0m00.22s || +0m00.04s
0m00.26s | Pullback | 0m00.29s || -0m00.02s
0m00.25s | Categories/Adjoint/UniversalMorphisms/Core | 0m00.19s || +0m00.06s
0m00.25s | HIT/Colimits/CommutativeSquares | 0m00.28s || -0m00.03s
0m00.25s | Categories/Category/Sigma/Core | 0m00.28s || -0m00.03s
0m00.25s | Categories/InitialTerminalCategory/Pseudofunctors | 0m00.24s || +0m00.01s
0m00.25s | Categories/GroupoidCategory/Dual | 0m00.21s || +0m00.04s
0m00.25s | Categories/Category/Sum | 0m00.34s || -0m00.09s
0m00.24s | Categories/FundamentalPreGroupoidCategory | 0m00.24s || +0m00.00s
0m00.24s | Spaces/Nat | 0m00.26s || -0m00.02s
0m00.24s | Categories/Adjoint/Functorial/Core | 0m00.21s || +0m00.03s
0m00.24s | Types/Forall | 0m00.28s || -0m00.04s
0m00.23s | Categories/Notations | 0m00.21s || +0m00.02s
0m00.23s | Categories/DualFunctor | 0m00.22s || +0m00.01s
0m00.22s | Categories/NaturalTransformation/Isomorphisms | 0m00.24s || -0m00.01s
0m00.22s | Categories/ExponentialLaws/Law1/Functors | 0m00.22s || +0m00.00s
0m00.22s | Categories/Structure/IdentityPrinciple | 0m00.20s || +0m00.01s
0m00.22s | Categories/Adjoint/Paths | 0m00.23s || -0m00.01s
0m00.21s | Spectra/Coinductive | 0m00.24s || -0m00.03s
0m00.20s | Categories/NaturalTransformation/Paths | 0m00.20s || +0m00.00s
0m00.20s | Categories/Functor | 0m00.19s || +0m00.01s
0m00.19s | Categories/Functor/Utf8 | 0m00.20s || -0m00.01s
0m00.19s | Categories/Limits/Core | 0m00.18s || +0m00.01s
0m00.19s | Categories/FunctorCategory/Utf8 | 0m00.19s || +0m00.00s
0m00.19s | Categories/Utf8 | 0m00.19s || +0m00.00s
0m00.18s | Algebra/ooAction | 0m00.20s || -0m00.02s
0m00.18s | Categories/Functor/Composition | 0m00.16s || +0m00.01s
0m00.17s | HIT/TruncImpliesFunext | 0m00.22s || -0m00.04s
0m00.17s | Categories/Functor/Notations | 0m00.17s || +0m00.00s
0m00.17s | Types/Wtype | 0m00.19s || -0m00.01s
0m00.17s | HIT/iso | 0m00.19s || -0m00.01s
0m00.17s | ObjectClassifier | 0m00.17s || +0m00.00s
0m00.16s | Categories/InitialTerminalCategory/Functors | 0m00.16s || +0m00.00s
0m00.16s | Categories/FunctorCategory/Morphisms | 0m00.17s || -0m00.01s
0m00.16s | HIT/unique_choice | 0m00.18s || -0m00.01s
0m00.16s | HIT/Colimits | 0m00.18s || -0m00.01s
0m00.16s | Spectra/Spectrum | 0m00.24s || -0m00.07s
0m00.16s | Categories/Functor/Composition/Functorial | 0m00.17s || -0m00.01s
0m00.15s | Modalities/Notnot | 0m00.15s || +0m00.00s
0m00.15s | UnivalenceImpliesFunext | 0m00.15s || +0m00.00s
0m00.15s | Categories/Functor/Prod/Core | 0m00.13s || +0m00.01s
0m00.15s | Categories/NaturalTransformation/Utf8 | 0m00.18s || -0m00.03s
0m00.15s | Utf8 | 0m00.24s || -0m00.09s
0m00.14s | Categories/PseudonaturalTransformation/Core | 0m00.12s || +0m00.02s
0m00.14s | Categories/Grothendieck/ToSet/Core | 0m00.16s || -0m00.01s
0m00.14s | Categories/Functor/Composition/Functorial/Core | 0m00.14s || +0m00.00s
0m00.14s | Spaces/Int | 0m00.16s || -0m00.01s
0m00.13s | Categories/FunctorCategory/Dual | 0m00.11s || +0m00.02s
0m00.13s | Categories/Category/Sigma/OnObjects | 0m00.15s || -0m00.01s
0m00.13s | Categories/Adjoint/Functorial/Parts | 0m00.13s || +0m00.00s
0m00.13s | Categories/NaturalTransformation/Composition/Laws | 0m00.15s || -0m00.01s
0m00.13s | EquivGroupoids | 0m00.15s || -0m00.01s
0m00.13s | Categories/Pseudofunctor/Core | 0m00.11s || +0m00.02s
0m00.12s | Categories/NaturalTransformation/Prod | 0m00.12s || +0m00.00s
0m00.12s | Categories/Structure/Core | 0m00.12s || +0m00.00s
0m00.12s | Categories/Limits/Functors | 0m00.12s || +0m00.00s
0m00.12s | Types/Arrow | 0m00.14s || -0m00.02s
0m00.12s | Tactics/RewriteModuloAssociativity | 0m00.12s || +0m00.00s
0m00.12s | Categories/Category/Objects | 0m00.09s || +0m00.03s
0m00.12s | Categories/HomFunctor | 0m00.10s || +0m00.01s
0m00.12s | HIT/Colimits/MappingTelescope | 0m00.13s || -0m00.01s
0m00.11s | Categories/Functor/Pointwise/Core | 0m00.12s || -0m00.00s
0m00.11s | Basics/UniverseLevel | 0m00.10s || +0m00.00s
0m00.11s | HSet | 0m00.12s || -0m00.00s
0m00.11s | Categories/Comma/Projection | 0m00.10s || +0m00.00s
0m00.11s | Tactics | 0m00.12s || -0m00.00s
0m00.11s | Categories/NaturalTransformation/Pointwise | 0m00.10s || +0m00.00s
0m00.11s | Categories/NatCategory | 0m00.08s || +0m00.03s
0m00.10s | Basics/Overture | 0m00.14s || -0m00.04s
0m00.10s | Categories/ExponentialLaws/Law2/Functors | 0m00.14s || -0m00.04s
0m00.10s | Categories/CategoryOfSections/Core | 0m00.09s || +0m00.01s
0m00.10s | Categories/Functor/Prod/Functorial | 0m00.12s || -0m00.01s
0m00.10s | Categories/KanExtensions/Functors | 0m00.10s || +0m00.00s
0m00.10s | Types/Bool | 0m00.12s || -0m00.01s
0m00.10s | Categories/Cat/Core | 0m00.11s || -0m00.00s
0m00.10s | Categories/Adjoint/UnitCounit | 0m00.10s || +0m00.00s
0m00.09s | Categories/Adjoint | 0m00.08s || +0m00.00s
0m00.09s | Categories/Category/Prod | 0m00.16s || -0m00.07s
0m00.09s | Categories/FunctorCategory/Functorial | 0m00.09s || +0m00.00s
0m00.09s | PropResizing/Truncations | 0m00.10s || -0m00.01s
0m00.09s | Categories/InitialTerminalCategory/NaturalTransformations | 0m00.08s || +0m00.00s
0m00.09s | Basics/Decidable | 0m00.08s || +0m00.00s
0m00.08s | Categories/LaxComma | 0m00.10s || -0m00.02s
0m00.08s | Categories/IndiscreteCategory | 0m00.11s || -0m00.03s
0m00.08s | Categories/Category/Pi | 0m00.08s || +0m00.00s
0m00.08s | Basics/Contractible | 0m00.08s || +0m00.00s
0m00.08s | Categories/NaturalTransformation/Sum | 0m00.06s || +0m00.02s
0m00.08s | Categories/KanExtensions/Core | 0m00.12s || -0m00.03s
0m00.08s | Categories/Cat | 0m00.06s || +0m00.02s
0m00.08s | Categories/Adjoint/Hom | 0m00.09s || -0m00.00s
0m00.08s | HProp | 0m00.14s || -0m00.06s
0m00.08s | Categories/Limits | 0m00.07s || +0m00.00s
0m00.07s | Categories/NaturalTransformation/Identity | 0m00.05s || +0m00.02s
0m00.07s | Functorish | 0m00.08s || -0m00.00s
0m00.07s | Categories/Adjoint/Utf8 | 0m00.06s || +0m00.01s
0m00.07s | Categories/Cat/Morphisms | 0m00.08s || -0m00.00s
0m00.07s | Basics/FunextVarieties | 0m00.06s || +0m00.01s
0m00.07s | Categories/ExponentialLaws/Law3/Functors | 0m00.09s || -0m00.01s
0m00.07s | Categories/LaxComma/Utf8 | 0m00.07s || +0m00.00s
0m00.07s | Types/Record | 0m00.10s || -0m00.03s
0m00.07s | Categories/Grothendieck/ToCat | 0m00.08s || -0m00.00s
0m00.06s | ExcludedMiddle | 0m00.06s || +0m00.00s
0m00.06s | Categories/Profunctor | 0m00.03s || +0m00.03s
0m00.06s | Categories/Category/Dual | 0m00.09s || -0m00.03s
0m00.06s | Categories/Category | 0m00.06s || +0m00.00s
0m00.06s | Categories/NaturalTransformation/Composition/Functorial | 0m00.06s || +0m00.00s
0m00.06s | Basics/Trunc | 0m00.06s || +0m00.00s
0m00.06s | Categories/SetCategory/Core | 0m00.07s || -0m00.01s
0m00.06s | coq/Init/Peano | 0m00.06s || +0m00.00s
0m00.06s | Categories/FunctorCategory | 0m00.04s || +0m00.01s
0m00.06s | Categories/InitialTerminalCategory/Core | 0m00.06s || +0m00.00s
0m00.06s | Categories/Grothendieck/ToSet | 0m00.05s || +0m00.00s
0m00.06s | Categories/Comma | 0m00.07s || -0m00.01s
0m00.06s | Categories/Adjoint/Composition | 0m00.04s || +0m00.01s
0m00.06s | Categories/Category/Notations | 0m00.06s || +0m00.00s
0m00.06s | Categories/InitialTerminalCategory/Notations | 0m00.05s || +0m00.00s
0m00.06s | Categories/GroupoidCategory/Core | 0m00.08s || -0m00.02s
0m00.06s | Categories/SetCategory | 0m00.04s || +0m00.01s
0m00.06s | Categories/CategoryOfGroupoids | 0m00.06s || +0m00.00s
0m00.06s | Categories/NaturalTransformation/Composition/Core | 0m00.10s || -0m00.04s
0m00.06s | Categories/Functor/Dual | 0m00.05s || +0m00.00s
0m00.06s | Categories/Profunctor/Representable | 0m00.06s || +0m00.00s
0m00.06s | Categories/InitialTerminalCategory | 0m00.05s || +0m00.00s
0m00.06s | Categories/NaturalTransformation/Notations | 0m00.06s || +0m00.00s
0m00.06s | HIT/Colimits/Colimit_Prod | 0m00.09s || -0m00.03s
0m00.06s | Categories/SetCategory/Functors/SetProp | 0m00.08s || -0m00.02s
0m00.06s | Categories/Category/Utf8 | 0m00.06s || +0m00.00s
0m00.06s | Categories/Adjoint/UniversalMorphisms | 0m00.04s || +0m00.01s
0m00.06s | Categories/Pseudofunctor | 0m00.06s || +0m00.00s
0m00.06s | Categories/Structure | 0m00.04s || +0m00.01s
0m00.06s | Categories/PseudonaturalTransformation | 0m00.06s || +0m00.00s
0m00.06s | Types | 0m00.06s || +0m00.00s
0m00.06s | Categories/Profunctor/Utf8 | 0m00.04s || +0m00.01s
0m00.05s | Categories/Functor/Pointwise | 0m00.04s || +0m00.01s
0m00.05s | Categories/Category/Sigma | 0m00.06s || -0m00.00s
0m00.05s | Categories/Functor/Prod | 0m00.05s || +0m00.00s
0m00.05s | coq/Init/Specif | 0m00.03s || +0m00.02s
0m00.05s | Categories/LaxComma/Notations | 0m00.06s || -0m00.00s
0m00.05s | Categories/Adjoint/Notations | 0m00.04s || +0m00.01s
0m00.05s | Categories/Adjoint/Dual | 0m00.06s || -0m00.00s
0m00.05s | Categories/KanExtensions | 0m00.06s || -0m00.00s
0m00.05s | Categories/Comma/Notations | 0m00.05s || +0m00.00s
0m00.05s | Categories/DependentProduct | 0m00.06s || -0m00.00s
0m00.05s | Categories/Grothendieck | 0m00.06s || -0m00.00s
0m00.05s | Spaces/Cantor | 0m00.06s || -0m00.00s
0m00.05s | Categories/NaturalTransformation/Composition | 0m00.04s || +0m00.01s
0m00.05s | Categories/Adjoint/Composition/LawsTactic | 0m00.06s || -0m00.00s
0m00.05s | Categories/NaturalTransformation | 0m00.04s || +0m00.01s
0m00.05s | Categories/ExponentialLaws | 0m00.04s || +0m00.01s
0m00.05s | Categories/NaturalTransformation/Core | 0m00.05s || +0m00.00s
0m00.05s | Categories/ExponentialLaws/Tactics | 0m00.04s || +0m00.01s
0m00.05s | Categories/Category/Univalent | 0m00.07s || -0m00.02s
0m00.05s | HIT/Interval | 0m00.06s || -0m00.00s
0m00.05s | Categories/FunctorCategory/Core | 0m00.06s || -0m00.00s
0m00.05s | Categories/ExponentialLaws/Law1 | 0m00.04s || +0m00.01s
0m00.05s | Categories/ExponentialLaws/Law3 | 0m00.06s || -0m00.00s
0m00.04s | Categories/Adjoint/Core | 0m00.04s || +0m00.00s
0m00.04s | Conjugation | 0m00.06s || -0m00.01s
0m00.04s | Categories/Adjoint/Functorial | 0m00.05s || -0m00.01s
0m00.04s | Categories/Profunctor/Core | 0m00.05s || -0m00.01s
0m00.04s | PropResizing/PropResizing | 0m00.03s || +0m00.01s
0m00.04s | Categories/Adjoint/Identity | 0m00.04s || +0m00.00s
0m00.04s | Types/Unit | 0m00.05s || -0m00.01s
0m00.04s | Misc | 0m00.06s || -0m00.01s
0m00.04s | Categories/Comma/Utf8 | 0m00.06s || -0m00.01s
0m00.04s | Categories/Functor/Composition/Core | 0m00.05s || -0m00.01s
0m00.04s | Categories/Category/Subcategory | 0m00.03s || +0m00.01s
0m00.04s | HIT/IntervalImpliesFunext | 0m00.03s || +0m00.01s
0m00.04s | Categories/Structure/Utf8 | 0m00.04s || +0m00.00s
0m00.04s | Categories/Structure/Notations | 0m00.05s || -0m00.01s
0m00.04s | Categories/Category/Subcategory/Full | 0m00.04s || +0m00.00s
0m00.04s | Categories/Profunctor/Notations | 0m00.03s || +0m00.01s
0m00.04s | Categories/Category/Core | 0m00.07s || -0m00.03s
0m00.04s | Categories/CategoryOfSections | 0m00.03s || +0m00.01s
0m00.04s | Categories/GroupoidCategory | 0m00.04s || +0m00.00s
0m00.04s | Categories/NaturalTransformation/Dual | 0m00.04s || +0m00.00s
0m00.04s | NullHomotopy | 0m00.04s || +0m00.00s
0m00.04s | Categories/Category/Subcategory/Wide | 0m00.05s || -0m00.01s
0m00.04s | Categories/Profunctor/Identity | 0m00.04s || +0m00.00s
0m00.04s | coq/Init/Logic_Type | 0m00.04s || +0m00.00s
0m00.04s | Categories/ExponentialLaws/Law2 | 0m00.04s || +0m00.00s
0m00.04s | Categories/SetCategory/Functors | 0m00.04s || +0m00.00s
0m00.03s | coq/Init/Datatypes | 0m00.03s || +0m00.00s
0m00.03s | Basics/Notations | 0m00.02s || +0m00.00s
0m00.03s | Types/Empty | 0m00.04s || -0m00.01s
0m00.03s | Categories/DiscreteCategory | 0m00.04s || -0m00.01s
0m00.03s | Categories/Category/Strict | 0m00.03s || +0m00.00s
0m00.03s | Categories/Functor/Core | 0m00.05s || -0m00.02s
0m00.03s | Categories/FunctorCategory/Notations | 0m00.03s || +0m00.00s
0m00.03s | Tactics/BinderApply | 0m00.05s || -0m00.02s
0m00.03s | coq/Program/Tactics | 0m00.02s || +0m00.00s
0m00.03s | Categories/ExponentialLaws/Law4 | 0m00.05s || -0m00.02s
0m00.02s | Categories/Functor/Identity | 0m00.04s || -0m00.02s
0m00.02s | Tactics/EvalIn | 0m00.04s || -0m00.02s
0m00.02s | coq/Unicode/Utf8_core | 0m00.01s || +0m00.01s
0m00.02s | coq/Init/Prelude | 0m00.02s || +0m00.00s
0m00.02s | UnivalenceAxiom | 0m00.04s || -0m00.02s
0m00.02s | Basics | 0m00.03s || -0m00.00s
0m00.02s | FunextAxiom | 0m00.02s || +0m00.00s
0m00.01s | coq/Init/Notations | 0m00.01s || +0m00.00s
0m00.01s | coq/Init/Logic | 0m00.01s || +0m00.00s
0m00.01s | Basics/Utf8 | 0m00.04s || -0m00.03s
0m00.01s | coq/Bool/Bool | 0m00.02s || -0m00.01s
0m00.00s | coq/Unicode/Utf8 | 0m00.02s || -0m00.02s
0m00.00s | coq/Init/Tactics | 0m00.01s || -0m00.01s
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment