🐪
- London, United Kingdom
-
08:17
(UTC)
Block or Report
Block or report Alizter
Report abuse
Contact GitHub support about this user’s behavior. Learn more about reporting abuse.
Report abusePinned
-
-
ejgallego/coq-lsp
ejgallego/coq-lsp PublicVisual Studio Code Extension and Language Server Protocol for Coq
-
-
coq-universe/coq-universe
coq-universe/coq-universe PublicWe aim to provide a composed build of all active Coq developments in existence
2,216 contributions in the last year
| Day of Week | February Feb | March Mar | April Apr | May May | June Jun | July Jul | August Aug | September Sep | October Oct | November Nov | December Dec | January Jan | February Feb | ||||||||||||||||||||||||||||||||||||||||
| Sunday Sun | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Monday Mon | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Tuesday Tue | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Wednesday Wed | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Thursday Thu | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Friday Fri | |||||||||||||||||||||||||||||||||||||||||||||||||||||
| Saturday Sat | |||||||||||||||||||||||||||||||||||||||||||||||||||||
Less
No contributions.
Low contributions.
Medium-low contributions.
Medium-high contributions.
High contributions.
More
Activity overview
Contribution activity
February 2024
Created 93 commits in 2 repositories
Created 1 repository
-
Alizter/alectryon
HTML
This contribution was made on Feb 9
Created a pull request in HoTT/Coq-HoTT that received 48 comments
flattening for pushouts + total space of Hopf construction
We use the colimits library to prove flattening for pushouts. The proof is a bit annoying as it doesn't compute well. We use this to show that the …
+110
−23
lines changed
•
48
comments
Opened 22 other pull requests in 2 repositories
HoTT/Coq-HoTT
3
open
18
merged
-
Smallness
This contribution was made on Feb 19
-
test: move Groups.Presentation tests to test/
This contribution was made on Feb 19
-
[8.18] bump minimal version to Coq 8.18
This contribution was made on Feb 19
-
surpress argument-scope-delimiter warning
This contribution was made on Feb 19
-
[8.19] fix % in Arguments warnings
This contribution was made on Feb 19
-
nix: update flake
This contribution was made on Feb 19
-
join construction
This contribution was made on Feb 19
-
flattening lemma for Coeq, Pushout and improvements to Hopf
This contribution was made on Feb 14
-
functoriality of GraphQuotient
This contribution was made on Feb 14
-
remove rewrite
This contribution was made on Feb 14
-
transport011: transport over 2 1-paths and lemmas about them
This contribution was made on Feb 14
-
add curried version of equiv_sigma_prod
This contribution was made on Feb 14
-
Flattening lemma for GraphQuotient
This contribution was made on Feb 14
-
characterize fiber of loop-susp counit
This contribution was made on Feb 12
-
various improvements to wedge
This contribution was made on Feb 12
-
diagonal map into binary product
This contribution was made on Feb 12
-
functoriality of binary coproducts
This contribution was made on Feb 12
-
put hor \/ notation in module
This contribution was made on Feb 12
-
pinch map of suspension
This contribution was made on Feb 12
-
wedge projections
This contribution was made on Feb 12
-
update alectryon
This contribution was made on Feb 12
NixOS/nixpkgs
1
merged
-
coqPackages.{serapi,coq-lsp}: {8.18.0+0.18.0,0.1.8+8.18.0} -> {8.19.0+0.19.0,0.1.8+8.19.0}
This contribution was made on Feb 12
Reviewed 19 pull requests in 2 repositories
HoTT/Coq-HoTT
18 pull requests
-
join construction
This contribution was made on Feb 19
-
Equivalences for displayed wild categories
This contribution was made on Feb 17
-
Miscellaneous things related to recent changes
This contribution was made on Feb 15
-
flattening lemma for Coeq, Pushout and improvements to Hopf
This contribution was made on Feb 14
-
functoriality of GraphQuotient
This contribution was made on Feb 14
-
remove rewrite
This contribution was made on Feb 14
-
Flattening lemma for GraphQuotient
This contribution was made on Feb 14
-
transport011: transport over 2 1-paths and lemmas about them
This contribution was made on Feb 14
-
characterize fiber of loop-susp counit
This contribution was made on Feb 13
-
functoriality of binary coproducts
This contribution was made on Feb 13
-
Makefile.coq.local: reduce long line warnings in alectryon build
This contribution was made on Feb 12
-
pinch map of suspension
This contribution was made on Feb 12
-
Colimits and Hopf: clean up and speed up
This contribution was made on Feb 12
-
flattening for pushouts + total space of Hopf construction
This contribution was made on Feb 12
-
Reduce dependencies, especially for Classes
This contribution was made on Feb 10
-
WildCat/Induced: add and use intros_of_type tactic
This contribution was made on Feb 8
-
WildCat/Induced: various minor simplifications
This contribution was made on Feb 8
-
ReflectiveSubuniverse: simplify universe vars in conn_map_homotopic
This contribution was made on Feb 6
Alizter/HoTT
1 pull request
-
Diagnose bad coercion
This contribution was made on Feb 20
Created an issue in HoTT/Coq-HoTT that received 2 comments
Split HIT files into Core and lemmas
We should split the various HIT files like GraphQuotient, Coeq, Pushout into separate files like we do for Join which will make the compilation fas…
2
comments
Opened 1 other issue in 1 repository
HoTT/Coq-HoTT
1
closed
-
Add transport lemmas for families of equivalences
This contribution was made on Feb 11
Started 1 discussion in 1 repository
plt-amy/1lab
plt-amy/1lab
-
Weak displayed monos and epis
This contribution was made on Feb 16





