Skip to content

History / CoqAndAxioms

Edit page New page

Revisions

  • Mention UIP and other variants of axiom K; clarify how proof-irrelevance and axiom K are in general orthogonal

    @herbelin herbelin committed Apr 21, 2024
    87841be

  • fix typo

    @davidjao davidjao committed Jan 26, 2022
    8a22f90

  • Revert e695c0349b0cdd7f888e634c91a06e83400bbf3e...dcfde3c3431cdeab893613aa8d291a5c0fa99b64 on CoqAndAxioms

    @NoLongerBreathedIn NoLongerBreathedIn committed Oct 2, 2021
    fd24081

  • Homotopy type theory with univalence proves dependent functional extensionality and propositional extensionality, merges ex, sig, and sigT, and violates Axiom K.

    @NoLongerBreathedIn NoLongerBreathedIn committed Sep 28, 2021
    dcfde3c

  • Updated CoqAndAxioms (markdown)

    @anton-trunov anton-trunov committed Aug 6, 2019
    e695c03

  • Updated CoqAndAxioms (markdown)

    Mike Solomon committed Aug 6, 2019
    7ec1fbe

  • Updated CoqAndAxioms (markdown)

    @soraros soraros committed May 12, 2019
    d4f2548

  • syntax highlighting (part 1)

    @letouzey letouzey committed Oct 26, 2017
    2de1e38

  • conversion from rst to markdown via pandoc

    root committed Oct 11, 2017
    d00fb45

  • Converted to reStructuredText via moin2rst

    root committed Oct 11, 2017
    8e866ca

  • No commit message

    @charguer charguer committed Oct 11, 2017
    5fc26d3