Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Commits on May 13, 2015
  1. @mikeshulman

    Merge pull request #756 from JasonGross/more-robust-equiv-induction

    mikeshulman authored
    Make [equiv_induction] a bit more robust
Commits on May 11, 2015
  1. @mikeshulman

    Merge pull request #755 from JasonGross/lift-equiv

    mikeshulman authored
    Add some definitions for lifting equivalences
Commits on May 9, 2015
  1. @JasonGross
  2. @JasonGross
Commits on Apr 20, 2015
  1. @spitters

    Merge pull request #753 from mikeshulman/coreflective

    spitters authored
    A naive coreflective subuniverse is uniquely determined by an hprop
Commits on Apr 17, 2015
  1. @JasonGross

    Merge pull request #752 from mikeshulman/lexrsu

    JasonGross authored
    Make Lex_Reflective_Subuniverses actually instantiate SigmaClosed
  2. @mikeshulman
  3. @andrejbauer

    Merge pull request #751 from mikeshulman/path_prod_pp_p

    andrejbauer authored
    Add a coherence for associativity of path_prod_pp
  4. @mikeshulman
  5. @mikeshulman

    Make Lex_Reflective_Subuniverses actually instantiate SigmaClosed.

    mikeshulman authored
    Needs lots of attention to universes.
  6. @mikeshulman
  7. @JasonGross

    Merge pull request #746 from mikeshulman/lex-fibers

    JasonGross authored
    If a reflective subuniverse preserves fibers, it is a modality (and lex)
Commits on Apr 16, 2015
  1. @mikeshulman

    Add a coherence for associativity of path_prod_pp

    mikeshulman authored
    (Mainly to check that what I wrote in the book is correct)
Commits on Apr 10, 2015
  1. @JasonGross

    Merge pull request #750 from JasonGross/fix-contrib-beta2

    JasonGross authored
    Add a local admit tactic to contrib/Frudenthal.v
Commits on Apr 9, 2015
  1. @JasonGross

    Move [proof_admitted] out of the standard library

    JasonGross authored
    Preparation for 8.5 beta 2.
  2. @JasonGross

    Add a local admit tactic to contrib/Frudenthal.v

    JasonGross authored
    In 8.5beta2, the built-in [admit] which uses [proof_admitted] is
    replaced by one aliased to [shelve]; we bring it back so we can use it
    in transparent proofs, in contrib/Freudenthal.v.
Commits on Apr 7, 2015
  1. @spitters

    Merge pull request #748 from mikeshulman/rewrite@A-rsu

    spitters authored
    Use rewrite@A more in O_coeq_cmp_eisretr
  2. @spitters

    Merge pull request #747 from JasonGross/fix-rewrite@A

    spitters authored
    Fix [rewrite@A]
  3. @mikeshulman
  4. @JasonGross

    Do [cbv beta] earlier in [rewrite@A]

    JasonGross authored
    This will hopefully prevent other loops, by making the thing we search
    in and the thing we pattern in the same.
  5. @JasonGross

    Fix [rewrite@A]

    JasonGross authored
    When the hypothesis contained [a @ (b @ c)] where the implicit arguments
    to [concat] did not match the implicit arguments inferred for [@concat _
    _ _ _ a (@concat _ _ _ _ b c)] (according to [pattern]),
    [left_associate_concat_in] looped, repeatedly finding [a @ (b @ c)], and
    failing to associate it to the left, introducing constant transports
    that did nothing.
    
    This is now fixed, by picking up and passing the implicit arguments,
    explicitly.
    
    The comment in Modalities/ReflectiveSubuniverse.v has been updated; a
    naive use of [rewrite@A] causes the subsequent rewrite to fail.  I
    haven't tracked it down, but I suspect @mikeshulman wouldn't have much
    trouble updating the file.
    
    This fixes #744; the test is now added to Tests.v.
  6. @JasonGross

    Merge pull request #743 from mikeshulman/Ocolim

    JasonGross authored
    reflectors preserve coproducts and coequalizers
  7. @mikeshulman

    Merge pull request #745 from mikeshulman/rapply

    mikeshulman authored
    swap rapply and rapply'
  8. @mikeshulman
Commits on Apr 5, 2015
  1. @mikeshulman
  2. @mikeshulman

    the 3x3 lemma

    mikeshulman authored
