TEXT   35
time build of both
Guest on 26th May 2023 01:08:48 AM


  1. After    | File Name                                                 | Before   || Change  
  2. --------------------------------------------------------------------------------------------
  3. 3m00.31s | Total                                                     | 3m20.65s || -0m20.33s
  4. --------------------------------------------------------------------------------------------
  5. 0m02.93s | HIT/V                                                     | 0m09.91s || -0m06.98s
  6. 0m15.10s | Spaces/BAut/Bool                                          | 0m18.24s || -0m03.13s
  7. 0m01.18s | contrib/HoTTBook                                          | 0m03.37s || -0m02.19s
  8. 0m01.49s | Spaces/BAut/Bool/IncoherentIdempotent                     | 0m03.35s || -0m01.86s
  9. 0m10.75s | Algebra/ooGroup                                           | 0m10.32s || +0m00.42s
  10. 0m07.43s | Modalities/ReflectiveSubuniverse                          | 0m07.73s || -0m00.30s
  11. 0m06.79s | Spaces/Finite                                             | 0m06.08s || +0m00.71s
  12. 0m05.77s | Categories/Adjoint/Pointwise                              | 0m06.26s || -0m00.49s
  13. 0m05.74s | Idempotents                                               | 0m05.63s || +0m00.11s
  14. 0m05.52s | contrib/Freudenthal                                       | 0m06.48s || -0m00.96s
  15. 0m05.39s | Categories/Category/Sigma/Univalent                       | 0m06.04s || -0m00.65s
  16. 0m05.29s | Spaces/BAut                                               | 0m05.53s || -0m00.24s
  17. 0m05.11s | Spaces/No                                                 | 0m05.37s || -0m00.25s
  18. 0m04.22s | Categories/Adjoint/Functorial/Laws                        | 0m04.10s || +0m00.12s
  19. 0m04.16s | Categories/ExponentialLaws/Law2/Law                       | 0m04.88s || -0m00.71s
  20. 0m03.86s | Modalities/Lex                                            | 0m04.16s || -0m00.30s
  21. 0m03.40s | Categories/ExponentialLaws/Law3/Law                       | 0m04.29s || -0m00.89s
  22. 0m03.33s | Pointed                                                   | 0m02.86s || +0m00.47s
  23. 0m02.86s | Categories/ExponentialLaws/Law4/Law                       | 0m03.74s || -0m00.88s
  24. 0m02.32s | HIT/Spheres                                               | 0m03.08s || -0m00.76s
  25. 0m02.25s | Categories/Category/Paths                                 | 0m02.35s || -0m00.10s
  26. 0m02.21s | Categories/LaxComma/CoreLaws                              | 0m02.42s || -0m00.20s
  27. 0m02.09s | Modalities/Modality                                       | 0m02.08s || +0m00.00s
  28. 0m02.06s | HIT/FreeIntQuotient                                       | 0m02.07s || -0m00.00s
  29. 0m01.96s | HIT/Coeq                                                  | 0m01.86s || +0m00.09s
  30. 0m01.74s | Categories/Comma/ProjectionFunctors                       | 0m02.42s || -0m00.68s
  31. 0m01.74s | HIT/Suspension                                            | 0m01.78s || -0m00.04s
  32. 0m01.72s | Spaces/BAut/Cantor                                        | 0m02.13s || -0m00.40s
  33. 0m01.66s | Factorization                                             | 0m01.62s || +0m00.03s
  34. 0m01.63s | contrib/HoTTBookExercises                                 | 0m01.43s || +0m00.19s
  35. 0m01.51s | Comodalities/CoreflectiveSubuniverse                      | 0m01.16s || +0m00.35s
  36. 0m01.37s | Modalities/Fracture                                       | 0m01.50s || -0m00.12s
  37. 0m01.36s | Types/Universe                                            | 0m01.82s || -0m00.46s
  38. 0m01.35s | HIT/Connectedness                                         | 0m01.23s || +0m00.12s
  39. 0m01.34s | Categories/Comma/Functorial                               | 0m01.48s || -0m00.13s
  40. 0m01.08s | HIT/Truncations                                           | 0m00.90s || +0m00.18s
  41. 0m01.06s | Categories/GroupoidCategory/Morphisms                     | 0m01.34s || -0m00.28s
  42. 0m01.00s | Categories/Category/Morphisms                             | 0m00.94s || +0m00.06s
  43. 0m00.95s | Tactics/EquivalenceInduction                              | 0m00.99s || -0m00.04s
  44. 0m00.94s | Types/Sigma                                               | 0m00.92s || +0m00.01s
  45. 0m00.94s | Categories/Grothendieck/ToSet/Morphisms                   | 0m00.88s || +0m00.05s
  46. 0m00.81s | HIT/epi                                                   | 0m00.79s || +0m00.02s
  47. 0m00.80s | Algebra/Aut                                               | 0m00.76s || +0m00.04s
  48. 0m00.79s | Categories/ExponentialLaws/Law1/Law                       | 0m00.82s || -0m00.02s
  49. 0m00.78s | Modalities/Open                                           | 0m00.62s || +0m00.16s
  50. 0m00.78s | Types/Sum                                                 | 0m01.03s || -0m00.25s
  51. 0m00.75s | Categories/Functor/Composition/Functorial/Attributes      | 0m00.68s || +0m00.06s
  52. 0m00.70s | Modalities/Closed                                         | 0m00.60s || +0m00.09s
  53. 0m00.68s | HIT/Flattening                                            | 0m00.78s || -0m00.09s
  54. 0m00.68s | Modalities/Topological                                    | 0m00.62s || +0m00.06s
  55. 0m00.67s | Modalities/Localization                                   | 0m00.73s || -0m00.05s
  56. 0m00.65s | Basics/PathGroupoids                                      | 0m00.66s || -0m00.01s
  57. 0m00.65s | Categories/Adjoint/Composition/AssociativityLaw           | 0m00.66s || -0m00.01s
  58. 0m00.65s | Categories/Grothendieck/ToSet/Univalent                   | 0m00.70s || -0m00.04s
  59. 0m00.64s | HIT/quotient                                              | 0m00.63s || +0m00.01s
  60. 0m00.62s | Modalities/Accessible                                     | 0m00.60s || +0m00.02s
  61. 0m00.61s | Categories/Grothendieck/PseudofunctorToCat                | 0m00.65s || -0m00.04s
  62. 0m00.60s | Categories/Functor/Paths                                  | 0m00.66s || -0m00.06s
  63. 0m00.60s | Categories/Functor/Sum                                    | 0m00.78s || -0m00.18s
  64. 0m00.59s | Categories/ExponentialLaws/Law4/Functors                  | 0m00.66s || -0m00.07s
  65. 0m00.59s | Tests                                                     | 0m00.56s || +0m00.02s
  66. 0m00.59s | DProp                                                     | 0m00.44s || +0m00.14s
  67. 0m00.54s | Categories/Pseudofunctor/RewriteLaws                      | 0m00.49s || +0m00.05s
  68. 0m00.53s | Categories/Adjoint/HomCoercions                           | 0m00.51s || +0m00.02s
  69. 0m00.52s | Constant                                                  | 0m00.46s || +0m00.06s
  70. 0m00.50s | HoTT                                                      | 0m00.48s || +0m00.02s
  71. 0m00.48s | HIT/TwoSphere                                             | 0m00.83s || -0m00.35s
  72. 0m00.46s | Categories/Functor/Composition/Laws                       | 0m00.48s || -0m00.01s
  73. 0m00.46s | EquivalenceVarieties                                      | 0m00.38s || +0m00.08s
  74. 0m00.45s | Categories/Adjoint/Composition/IdentityLaws               | 0m00.56s || -0m00.11s
  75. 0m00.44s | Categories/UniversalProperties                            | 0m00.36s || +0m00.08s
  76. 0m00.42s | TruncType                                                 | 0m00.36s || +0m00.06s
  77. 0m00.42s | Categories/Pseudofunctor/Identity                         | 0m00.43s || -0m00.01s
  78. 0m00.41s | Categories/Comma/InducedFunctors                          | 0m00.43s || -0m00.02s
  79. 0m00.41s | Categories/ChainCategory                                  | 0m00.31s || +0m00.09s
  80. 0m00.40s | Categories/LaxComma/Core                                  | 0m00.37s || +0m00.03s
  81. 0m00.40s | Basics/Equivalences                                       | 0m00.35s || +0m00.05s
  82. 0m00.40s | Categories/Yoneda                                         | 0m00.52s || -0m00.12s
  83. 0m00.40s | Categories/Pseudofunctor/FromFunctor                      | 0m00.44s || -0m00.03s
  84. 0m00.40s | Types/Paths                                               | 0m00.45s || -0m00.04s
  85. 0m00.37s | Categories/LaxComma/CoreParts                             | 0m00.33s || +0m00.03s
  86. 0m00.37s | Categories/Comma/Dual                                     | 0m00.31s || +0m00.06s
  87. 0m00.35s | Categories                                                | 0m00.32s || +0m00.02s
  88. 0m00.35s | Categories/Functor/Pointwise/Properties                   | 0m00.36s || -0m00.01s
  89. 0m00.34s | Categories/Comma/Core                                     | 0m00.30s || +0m00.04s
  90. 0m00.34s | Categories/Category/Sigma/OnMorphisms                     | 0m00.38s || -0m00.03s
  91. 0m00.34s | HIT/Pushout                                               | 0m00.38s || -0m00.03s
  92. 0m00.33s | Categories/Adjoint/UnitCounitCoercions                    | 0m00.29s || +0m00.04s
  93. 0m00.32s | Categories/Adjoint/Composition/Core                       | 0m00.30s || +0m00.02s
  94. 0m00.32s | Types/Prod                                                | 0m00.38s || -0m00.06s
  95. 0m00.31s | Types/Equiv                                               | 0m00.34s || -0m00.03s
  96. 0m00.29s | Categories/Functor/Attributes                             | 0m00.26s || +0m00.02s
  97. 0m00.29s | Extensions                                                | 0m00.24s || +0m00.04s
  98. 0m00.28s | Modalities/Identity                                       | 0m00.19s || +0m00.09s
  99. 0m00.27s | Categories/ProductLaws                                    | 0m00.28s || -0m00.01s
  100. 0m00.27s | HIT/Circle                                                | 0m00.27s || +0m00.00s
  101. 0m00.26s | Modalities/Nullification                                  | 0m00.26s || +0m00.00s
  102. 0m00.26s | Categories/GroupoidCategory/Dual                          | 0m00.16s || +0m00.10s
  103. 0m00.26s | Categories/ExponentialLaws/Law0                           | 0m00.27s || -0m00.01s
  104. 0m00.25s | Categories/Functor/Prod/Universal                         | 0m00.27s || -0m00.02s
  105. 0m00.24s | Categories/SemiSimplicialSets                             | 0m00.25s || -0m00.01s
  106. 0m00.23s | Categories/Adjoint/UniversalMorphisms/Core                | 0m00.23s || +0m00.00s
  107. 0m00.23s | Categories/ExponentialLaws/Law1/Functors                  | 0m00.24s || -0m00.00s
  108. 0m00.22s | Categories/FundamentalPreGroupoidCategory                 | 0m00.18s || +0m00.04s
  109. 0m00.22s | Categories/SimplicialSets                                 | 0m00.20s || +0m00.01s
  110. 0m00.22s | Categories/Category/Sigma/Core                            | 0m00.21s || +0m00.01s
  111. 0m00.22s | Categories/InitialTerminalCategory/Pseudofunctors         | 0m00.27s || -0m00.05s
  112. 0m00.22s | Categories/SetCategory/Morphisms                          | 0m00.22s || +0m00.00s
  113. 0m00.22s | Categories/Adjoint/Paths                                  | 0m00.20s || +0m00.01s
  114. 0m00.22s | Fibrations                                                | 0m00.23s || -0m00.01s
  115. 0m00.21s | Categories/Structure/IdentityPrinciple                    | 0m00.21s || +0m00.00s
  116. 0m00.21s | Categories/Adjoint/Functorial/Core                        | 0m00.20s || +0m00.00s
  117. 0m00.21s | Categories/Category/Sum                                   | 0m00.22s || -0m00.01s
  118. 0m00.20s | Types/Wtype                                               | 0m00.21s || -0m00.00s
  119. 0m00.20s | Categories/Limits/Core                                    | 0m00.18s || +0m00.02s
  120. 0m00.20s | Categories/HomotopyPreCategory                            | 0m00.18s || +0m00.02s
  121. 0m00.20s | Pullback                                                  | 0m00.21s || -0m00.00s
  122. 0m00.19s | Categories/NaturalTransformation/Isomorphisms             | 0m00.22s || -0m00.03s
  123. 0m00.19s | Spectra/Coinductive                                       | 0m00.14s || +0m00.04s
  124. 0m00.19s | Categories/DualFunctor                                    | 0m00.20s || -0m00.01s
  125. 0m00.18s | Algebra/ooAction                                          | 0m00.16s || +0m00.01s
  126. 0m00.18s | Categories/Functor/Composition/Functorial                 | 0m00.12s || +0m00.06s
  127. 0m00.18s | Spectra/Spectrum                                          | 0m00.16s || +0m00.01s
  128. 0m00.18s | Categories/NaturalTransformation/Paths                    | 0m00.17s || +0m00.00s
  129. 0m00.18s | HIT/Join                                                  | 0m00.20s || -0m00.02s
  130. 0m00.17s | Categories/PseudonaturalTransformation/Core               | 0m00.12s || +0m00.05s
  131. 0m00.16s | Categories/Notations                                      | 0m00.14s || +0m00.01s
  132. 0m00.16s | Categories/InitialTerminalCategory/Functors               | 0m00.12s || +0m00.04s
  133. 0m00.16s | UnivalenceImpliesFunext                                   | 0m00.15s || +0m00.01s
  134. 0m00.16s | Spaces/Nat                                                | 0m00.16s || +0m00.00s
  135. 0m00.15s | Categories/Utf8                                           | 0m00.20s || -0m00.05s
  136. 0m00.15s | Types/Forall                                              | 0m00.16s || -0m00.01s
  137. 0m00.14s | Modalities/Notnot                                         | 0m00.14s || +0m00.00s
  138. 0m00.14s | Categories/Functor/Notations                              | 0m00.12s || +0m00.02s
  139. 0m00.14s | HIT/iso                                                   | 0m00.18s || -0m00.03s
  140. 0m00.14s | Tactics                                                   | 0m00.10s || +0m00.04s
  141. 0m00.14s | Spaces/Int                                                | 0m00.11s || +0m00.03s
  142. 0m00.14s | Categories/Functor/Composition                            | 0m00.13s || +0m00.01s
  143. 0m00.14s | Categories/Functor                                        | 0m00.12s || +0m00.02s
  144. 0m00.13s | HIT/TruncImpliesFunext                                    | 0m00.14s || -0m00.01s
  145. 0m00.13s | Categories/Functor/Utf8                                   | 0m00.14s || -0m00.01s
  146. 0m00.13s | Categories/Limits/Functors                                | 0m00.14s || -0m00.01s
  147. 0m00.13s | ObjectClassifier                                          | 0m00.14s || -0m00.01s
  148. 0m00.12s | Categories/LaxComma                                       | 0m00.07s || +0m00.04s
  149. 0m00.12s | Categories/Grothendieck/ToSet/Core                        | 0m00.12s || +0m00.00s
  150. 0m00.12s | Types/Arrow                                               | 0m00.10s || +0m00.01s
  151. 0m00.12s | Categories/Functor/Prod/Core                              | 0m00.11s || +0m00.00s
  152. 0m00.12s | Categories/NaturalTransformation/Utf8                     | 0m00.12s || +0m00.00s
  153. 0m00.12s | Categories/NaturalTransformation/Composition/Laws         | 0m00.12s || +0m00.00s
  154. 0m00.12s | Categories/FunctorCategory/Morphisms                      | 0m00.12s || +0m00.00s
  155. 0m00.12s | Categories/Functor/Composition/Functorial/Core            | 0m00.16s || -0m00.04s
  156. 0m00.12s | EquivGroupoids                                            | 0m00.12s || +0m00.00s
  157. 0m00.12s | HIT/unique_choice                                         | 0m00.11s || +0m00.00s
  158. 0m00.12s | Categories/FunctorCategory/Utf8                           | 0m00.12s || +0m00.00s
  159. 0m00.11s | Categories/ExponentialLaws/Law2/Functors                  | 0m00.14s || -0m00.03s
  160. 0m00.11s | Categories/Functor/Pointwise/Core                         | 0m00.13s || -0m00.02s
  161. 0m00.11s | Categories/Adjoint/Functorial/Parts                       | 0m00.11s || +0m00.00s
  162. 0m00.11s | Categories/Functor/Prod/Functorial                        | 0m00.12s || -0m00.00s
  163. 0m00.11s | Utf8                                                      | 0m00.12s || -0m00.00s
  164. 0m00.10s | Categories/NaturalTransformation/Prod                     | 0m00.09s || +0m00.01s
  165. 0m00.10s | Categories/FunctorCategory/Dual                           | 0m00.11s || -0m00.00s
  166. 0m00.10s | Categories/Category/Sigma/OnObjects                       | 0m00.10s || +0m00.00s
  167. 0m00.10s | Categories/IndiscreteCategory                             | 0m00.10s || +0m00.00s
  168. 0m00.10s | Categories/Structure/Core                                 | 0m00.12s || -0m00.01s
  169. 0m00.10s | Basics/Contractible                                       | 0m00.07s || +0m00.03s
  170. 0m00.10s | HSet                                                      | 0m00.10s || +0m00.00s
  171. 0m00.10s | Categories/Comma/Projection                               | 0m00.17s || -0m00.07s
  172. 0m00.10s | Types/Bool                                                | 0m00.12s || -0m00.01s
  173. 0m00.10s | Tactics/RewriteModuloAssociativity                        | 0m00.09s || +0m00.01s
  174. 0m00.10s | Categories/Pseudofunctor/Core                             | 0m00.10s || +0m00.00s
  175. 0m00.10s | Categories/ExponentialLaws/Law3/Functors                  | 0m00.09s || +0m00.01s
  176. 0m00.10s | HProp                                                     | 0m00.10s || +0m00.00s
  177. 0m00.09s | Categories/CategoryOfSections/Core                        | 0m00.11s || -0m00.02s
  178. 0m00.09s | Categories/KanExtensions/Functors                         | 0m00.16s || -0m00.07s
  179. 0m00.09s | Basics/FunextVarieties                                    | 0m00.07s || +0m00.01s
  180. 0m00.09s | Categories/Cat/Core                                       | 0m00.09s || +0m00.00s
  181. 0m00.09s | Categories/NaturalTransformation/Pointwise                | 0m00.10s || -0m00.01s
  182. 0m00.09s | Basics/Decidable                                          | 0m00.09s || +0m00.00s
  183. 0m00.09s | Categories/NatCategory                                    | 0m00.07s || +0m00.01s
  184. 0m00.08s | Categories/Category/Prod                                  | 0m00.09s || -0m00.00s
  185. 0m00.08s | Categories/Adjoint                                        | 0m00.12s || -0m00.03s
  186. 0m00.08s | Basics/Trunc                                              | 0m00.06s || +0m00.02s
  187. 0m00.08s | Categories/FunctorCategory/Functorial                     | 0m00.08s || +0m00.00s
  188. 0m00.08s | Categories/Adjoint/Hom                                    | 0m00.08s || +0m00.00s
  189. 0m00.08s | Categories/Adjoint/UnitCounit                             | 0m00.07s || +0m00.00s
  190. 0m00.08s | Categories/HomFunctor                                     | 0m00.10s || -0m00.02s
  191. 0m00.07s | Basics/Overture                                           | 0m00.06s || +0m00.01s
  192. 0m00.07s | Categories/Adjoint/Functorial                             | 0m00.04s || +0m00.03s
  193. 0m00.07s | Basics/UniverseLevel                                      | 0m00.10s || -0m00.03s
  194. 0m00.07s | Categories/Adjoint/Composition                            | 0m00.07s || +0m00.00s
  195. 0m00.07s | Categories/GroupoidCategory/Core                          | 0m00.07s || +0m00.00s
  196. 0m00.07s | Categories/Category/Objects                               | 0m00.06s || +0m00.01s
  197. 0m00.07s | Categories/Functor/Dual                                   | 0m00.04s || +0m00.03s
  198. 0m00.07s | Categories/LaxComma/Utf8                                  | 0m00.10s || -0m00.03s
  199. 0m00.07s | Categories/NaturalTransformation/Dual                     | 0m00.06s || +0m00.01s
  200. 0m00.07s | Categories/Grothendieck/ToCat                             | 0m00.06s || +0m00.01s
  201. 0m00.07s | HIT/Interval                                              | 0m00.08s || -0m00.00s
  202. 0m00.07s | Categories/FunctorCategory/Core                           | 0m00.06s || +0m00.01s
  203. 0m00.07s | Categories/InitialTerminalCategory/NaturalTransformations | 0m00.10s || -0m00.03s
  204. 0m00.07s | Categories/DiscreteCategory                               | 0m00.03s || +0m00.04s
  205. 0m00.06s | Categories/KanExtensions                                  | 0m00.04s || +0m00.01s
  206. 0m00.06s | Categories/NaturalTransformation/Identity                 | 0m00.05s || +0m00.00s
  207. 0m00.06s | Categories/Category/Dual                                  | 0m00.08s || -0m00.02s
  208. 0m00.06s | Categories/LaxComma/Notations                             | 0m00.06s || +0m00.00s
  209. 0m00.06s | Categories/NaturalTransformation/Sum                      | 0m00.06s || +0m00.00s
  210. 0m00.06s | Categories/KanExtensions/Core                             | 0m00.08s || -0m00.02s
  211. 0m00.06s | coq/Init/Peano                                            | 0m00.04s || +0m00.01s
  212. 0m00.06s | Categories/DependentProduct                               | 0m00.04s || +0m00.01s
  213. 0m00.06s | Functorish                                                | 0m00.04s || +0m00.01s
  214. 0m00.06s | Categories/InitialTerminalCategory/Core                   | 0m00.07s || -0m00.01s
  215. 0m00.06s | Categories/Grothendieck                                   | 0m00.06s || +0m00.00s
  216. 0m00.06s | Categories/Grothendieck/ToSet                             | 0m00.06s || +0m00.00s
  217. 0m00.06s | Categories/Comma                                          | 0m00.10s || -0m00.04s
  218. 0m00.06s | Categories/Cat/Morphisms                                  | 0m00.06s || +0m00.00s
  219. 0m00.06s | Categories/CategoryOfGroupoids                            | 0m00.07s || -0m00.01s
  220. 0m00.06s | Categories/SetCategory/Functors/SetProp                   | 0m00.06s || +0m00.00s
  221. 0m00.06s | Categories/Category/Utf8                                  | 0m00.06s || +0m00.00s
  222. 0m00.06s | Types/Record                                              | 0m00.11s || -0m00.05s
  223. 0m00.06s | Categories/Pseudofunctor                                  | 0m00.06s || +0m00.00s
  224. 0m00.06s | UnivalenceAxiom                                           | 0m00.06s || +0m00.00s
  225. 0m00.06s | Categories/Category/Subcategory/Wide                      | 0m00.04s || +0m00.01s
  226. 0m00.06s | Categories/Category                                       | 0m00.12s || -0m00.06s
  227. 0m00.06s | Categories/ExponentialLaws/Law2                           | 0m00.05s || +0m00.00s
  228. 0m00.06s | Categories/Limits                                         | 0m00.05s || +0m00.00s
  229. 0m00.05s | Conjugation                                               | 0m00.06s || -0m00.00s
  230. 0m00.05s | Categories/Profunctor/Core                                | 0m00.04s || +0m00.01s
  231. 0m00.05s | Categories/Category/Pi                                    | 0m00.04s || +0m00.01s
  232. 0m00.05s | Categories/Functor/Prod                                   | 0m00.06s || -0m00.00s
  233. 0m00.05s | Categories/Profunctor                                     | 0m00.05s || +0m00.00s
  234. 0m00.05s | Categories/NaturalTransformation/Composition/Functorial   | 0m00.07s || -0m00.02s
  235. 0m00.05s | Categories/NaturalTransformation/Composition/Core         | 0m00.06s || -0m00.00s
  236. 0m00.05s | Categories/Adjoint/Notations                              | 0m00.03s || +0m00.02s
  237. 0m00.05s | Categories/Adjoint/Dual                                   | 0m00.05s || +0m00.00s
  238. 0m00.05s | Categories/SetCategory/Core                               | 0m00.07s || -0m00.02s
  239. 0m00.05s | Types/Unit                                                | 0m00.06s || -0m00.00s
  240. 0m00.05s | Categories/FunctorCategory                                | 0m00.06s || -0m00.00s
  241. 0m00.05s | Categories/Comma/Utf8                                     | 0m00.04s || +0m00.01s
  242. 0m00.05s | Spaces/Cantor                                             | 0m00.04s || +0m00.01s
  243. 0m00.05s | Categories/Cat                                            | 0m00.05s || +0m00.00s
  244. 0m00.05s | Categories/Category/Notations                             | 0m00.04s || +0m00.01s
  245. 0m00.05s | Categories/InitialTerminalCategory/Notations              | 0m00.04s || +0m00.01s
  246. 0m00.05s | Categories/NaturalTransformation                          | 0m00.05s || +0m00.00s
  247. 0m00.05s | Categories/FunctorCategory/Notations                      | 0m00.03s || +0m00.02s
  248. 0m00.05s | Categories/NaturalTransformation/Notations                | 0m00.05s || +0m00.00s
  249. 0m00.05s | Categories/Adjoint/UniversalMorphisms                     | 0m00.06s || -0m00.00s
  250. 0m00.05s | Categories/Category/Univalent                             | 0m00.05s || +0m00.00s
  251. 0m00.05s | NullHomotopy                                              | 0m00.05s || +0m00.00s
  252. 0m00.05s | Categories/Structure                                      | 0m00.08s || -0m00.03s
  253. 0m00.05s | Categories/PseudonaturalTransformation                    | 0m00.05s || +0m00.00s
  254. 0m00.04s | Categories/Adjoint/Core                                   | 0m00.04s || +0m00.00s
  255. 0m00.04s | Categories/Category/Sigma                                 | 0m00.05s || -0m00.01s
  256. 0m00.04s | Categories/Adjoint/Identity                               | 0m00.06s || -0m00.01s
  257. 0m00.04s | Categories/Comma/Notations                                | 0m00.04s || +0m00.00s
  258. 0m00.04s | Misc                                                      | 0m00.04s || +0m00.00s
  259. 0m00.04s | Categories/NaturalTransformation/Core                     | 0m00.04s || +0m00.00s
  260. 0m00.04s | Categories/NaturalTransformation/Composition              | 0m00.03s || +0m00.01s
  261. 0m00.04s | Categories/Adjoint/Composition/LawsTactic                 | 0m00.05s || -0m00.01s
  262. 0m00.04s | Categories/Structure/Utf8                                 | 0m00.03s || +0m00.01s
  263. 0m00.04s | Categories/Structure/Notations                            | 0m00.04s || +0m00.00s
  264. 0m00.04s | Categories/Category/Subcategory/Full                      | 0m00.03s || +0m00.01s
  265. 0m00.04s | Categories/Profunctor/Notations                           | 0m00.04s || +0m00.00s
  266. 0m00.04s | Categories/ExponentialLaws                                | 0m00.05s || -0m00.01s
  267. 0m00.04s | Categories/Profunctor/Representable                       | 0m00.04s || +0m00.00s
  268. 0m00.04s | Categories/InitialTerminalCategory                        | 0m00.04s || +0m00.00s
  269. 0m00.04s | Categories/GroupoidCategory                               | 0m00.04s || +0m00.00s
  270. 0m00.04s | Categories/ExponentialLaws/Tactics                        | 0m00.04s || +0m00.00s
  271. 0m00.04s | Categories/Profunctor/Identity                            | 0m00.04s || +0m00.00s
  272. 0m00.04s | Categories/Profunctor/Utf8                                | 0m00.04s || +0m00.00s
  273. 0m00.04s | Categories/ExponentialLaws/Law4                           | 0m00.05s || -0m00.01s
  274. 0m00.03s | Categories/Functor/Pointwise                              | 0m00.04s || -0m00.01s
  275. 0m00.03s | coq/Init/Specif                                           | 0m00.02s || +0m00.00s
  276. 0m00.03s | Categories/Adjoint/Utf8                                   | 0m00.04s || -0m00.01s
  277. 0m00.03s | Categories/Functor/Composition/Core                       | 0m00.02s || +0m00.00s
  278. 0m00.03s | Types/Empty                                               | 0m00.02s || +0m00.00s
  279. 0m00.03s | Categories/Category/Subcategory                           | 0m00.04s || -0m00.01s
  280. 0m00.03s | Categories/Functor/Identity                               | 0m00.02s || +0m00.00s
  281. 0m00.03s | Categories/SetCategory                                    | 0m00.04s || -0m00.01s
  282. 0m00.03s | Tactics/EvalIn                                            | 0m00.04s || -0m00.01s
  283. 0m00.03s | HIT/IntervalImpliesFunext                                 | 0m00.04s || -0m00.01s
  284. 0m00.03s | Categories/Category/Core                                  | 0m00.03s || +0m00.00s
  285. 0m00.03s | Tactics/BinderApply                                       | 0m00.03s || +0m00.00s
  286. 0m00.03s | Types                                                     | 0m00.02s || +0m00.00s
  287. 0m00.03s | Basics                                                    | 0m00.03s || +0m00.00s
  288. 0m00.03s | Categories/ExponentialLaws/Law1                           | 0m00.06s || -0m00.03s
  289. 0m00.03s | Categories/ExponentialLaws/Law3                           | 0m00.04s || -0m00.01s
  290. 0m00.02s | coq/Init/Datatypes                                        | 0m00.02s || +0m00.00s
  291. 0m00.02s | Categories/Functor/Core                                   | 0m00.02s || +0m00.00s
  292. 0m00.02s | coq/Init/Prelude                                          | 0m00.01s || +0m00.01s
  293. 0m00.02s | Categories/CategoryOfSections                             | 0m00.04s || -0m00.02s
  294. 0m00.02s | coq/Init/Logic_Type                                       | 0m00.02s || +0m00.00s
  295. 0m00.02s | coq/Program/Tactics                                       | 0m00.01s || +0m00.01s
  296. 0m00.02s | Categories/SetCategory/Functors                           | 0m00.04s || -0m00.02s
  297. 0m00.02s | FunextAxiom                                               | 0m00.01s || +0m00.01s
  298. 0m00.01s | coq/Init/Notations                                        | 0m00.00s || +0m00.01s
  299. 0m00.01s | Basics/Notations                                          | 0m00.01s || +0m00.00s
  300. 0m00.01s | Categories/Category/Strict                                | 0m00.02s || -0m00.01s
  301. 0m00.01s | coq/Unicode/Utf8_core                                     | 0m00.00s || +0m00.01s
  302. 0m00.01s | coq/Init/Tactics                                          | 0m00.01s || +0m00.00s
  303. 0m00.00s | coq/Unicode/Utf8                                          | 0m00.01s || -0m00.01s
  304. 0m00.00s | coq/Init/Logic                                            | 0m00.01s || -0m00.01s
  305. 0m00.00s | coq/Bool/Bool                                             | 0m00.00s || +0m00.00s
Raw Paste

Login or Register to edit or fork this paste. It's free.