Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: Coq

Bottom of Page

1 to 15 of 15

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2011

    I have been trying to collect some information at Coq.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2011

    I have added to the References-section at Coq

    • a pointer to a web-interface that runs Coq;

    • a pointer to a tool that allows to display Coq proofs from static Coq-files without having to load everything into a Coq-system itself.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 24th 2011

    Jelle Herold kindly added a section learning Coq to Coq.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 24th 2011

    Yes, that was kind! Thank you, Jelle.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 24th 2011
    • (edited Nov 24th 2011)

    Since one needs to have already some experience with the Coq software environment in order to know what to do (and to think) when stumbling across a page like https://github.com/andrejbauer/Homotopy/tree/master/OberwolfachTutorial, and since it never occured to me (!) that I need to click on the word “raw” in order to get a pdf-file, I have split the pointer to that tutorial off as a category: Reference-entry

    Oberwolfach HoTT-Coq tutorial,

    uploaded the pdf there, and added some directions.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2019
    • (edited Jun 18th 2019)

    added pointer to

    • jsCoq, a ready-to-use online Coq environment

    diff, v29, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2019
    • (edited Jun 18th 2019)

    and also to

    diff, v30, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2019

    beautified the formatting of this reference:

    but this seems a little thin a pointer. Any expert who cares about whatever issue is meant to be pointed out here might want to expand just a bit.

    diff, v30, current

    • CommentRowNumber9.
    • CommentAuthoratmacen
    • CommentTimeJun 18th 2019

    Re #8: I’m not sure what you think is missing that would make sense to put on this page: O’Connor already says that ordinal analysis techniques don’t currently handle Coq’s theory, and some may find this worrisome.

    Wait you mean to put something like what I just wrote next to the link?

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJun 18th 2019

    Yes! The entry deserves to be expanded a little here and there by some expert. Think of all the kids that visit this page.

    • CommentRowNumber11.
    • CommentAuthoratmacen
    • CommentTimeJun 19th 2019

    Changed the parenthetical summary of the “Believing In-Consistency” reference. It now links to ordinal analysis instead of predicativity. They’re related, but O’Connor focuses on ordinal analysis.

    diff, v31, current

    • CommentRowNumber12.
    • CommentAuthoratmacen
    • CommentTimeJun 19th 2019

    Added a “Relation to Predicativity” subsection to ordinal analysis to compensate. I hope these changes are not too far off what you wanted.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJun 19th 2019

    Yes, thanks for doing this.

    • CommentRowNumber14.
    • CommentAuthorHugo Herbelin
    • CommentTimeNov 12th 2022

    Add the connection between Coq and the acronym CoC.

    diff, v33, current

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2022

    added pointer to:

    diff, v34, current

1 to 15 of 15

  1.