Commits on Apr 4, 2015
  1. @mikeshulman

    swap rapply and rapply'

    mikeshulman authored
    After    | File Name                                                 | Before   || Change
    --------------------------------------------------------------------------------------------
    5m15.64s | Total                                                     | 5m16.66s || -0m01.01s
    --------------------------------------------------------------------------------------------
    0m45.31s | categories/Adjoint/Pointwise                              | 0m45.31s || +0m00.00s
    0m17.60s | hit/V                                                     | 0m17.62s || -0m00.01s
    0m14.41s | categories/Category/Sigma/Univalent                       | 0m14.48s || -0m00.07s
    0m13.55s | Spaces/BAut/Bool                                          | 0m13.58s || -0m00.02s
    0m11.56s | contrib/Freudenthal                                       | 0m11.61s || -0m00.04s
    0m10.76s | Idempotents                                               | 0m10.72s || +0m00.03s
    0m08.67s | Spaces/No                                                 | 0m08.61s || +0m00.06s
    0m07.76s | Spaces/Finite                                             | 0m07.75s || +0m00.00s
    0m07.66s | categories/Adjoint/Functorial/Laws                        | 0m07.69s || -0m00.03s
    0m07.52s | categories/ExponentialLaws/Law4/Law                       | 0m07.54s || -0m00.02s
    0m07.32s | categories/ExponentialLaws/Law3/Law                       | 0m07.36s || -0m00.04s
    0m06.96s | categories/ExponentialLaws/Law2/Law                       | 0m06.98s || -0m00.02s
    0m06.73s | Modalities/Lex                                            | 0m06.70s || +0m00.03s
    0m04.78s | categories/LaxComma/CoreLaws                              | 0m04.79s || -0m00.00s
    0m04.66s | categories/Comma/ProjectionFunctors                       | 0m04.68s || -0m00.01s
    0m04.35s | categories/Category/Paths                                 | 0m04.29s || +0m00.05s
    0m04.13s | PType                                                     | 0m04.14s || -0m00.00s
    0m03.98s | Spaces/BAut                                               | 0m03.98s || +0m00.00s
    0m03.90s | Modalities/Modality                                       | 0m03.66s || +0m00.23s
    0m03.84s | hit/Suspension                                            | 0m03.84s || +0m00.00s
    0m03.54s | hit/Coeq                                                  | 0m03.50s || +0m00.04s
    0m03.30s | hit/FreeIntQuotient                                       | 0m03.30s || +0m00.00s
    0m03.24s | Types/Universe                                            | 0m03.26s || -0m00.01s
    0m03.24s | Factorization                                             | 0m03.24s || +0m00.00s
    0m03.03s | categories/Comma/Functorial                               | 0m03.02s || +0m00.00s
    0m02.58s | contrib/HoTTBookExercises                                 | 0m02.56s || +0m00.02s
    0m02.50s | Modalities/Fracture                                       | 0m02.49s || +0m00.00s
    0m02.41s | contrib/HoTTBook                                          | 0m02.38s || +0m00.03s
    0m02.39s | hit/Connectedness                                         | 0m02.38s || +0m00.01s
    0m02.28s | Types/Sigma                                               | 0m02.34s || -0m00.06s
    0m02.27s | Modalities/ReflectiveSubuniverse                          | 0m02.27s || +0m00.00s
    0m02.15s | categories/GroupoidCategory/Morphisms                     | 0m02.16s || -0m00.01s
    0m02.02s | categories/Grothendieck/ToSet/Morphisms                   | 0m02.02s || +0m00.00s
    0m01.83s | Spaces/BAut/Bool/IncoherentIdempotent                     | 0m01.79s || +0m00.04s
    0m01.69s | categories/Grothendieck/ToSet/Univalent                   | 0m01.67s || +0m00.02s
    0m01.64s | categories/Category/Morphisms                             | 0m01.67s || -0m00.03s
    0m01.56s | categories/Functor/Sum                                    | 0m01.49s || +0m00.07s
    0m01.53s | hit/Flattening                                            | 0m01.50s || +0m00.03s
    0m01.51s | categories/ExponentialLaws/Law4/Functors                  | 0m01.52s || -0m00.01s
    0m01.50s | Tactics/EquivalenceInduction                              | 0m01.50s || +0m00.00s
    0m01.47s | categories/ExponentialLaws/Law1/Law                       | 0m01.54s || -0m00.07s
    0m01.38s | Modalities/Localization                                   | 0m01.36s || +0m00.01s
    0m01.36s | Types/Sum                                                 | 0m01.38s || -0m00.01s
    0m01.32s | hit/epi                                                   | 0m01.35s || -0m00.03s
    0m01.27s | categories/Adjoint/Composition/AssociativityLaw           | 0m01.29s || -0m00.02s
    0m01.13s | hit/Truncations                                           | 0m01.16s || -0m00.03s
    0m01.11s | categories/Functor/Paths                                  | 0m01.12s || -0m00.01s
    0m01.10s | DProp                                                     | 0m01.07s || +0m00.03s
    0m01.07s | Basics/PathGroupoids                                      | 0m01.08s || -0m00.01s
    0m01.07s | categories/Grothendieck/PseudofunctorToCat                | 0m01.09s || -0m00.02s
    0m01.04s | Modalities/Open                                           | 0m01.00s || +0m00.04s
    0m01.03s | categories/Functor/Composition/Functorial/Attributes      | 0m01.01s || +0m00.02s
    0m01.00s | hit/quotient                                              | 0m01.04s || -0m00.04s
    0m00.99s | categories/Adjoint/HomCoercions                           | 0m01.02s || -0m00.03s
    0m00.96s | categories/Functor/Pointwise/Properties                   | 0m00.98s || -0m00.02s
    0m00.94s | categories/Yoneda                                         | 0m00.98s || -0m00.04s
    0m00.90s | TruncType                                                 | 0m00.88s || +0m00.02s
    0m00.89s | categories/Comma/InducedFunctors                          | 0m00.90s || -0m00.01s
    0m00.86s | categories/Adjoint/Composition/IdentityLaws               | 0m00.88s || -0m00.02s
    0m00.83s | categories/Pseudofunctor/FromFunctor                      | 0m00.84s || -0m00.01s
    0m00.83s | categories/Pseudofunctor/RewriteLaws                      | 0m00.80s || +0m00.02s
    0m00.82s | Modalities/Topological                                    | 0m00.82s || +0m00.00s
    0m00.81s | Types/Paths                                               | 0m00.76s || +0m00.05s
    0m00.79s | categories/Pseudofunctor/Identity                         | 0m00.82s || -0m00.02s
    0m00.78s | Modalities/Closed                                         | 0m00.84s || -0m00.05s
    0m00.78s | Constant                                                  | 0m00.75s || +0m00.03s
    0m00.76s | EquivalenceVarieties                                      | 0m00.80s || -0m00.04s
    0m00.76s | Spaces/BAut/Cantor                                        | 0m00.76s || +0m00.00s
    0m00.75s | categories/Category/Sigma/OnMorphisms                     | 0m00.76s || -0m00.01s
    0m00.68s | categories/Functor/Composition/Laws                       | 0m00.70s || -0m00.01s
    0m00.68s | HoTT                                                      | 0m00.73s || -0m00.04s
    0m00.68s | Tests                                                     | 0m00.67s || +0m00.01s
    0m00.66s | categories/ExponentialLaws/Law0                           | 0m00.64s || +0m00.02s
    0m00.66s | Types/Equiv                                               | 0m00.65s || +0m00.01s
    0m00.66s | categories/Comma/Dual                                     | 0m00.65s || +0m00.01s
    0m00.65s | Basics/Equivalences                                       | 0m00.66s || -0m00.01s
    0m00.63s | Basics/Pointed                                            | 0m00.64s || -0m00.01s
    0m00.60s | hit/Spheres                                               | 0m00.58s || +0m00.02s
    0m00.59s | categories                                                | 0m00.52s || +0m00.06s
    0m00.59s | categories/Category/Sum                                   | 0m00.60s || -0m00.01s
    0m00.58s | categories/Adjoint/Composition/Core                       | 0m00.60s || -0m00.02s
    0m00.58s | categories/Comma/Core                                     | 0m00.59s || -0m00.01s
    0m00.58s | categories/Adjoint/UnitCounitCoercions                    | 0m00.53s || +0m00.04s
    0m00.57s | categories/UniversalProperties                            | 0m00.56s || +0m00.00s
    0m00.57s | categories/LaxComma/CoreParts                             | 0m00.55s || +0m00.01s
    0m00.57s | categories/Functor/Attributes                             | 0m00.49s || +0m00.07s
    0m00.52s | categories/LaxComma/Core                                  | 0m00.55s || -0m00.03s
    0m00.52s | hit/Circle                                                | 0m00.55s || -0m00.03s
    0m00.52s | categories/Functor/Prod/Universal                         | 0m00.50s || +0m00.02s
    0m00.51s | Modalities/Accessible                                     | 0m00.52s || -0m00.01s
    0m00.49s | Extensions                                                | 0m00.50s || -0m00.01s
    0m00.48s | categories/ProductLaws                                    | 0m00.52s || -0m00.04s
    0m00.44s | categories/ChainCategory                                  | 0m00.45s || -0m00.01s
    0m00.44s | Types/Prod                                                | 0m00.44s || +0m00.00s
    0m00.43s | Spaces/Nat                                                | 0m00.40s || +0m00.02s
    0m00.43s | categories/Structure/IdentityPrinciple                    | 0m00.42s || +0m00.01s
    0m00.42s | categories/SetCategory/Morphisms                          | 0m00.41s || +0m00.01s
    0m00.42s | categories/DualFunctor                                    | 0m00.42s || +0m00.00s
    0m00.41s | Pullback                                                  | 0m00.41s || +0m00.00s
    0m00.40s | categories/FundamentalPreGroupoidCategory                 | 0m00.38s || +0m00.02s
    0m00.40s | categories/Adjoint/Paths                                  | 0m00.36s || +0m00.04s
    0m00.40s | categories/InitialTerminalCategory/Pseudofunctors         | 0m00.37s || +0m00.03s
    0m00.38s | categories/GroupoidCategory/Dual                          | 0m00.38s || +0m00.00s
    0m00.37s | categories/Adjoint/Functorial/Core                        | 0m00.36s || +0m00.01s
    0m00.36s | categories/Functor/Composition/Functorial/Core            | 0m00.37s || -0m00.01s
    0m00.36s | hit/Join                                                  | 0m00.37s || -0m00.01s
    0m00.35s | categories/NaturalTransformation/Isomorphisms             | 0m00.37s || -0m00.02s
    0m00.35s | categories/Adjoint/UniversalMorphisms/Core                | 0m00.37s || -0m00.02s
    0m00.35s | categories/ExponentialLaws/Law1/Functors                  | 0m00.37s || -0m00.02s
    0m00.34s | categories/Category/Sigma/Core                            | 0m00.34s || +0m00.00s
    0m00.34s | Modalities/Nullification                                  | 0m00.35s || -0m00.00s
    0m00.34s | categories/Limits/Core                                    | 0m00.36s || -0m00.01s
    0m00.33s | categories/SemiSimplicialSets                             | 0m00.37s || -0m00.03s
    0m00.32s | Fibrations                                                | 0m00.34s || -0m00.02s
    0m00.31s | categories/HomotopyPreCategory                            | 0m00.30s || +0m00.01s
    0m00.31s | categories/Notations                                      | 0m00.31s || +0m00.00s
    0m00.30s | categories/Utf8                                           | 0m00.30s || +0m00.00s
    0m00.30s | hit/Pushout                                               | 0m00.29s || +0m00.01s
    0m00.30s | categories/Functor/Pointwise/Core                         | 0m00.29s || +0m00.01s
    0m00.29s | categories/NaturalTransformation/Paths                    | 0m00.30s || -0m00.01s
    0m00.28s | categories/SimplicialSets                                 | 0m00.32s || -0m00.03s
    0m00.28s | Types/Wtype                                               | 0m00.54s || -0m00.26s
    0m00.28s | categories/Functor/Notations                              | 0m00.23s || +0m00.05s
    0m00.28s | categories/Functor                                        | 0m00.28s || +0m00.00s
    0m00.27s | categories/ExponentialLaws/Law2/Functors                  | 0m00.30s || -0m00.02s
    0m00.27s | categories/Functor/Prod/Core                              | 0m00.27s || +0m00.00s
    0m00.26s | categories/Functor/Composition/Functorial                 | 0m00.25s || +0m00.01s
    0m00.26s | categories/FunctorCategory/Morphisms                      | 0m00.28s || -0m00.02s
    0m00.26s | ObjectClassifier                                          | 0m00.26s || +0m00.00s
    0m00.26s | categories/InitialTerminalCategory/Functors               | 0m00.22s || +0m00.04s
    0m00.26s | Modalities/Identity                                       | 0m00.27s || -0m00.01s
    0m00.25s | categories/Grothendieck/ToSet/Core                        | 0m00.25s || +0m00.00s
    0m00.25s | categories/Structure/Core                                 | 0m00.23s || +0m00.01s
    0m00.25s | Types/Forall                                              | 0m00.28s || -0m00.03s
    0m00.25s | categories/NaturalTransformation/Utf8                     | 0m00.23s || +0m00.01s
    0m00.24s | categories/FunctorCategory/Utf8                           | 0m00.26s || -0m00.02s
    0m00.24s | Spaces/Int                                                | 0m00.26s || -0m00.02s
    0m00.23s | categories/Functor/Prod/Functorial                        | 0m00.26s || -0m00.03s
    0m00.23s | categories/Limits/Functors                                | 0m00.23s || +0m00.00s
    0m00.23s | categories/NaturalTransformation/Prod                     | 0m00.22s || +0m00.01s
    0m00.23s | hit/TruncImpliesFunext                                    | 0m00.26s || -0m00.03s
    0m00.22s | hit/iso                                                   | 0m00.22s || +0m00.00s
    0m00.22s | categories/NaturalTransformation/Composition/Laws         | 0m00.26s || -0m00.04s
    0m00.22s | categories/Functor/Utf8                                   | 0m00.25s || -0m00.03s
    0m00.22s | EquivGroupoids                                            | 0m00.20s || +0m00.01s
    0m00.22s | categories/Adjoint/Functorial/Parts                       | 0m00.20s || +0m00.01s
    0m00.21s | Modalities/Notnot                                         | 0m00.20s || +0m00.00s
    0m00.21s | UnivalenceImpliesFunext                                   | 0m00.27s || -0m00.06s
    0m00.21s | categories/Category/Sigma/OnObjects                       | 0m00.22s || -0m00.01s
    0m00.21s | categories/HomFunctor                                     | 0m00.19s || +0m00.01s
    0m00.21s | categories/CategoryOfSections/Core                        | 0m00.21s || +0m00.00s
    0m00.21s | Utf8                                                      | 0m00.24s || -0m00.03s
    0m00.21s | categories/Functor/Composition                            | 0m00.24s || -0m00.03s
    0m00.20s | categories/NaturalTransformation/Pointwise                | 0m00.23s || -0m00.03s
    0m00.20s | categories/Category/Prod                                  | 0m00.22s || -0m00.01s
    0m00.20s | HSet                                                      | 0m00.22s || -0m00.01s
    0m00.20s | hit/unique_choice                                         | 0m00.22s || -0m00.01s
    0m00.20s | Tactics                                                   | 0m00.18s || +0m00.02s
    0m00.19s | categories/PseudonaturalTransformation/Core               | 0m00.21s || -0m00.01s
    0m00.19s | HProp                                                     | 0m00.21s || -0m00.01s
    0m00.18s | Types/Arrow                                               | 0m00.20s || -0m00.02s
    0m00.17s | categories/ExponentialLaws/Law3/Functors                  | 0m00.18s || -0m00.00s
    0m00.17s | categories/IndiscreteCategory                             | 0m00.19s || -0m00.01s
    0m00.17s | Types/Bool                                                | 0m00.20s || -0m00.03s
    0m00.17s | categories/Pseudofunctor/Core                             | 0m00.21s || -0m00.03s
    0m00.17s | categories/Adjoint/UnitCounit                             | 0m00.15s || +0m00.02s
    0m00.17s | categories/Comma/Projection                               | 0m00.19s || -0m00.01s
    0m00.16s | categories/Cat/Core                                       | 0m00.16s || +0m00.00s
    0m00.16s | categories/FunctorCategory/Functorial                     | 0m00.16s || +0m00.00s
    0m00.16s | Tactics/RewriteModuloAssociativity                        | 0m00.16s || +0m00.00s
    0m00.15s | categories/NatCategory                                    | 0m00.15s || +0m00.00s
    0m00.15s | categories/FunctorCategory/Dual                           | 0m00.19s || -0m00.04s
    0m00.15s | categories/KanExtensions/Core                             | 0m00.16s || -0m00.01s
    0m00.15s | categories/KanExtensions/Functors                         | 0m00.18s || -0m00.03s
    0m00.14s | categories/NaturalTransformation/Sum                      | 0m00.13s || +0m00.01s
    0m00.14s | categories/Adjoint/Hom                                    | 0m00.11s || +0m00.03s
    0m00.14s | categories/Category/Objects                               | 0m00.13s || +0m00.01s
    0m00.14s | categories/Adjoint                                        | 0m00.16s || -0m00.01s
    0m00.13s | Basics/Overture                                           | 0m00.15s || -0m00.01s
    0m00.13s | categories/LaxComma                                       | 0m00.10s || +0m00.03s
    0m00.13s | Basics/Decidable                                          | 0m00.13s || +0m00.00s
    0m00.13s | categories/GroupoidCategory/Core                          | 0m00.12s || +0m00.01s
    0m00.13s | categories/NaturalTransformation/Composition/Functorial   | 0m00.11s || +0m00.02s
    0m00.12s | Basics/Contractible                                       | 0m00.11s || +0m00.00s
    0m00.12s | categories/Comma                                          | 0m00.10s || +0m00.01s
    0m00.12s | categories/Grothendieck/ToCat                             | 0m00.13s || -0m00.01s
    0m00.12s | Basics/FunextVarieties                                    | 0m00.12s || +0m00.00s
    0m00.11s | categories/LaxComma/Notations                             | 0m00.09s || +0m00.02s
    0m00.11s | categories/Category                                       | 0m00.13s || -0m00.02s
    0m00.11s | Functorish                                                | 0m00.10s || +0m00.00s
    0m00.11s | Basics/Trunc                                              | 0m00.10s || +0m00.00s
    0m00.11s | categories/InitialTerminalCategory/NaturalTransformations | 0m00.12s || -0m00.00s
    0m00.11s | categories/NaturalTransformation                          | 0m00.09s || +0m00.02s
    0m00.11s | categories/NaturalTransformation/Identity                 | 0m00.11s || +0m00.00s
    0m00.11s | Types/Record                                              | 0m00.12s || -0m00.00s
    0m00.11s | categories/NaturalTransformation/Composition/Core         | 0m00.14s || -0m00.03s
    0m00.10s | Conjugation                                               | 0m00.11s || -0m00.00s
    0m00.10s | categories/Comma/Utf8                                     | 0m00.09s || +0m00.01s
    0m00.10s | categories/DependentProduct                               | 0m00.10s || +0m00.00s
    0m00.10s | categories/Category/Sigma                                 | 0m00.07s || +0m00.03s
    0m00.10s | categories/Adjoint/Dual                                   | 0m00.11s || -0m00.00s
    0m00.10s | categories/Category/Pi                                    | 0m00.11s || -0m00.00s
    0m00.10s | categories/Profunctor/Core                                | 0m00.09s || +0m00.01s
    0m00.10s | categories/ExponentialLaws                                | 0m00.11s || -0m00.00s
    0m00.10s | categories/Category/Dual                                  | 0m00.08s || +0m00.02s
    0m00.10s | categories/ExponentialLaws/Law2                           | 0m00.08s || +0m00.02s
    0m00.10s | categories/InitialTerminalCategory/Core                   | 0m00.10s || +0m00.00s
    0m00.10s | categories/CategoryOfGroupoids                            | 0m00.09s || +0m00.01s
    0m00.10s | categories/Pseudofunctor                                  | 0m00.08s || +0m00.02s
    0m00.10s | categories/Functor/Prod                                   | 0m00.07s || +0m00.03s
    0m00.10s | categories/LaxComma/Utf8                                  | 0m00.10s || +0m00.00s
    0m00.10s | categories/FunctorCategory                                | 0m00.09s || +0m00.01s
    0m00.10s | categories/KanExtensions                                  | 0m00.10s || +0m00.00s
    0m00.10s | categories/Cat/Morphisms                                  | 0m00.11s || -0m00.00s
    0m00.10s | categories/Limits                                         | 0m00.12s || -0m00.01s
    0m00.10s | categories/FunctorCategory/Core                           | 0m00.11s || -0m00.00s
    0m00.10s | categories/NaturalTransformation/Core                     | 0m00.08s || +0m00.02s
    0m00.09s | categories/Adjoint/Utf8                                   | 0m00.08s || +0m00.00s
    0m00.09s | categories/NaturalTransformation/Notations                | 0m00.08s || +0m00.00s
    0m00.09s | categories/Profunctor                                     | 0m00.06s || +0m00.03s
    0m00.09s | categories/PseudonaturalTransformation                    | 0m00.10s || -0m00.01s
    0m00.09s | categories/Adjoint/Identity                               | 0m00.09s || +0m00.00s
    0m00.09s | categories/Grothendieck                                   | 0m00.08s || +0m00.00s
    0m00.09s | categories/SetCategory/Functors/SetProp                   | 0m00.11s || -0m00.02s
    0m00.09s | categories/SetCategory/Core                               | 0m00.09s || +0m00.00s
    0m00.08s | categories/Adjoint/Core                                   | 0m00.07s || +0m00.00s
    0m00.08s | categories/Category/Utf8                                  | 0m00.07s || +0m00.00s
    0m00.08s | hit/Interval                                              | 0m00.09s || -0m00.00s
    0m00.08s | categories/Functor/Dual                                   | 0m00.08s || +0m00.00s
    0m00.08s | categories/ExponentialLaws/Tactics                        | 0m00.08s || +0m00.00s
    0m00.08s | categories/InitialTerminalCategory                        | 0m00.08s || +0m00.00s
    0m00.08s | categories/ExponentialLaws/Law1                           | 0m00.08s || +0m00.00s
    0m00.08s | categories/ExponentialLaws/Law3                           | 0m00.09s || -0m00.00s
    0m00.08s | Types/Unit                                                | 0m00.10s || -0m00.02s
    0m00.08s | coq/Init/Peano                                            | 0m00.09s || -0m00.00s
    0m00.08s | Spaces/Cantor                                             | 0m00.07s || +0m00.00s
    0m00.08s | categories/Adjoint/Notations                              | 0m00.08s || +0m00.00s
    0m00.08s | categories/SetCategory                                    | 0m00.09s || -0m00.00s
    0m00.08s | categories/NaturalTransformation/Dual                     | 0m00.09s || -0m00.00s
    0m00.08s | categories/Category/Univalent                             | 0m00.09s || -0m00.00s
    0m00.08s | categories/Comma/Notations                                | 0m00.11s || -0m00.03s
    0m00.08s | categories/InitialTerminalCategory/Notations              | 0m00.10s || -0m00.02s
    0m00.08s | categories/Adjoint/Functorial                             | 0m00.10s || -0m00.02s
    0m00.08s | categories/Profunctor/Representable                       | 0m00.08s || +0m00.00s
    0m00.08s | categories/Structure                                      | 0m00.09s || -0m00.00s
    0m00.08s | hit/TwoSphere                                             | 0m00.08s || +0m00.00s
    0m00.08s | categories/Category/Notations                             | 0m00.08s || +0m00.00s
    0m00.08s | categories/Profunctor/Identity                            | 0m00.09s || -0m00.00s
    0m00.08s | Types/Nat                                                 | 0m00.07s || +0m00.00s
    0m00.08s | categories/FunctorCategory/Notations                      | 0m00.09s || -0m00.00s
    0m00.08s | categories/Structure/Utf8                                 | 0m00.08s || +0m00.00s
    0m00.08s | categories/Adjoint/Composition/LawsTactic                 | 0m00.10s || -0m00.02s
    0m00.08s | categories/Adjoint/UniversalMorphisms                     | 0m00.08s || +0m00.00s
    0m00.07s | categories/DiscreteCategory                               | 0m00.08s || -0m00.00s
    0m00.07s | categories/Cat                                            | 0m00.07s || +0m00.00s
    0m00.07s | categories/Profunctor/Notations                           | 0m00.09s || -0m00.01s
    0m00.07s | categories/ExponentialLaws/Law4                           | 0m00.06s || +0m00.01s
    0m00.07s | Misc                                                      | 0m00.07s || +0m00.00s
    0m00.07s | categories/Structure/Notations                            | 0m00.08s || -0m00.00s
    0m00.07s | categories/Category/Core                                  | 0m00.08s || -0m00.00s
    0m00.07s | categories/GroupoidCategory                               | 0m00.07s || +0m00.00s
    0m00.06s | hit/IntervalImpliesFunext                                 | 0m00.06s || +0m00.00s
    0m00.06s | categories/Category/Subcategory                           | 0m00.06s || +0m00.00s
    0m00.06s | Types/Empty                                               | 0m00.07s || -0m00.01s
    0m00.06s | categories/Functor/Pointwise                              | 0m00.09s || -0m00.03s
    0m00.06s | Types                                                     | 0m00.07s || -0m00.01s
    0m00.06s | categories/CategoryOfSections                             | 0m00.08s || -0m00.02s
    0m00.06s | categories/Category/Subcategory/Wide                      | 0m00.07s || -0m00.01s
    0m00.06s | categories/NaturalTransformation/Composition              | 0m00.05s || +0m00.00s
    0m00.06s | categories/Functor/Composition/Core                       | 0m00.05s || +0m00.00s
    0m00.06s | categories/Grothendieck/ToSet                             | 0m00.09s || -0m00.03s
    0m00.06s | Tactics/BinderApply                                       | 0m00.06s || +0m00.00s
    0m00.06s | NullHomotopy                                              | 0m00.08s || -0m00.02s
    0m00.06s | categories/Category/Subcategory/Full                      | 0m00.07s || -0m00.01s
    0m00.06s | categories/Profunctor/Utf8                                | 0m00.08s || -0m00.02s
    0m00.06s | categories/Adjoint/Composition                            | 0m00.09s || -0m00.03s
    0m00.05s | Basics/UniverseLevel                                      | 0m00.04s || +0m00.01s
    0m00.05s | categories/Category/Strict                                | 0m00.04s || +0m00.01s
    0m00.05s | UnivalenceAxiom                                           | 0m00.06s || -0m00.00s
    0m00.05s | coq/Program/Tactics                                       | 0m00.06s || -0m00.00s
    0m00.04s | coq/Init/Datatypes                                        | 0m00.04s || +0m00.00s
    0m00.04s | categories/SetCategory/Functors                           | 0m00.08s || -0m00.04s
    0m00.04s | categories/Functor/Core                                   | 0m00.06s || -0m00.01s
    0m00.04s | coq/Init/Logic_Type                                       | 0m00.06s || -0m00.01s
    0m00.04s | Basics                                                    | 0m00.04s || +0m00.00s
    0m00.04s | FunextAxiom                                               | 0m00.04s || +0m00.00s
    0m00.03s | categories/Functor/Identity                               | 0m00.03s || +0m00.00s
    0m00.03s | coq/Init/Specif                                           | 0m00.04s || -0m00.01s
    0m00.02s | coq/Unicode/Utf8                                          | 0m00.02s || +0m00.00s
    0m00.02s | coq/Unicode/Utf8_core                                     | 0m00.02s || +0m00.00s
    0m00.02s | coq/Init/Prelude                                          | 0m00.02s || +0m00.00s
    0m00.02s | coq/Bool/Bool                                             | 0m00.02s || +0m00.00s
    0m00.02s | coq/Init/Tactics                                          | 0m00.03s || -0m00.00s
    0m00.02s | coq/Init/Logic                                            | 0m00.03s || -0m00.00s
    0m00.01s | coq/Init/Notations                                        | 0m00.03s || -0m00.01s
Commits on Apr 3, 2015
  1. @mikeshulman

    Merge pull request #742 from mikeshulman/free-int-quotients

    mikeshulman authored
    quotients by free actions of Int
  2. @mikeshulman
  3. @mikeshulman
Commits on Mar 31, 2015
  1. @mikeshulman
  2. @mikeshulman
  3. @mikeshulman

    Merge pull request #741 from mikeshulman/coeq-circle

    mikeshulman authored
    More about coequalizers and the circle
  4. @mikeshulman
Commits on Mar 28, 2015
  1. @mikeshulman
Something went wrong with that request. Please try again.