HoTT/Coq-HoTT issues and pull requests

#100 - Unit in Prop ??

Issue - State: closed - Opened by spitters over 11 years ago - 4 comments

#100 - Unit in Prop ??

Issue - State: closed - Opened by spitters over 11 years ago - 4 comments

#99 - FunextAxiom gives Universe inconsistency

Issue - State: closed - Opened by spitters over 11 years ago - 29 comments

#99 - FunextAxiom gives Universe inconsistency

Issue - State: closed - Opened by spitters over 11 years ago - 29 comments

#98 - Pullbacks?

Issue - State: closed - Opened by spitters over 11 years ago - 3 comments

#98 - Pullbacks?

Issue - State: closed - Opened by spitters over 11 years ago - 3 comments

#97 - simplified flattening lemma, via some new lemmas elsewhere

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#97 - simplified flattening lemma, via some new lemmas elsewhere

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#96 - The Flattening Lemma

Pull Request - State: closed - Opened by mikeshulman over 11 years ago - 1 comment

#96 - The Flattening Lemma

Pull Request - State: closed - Opened by mikeshulman over 11 years ago - 1 comment

#95 - Added axiom export files.

Pull Request - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 4 comments

#95 - Added axiom export files.

Pull Request - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 4 comments

#94 - Some mote PathGroupoid operations

Pull Request - State: closed - Opened by peterlefanulumsdaine over 11 years ago

#94 - Some mote PathGroupoid operations

Pull Request - State: closed - Opened by peterlefanulumsdaine over 11 years ago

#93 - HoTT does not export EquivalenceVarieties

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#93 - HoTT does not export EquivalenceVarieties

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#92 - port 2Sphere1 and Pi1S2 from Dan Licata's Agda Library

Issue - State: closed - Opened by mdnahas over 11 years ago - 6 comments

#92 - port 2Sphere1 and Pi1S2 from Dan Licata's Agda Library

Issue - State: closed - Opened by mdnahas over 11 years ago - 6 comments

#91 - types/Arrow.v

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#91 - types/Arrow.v

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#90 - Add Kristina's better proof that IsEquiv is an hprop.

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#90 - Add Kristina's better proof that IsEquiv is an hprop.

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#89 - naming and arguments for contr_equiv and trunc_equiv

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#89 - naming and arguments for contr_equiv and trunc_equiv

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#88 - HITs: S1 and Interval

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#87 - Notation 'idmap'

Issue - State: closed - Opened by JasonGross over 11 years ago - 10 comments

#87 - Notation 'idmap'

Issue - State: closed - Opened by JasonGross over 11 years ago - 10 comments

#86 - Fixing HProp

Pull Request - State: closed - Opened by spitters over 11 years ago

#86 - Fixing HProp

Pull Request - State: closed - Opened by spitters over 11 years ago

#85 - improve "make clean" and change some identifier names

Pull Request - State: closed - Opened by DanGrayson over 11 years ago

#84 - Comparing notions of equivalence (with some other minor changes)

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#83 - types/Paths: basically finished

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#82 - types/Forall

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#81 - Define projT2_path in terms of things we know.

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#80 - Some additions to Forall.v

Pull Request - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#79 - Shuffle around the locations of some things, eliminate some duplicate lemmas

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#78 - now I think Empty.v is done

Pull Request - State: closed - Opened by DanGrayson over 11 years ago

#77 - a few updates to types/Prod

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#76 - types/Sigma

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#75 - Empty is done

Pull Request - State: closed - Opened by DanGrayson over 11 years ago

#74 - added a few lemmas. "cancel" now means "unwhisker".

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#73 - remove an extra definition of HProp from Empty

Pull Request - State: closed - Opened by DanGrayson over 11 years ago

#72 - Port Automation

Issue - State: closed - Opened by spitters over 11 years ago - 8 comments

#71 - types/Unit

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#70 - types/Prod: add the negative universal property

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#69 - Port HSet (from old HoTT)

Issue - State: closed - Opened by mikeshulman over 11 years ago - 2 comments

#68 - a few small things

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#67 - Hlevels

Pull Request - State: closed - Opened by mikeshulman over 11 years ago - 2 comments

#66 - Added notation [==] for pointwise function equality

Pull Request - State: closed - Opened by peterlefanulumsdaine over 11 years ago

#65 - Greatly improved Record tactics, thanks to help from Jason Gross

Pull Request - State: closed - Opened by mikeshulman over 11 years ago - 6 comments

#64 - transport_forall_unwound is unnecessary

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#63 - Correct arguments to equiv_compose, and simplify equiv_Transitive.

Pull Request - State: closed - Opened by mikeshulman over 11 years ago - 2 comments

