Giter Club home page Giter Club logo

rezk_completion's People

Contributors

benediktahrens avatar dangrayson avatar

Stargazers

avatar avatar avatar avatar avatar

Watchers

avatar avatar avatar avatar avatar

Forkers

dangrayson timrichter

rezk_completion's Issues

Slowness in compiling the library

When I compile the library with Coq 8.4 and time how long it takes to make each file, I get

0.10    pathnotations
0.17    topos/epis_monos
0.18    limits/terminal
0.20    limits/initial
0.21    HLevel_n_is_of_hlevel_Sn
0.24    limits/aux_lemmas_HoTT
0.31    category_hset
0.43    whiskering
0.46    auxiliary_lemmas_HoTT
0.70    rezk_completion
0.86    precategories
1.03    yoneda
1.12    limits/cones
1.12    sub_precategories
4.71    equivalences
6.99    functors_transformations
9.29    precomp_fully_faithful
32.22   precomp_ess_surj
69.37   limits/pullbacks

(Admittedly, the HoTT library takes around three times as long, and I don't have a good sense of how complicated the constructions in precomp_ess_surj and limits/pullbacks.)

At least a third of the time in limits/pullbacks, probably much more, is spent checking trivial lemmas which are slow due to nested sigma types. It's plausible that Matthieu's polyproj branch fixes this, but if you're interested in fixing it before that lands for 8.5, you can replace nested sigmas with records (or, possibly just define custom projections for each nested sigma, so that you never use the bare projections from a sigma type).

Lemma iso_set_isweq

Lemma iso_set_isweq is in precategories.v, with which it has nothing to do.

"iso" can be applied to objects in different precategories

... and that's mathematically strange and can cause confusion.

However, it might be sort of convenient if it would check at least that the two categories have the same morphisms, the same identity arrows, and the same composition operations, but not check that the proofs of the identities are the same. But even that might lead to confusion, so better not.

Here is the code that shows the problem.

Require Import RezkCompletion.precategories.
        Import pathnotations.PathNotations.
Local Notation "a --> b" := (precategory_morphisms a b)(at level 50).
Require Import Foundations.Generalities.uu0.
Require Import Foundations.hlevel2.hSet.

(* make two precategories with the same objects *)
Parameter o : Type.
Parameter m m' : o -> o -> Type.
Parameter is : forall (c d:o), isaset (m c d).
Parameter is': forall (c d:o), isaset (m' c d).
Parameter id : forall c:o, m c c.
Parameter id': forall c:o, m' c c.
Parameter co : forall {c d e:o} (f:m c d) (g:m d e), m c e.
Parameter co': forall {c d e:o} (f:m' c d) (g:m' d e), m' c e.
Parameter rg: forall (c d:o) (f:m c d), co (id c) f == f.
Parameter lf: forall (c d:o) (f:m c d), co f (id d) == f.
Parameter rg': forall (c d:o) (f:m' c d), co' (id' c) f == f.
Parameter lf': forall (c d:o) (f:m' c d), co' f (id' d) == f.
Parameter ass: forall (a b c d : o)
                      (f : m a b) (g : m b c) (h : m c d),
                 co f (co g h) == co (co f g) h.
Parameter ass': forall (a b c d : o)
                      (f : m' a b) (g : m' b c) (h : m' c d),
                 co' f (co' g h) == co' (co' f g) h.

Definition precategory_pair (C:precategory_data) (i:is_precategory C)
  : precategory := tpair _ C i.

Definition makePrecategory 
    (obj : UU)
    (mor : obj -> obj -> UU)
    (imor : forall i j:obj, isaset (mor i j))
    (identity : forall i:obj, mor i i)
    (compose : forall (i j k:obj) (f:mor i j) (g:mor j k), mor i k)
    (right : forall (i j:obj) (f:mor i j), compose _ _ _ (identity i) f == f)
    (left  : forall (i j:obj) (f:mor i j), compose _ _ _ f (identity j) == f)
    (associativity : forall (a b c d:obj) (f:mor a b) (g:mor b c) (h:mor c d),
        compose _ _ _ f (compose _ _ _ g h) == compose _ _ _ (compose _ _ _ f g) h)
    : precategory.
  intros.
  set (C := precategory_data_pair
              (precategory_ob_mor_pair 
                 obj 
                 (fun i j:obj => hSetpair (mor i j) (imor i j))) identity compose).
  assert (iC : is_precategory C).
    split. split. exact right. exact left. exact associativity.
  exact (precategory_pair C iC).
Defined.    

Definition C := makePrecategory o m is id (@co) rg lf ass.
Definition C':= makePrecategory o m' is' id' (@co') rg' lf' ass'.

Definition funny (c:C) (c':C') := iso c c'.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.