#62 - TypeClasses for Refl, Sym, Trans applied to Paths and Equiv.

Pull Request - State: closed - Opened by mdnahas over 11 years ago - 4 comments

#61 - Added acceptable tactics from Jason

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#60 - Draft of a style guide

Pull Request - State: closed - Opened by mikeshulman over 11 years ago

#59 - Added a convenience file theories/HoTT.v which exports the rest of the librarary

Pull Request - State: closed - Opened by andrejbauer over 11 years ago

#58 - Complete types/Record

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 3 comments

#57 - Complete types/Universe

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#56 - Complete types/Bool

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#55 - Complete types/Empty[Set]

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 3 comments

#54 - Complete types/Unit

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago

#53 - Complete types/Sum

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 2 comments

#52 - Complete types/Prod

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 3 comments

#51 - complete types/Sigma

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago

#50 - Complete types/Arrow

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago

#49 - Complete types/Forall

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 7 comments

#48 - Complete types/Paths

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 12 comments

#47 - Port HLevel (from old HoTT)

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 4 comments

#46 - Port UnivalenceImpliesFunext (from old HoTT)

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#45 - Port Funext (from old HoTT)

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#44 - Port FiberEquivalences (from old HoTT)

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#43 - Port FiberSequences (from old HoTT)

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#42 - Port FunextEquivalences (from old HoTT)

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#41 - Port UsefulEquivalences (from old HoTT)

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago - 1 comment

#40 - Style Guide

Issue - State: closed - Opened by peterlefanulumsdaine over 11 years ago

#39 - "only global references can be polymorphic hints"

Issue - State: closed - Opened by DanGrayson over 11 years ago - 2 comments

#38 - Mike's Record tactics and a fix in hoqide

Pull Request - State: closed - Opened by andrejbauer over 11 years ago

#37 - Improvements to the library, optional compilation of ssreflect (because it is currently broken)

Pull Request - State: closed - Opened by andrejbauer over 11 years ago - 12 comments

#36 - fix dependencies

Pull Request - State: closed - Opened by DanGrayson almost 12 years ago

#35 - Stand-alone?

Issue - State: closed - Opened by andrejbauer almost 12 years ago - 4 comments

#34 - Equivalences

Issue - State: closed - Opened by andrejbauer almost 12 years ago - 16 comments

#33 - Contractible.v

Issue - State: closed - Opened by andrejbauer almost 12 years ago - 1 comment

#32 - Transport.v

Issue - State: closed - Opened by andrejbauer almost 12 years ago - 1 comment

#31 - Placing the new ssreflect-like version of HoTT onto the main repo.

Pull Request - State: closed - Opened by andrejbauer almost 12 years ago

#30 - In the absence of "contradict"

Issue - State: closed - Opened by jcmckeown almost 12 years ago - 2 comments

#29 - Added lemma [forall_hlevel], that h-levels are closed under arbitrary products.

Pull Request - State: closed - Opened by peterlefanulumsdaine almost 12 years ago

#28 - Ssreflect compiles with HoTT automatically

Pull Request - State: closed - Opened by andrejbauer almost 12 years ago

#27 - make constructions compile again

Pull Request - State: closed - Opened by benediktahrens almost 12 years ago

#26 - Ssrhott

Pull Request - State: closed - Opened by amahboubi almost 12 years ago

#25 - removed detour in path construction

Pull Request - State: closed - Opened by benediktahrens almost 12 years ago

#24 - fix dependencies

Pull Request - State: closed - Opened by DanGrayson almost 12 years ago

#23 - Fiddling with ssreflect

Pull Request - State: closed - Opened by andrejbauer almost 12 years ago

#22 - Still trying to get ssreflect to compile with hott

Pull Request - State: closed - Opened by andrejbauer almost 12 years ago

#21 - Setting things up so we can work on ssreflect plugin for hoq

Pull Request - State: closed - Opened by andrejbauer almost 12 years ago

#20 - Equiv as total space

Pull Request - State: closed - Opened by benediktahrens almost 12 years ago - 3 comments

#19 - Init/Datatypes.v: prod as sigma

Pull Request - State: closed - Opened by benediktahrens almost 12 years ago - 4 comments

#18 - Support for hoqide and changing notation for paths from == to =

Pull Request - State: closed - Opened by andrejbauer almost 12 years ago

#17 - Improved installation procedure

Pull Request - State: closed - Opened by andrejbauer almost 12 years ago

#16 - Major cleanup, usage of custom Coq version

Pull Request - State: closed - Opened by andrejbauer almost 12 years ago

#15 - Compatibility with Coq 8.4

Pull Request - State: closed - Opened by andrejbauer about 12 years ago - 2 comments

GitHub / HoTT/Coq-HoTT issues and pull requests