issues
search
UniMath
/
agda-unimath
The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
211
stars
67
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Fix typos
#1156
pitmonticone
closed
5 days ago
0
Use box drawing characters in diagrams
#1155
fredrik-bakke
closed
1 week ago
1
Various website improvements
#1154
VojtechStep
closed
2 weeks ago
5
Path-cosplit maps
#1153
fredrik-bakke
closed
2 weeks ago
2
Fiberwise orthogonal maps and closure properties of the right class
#1152
fredrik-bakke
closed
3 weeks ago
0
Change equiv-comp to comp-equiv
#1151
EgbertRijke
closed
3 weeks ago
0
Identity systems of descent data for pushouts
#1150
VojtechStep
closed
2 weeks ago
1
Characterize identity types of dependent sequential diagrams
#1149
VojtechStep
closed
3 weeks ago
1
Characterization of various families over pushouts
#1148
VojtechStep
closed
2 weeks ago
0
`comp-equiv`
#1147
EgbertRijke
closed
3 weeks ago
0
Modal logic
#1146
spcfox
opened
3 weeks ago
1
Refactor the descent property of pushouts
#1145
VojtechStep
closed
3 weeks ago
0
Overview of SvDR20 formalization
#1144
VojtechStep
closed
2 weeks ago
3
Fix citation tag configuration for some references
#1143
fredrik-bakke
closed
1 month ago
1
Horizontal fiber condition for pullbacks
#1142
fredrik-bakke
opened
1 month ago
0
Use box-drawing characters for character diagrams
#1141
fredrik-bakke
closed
1 week ago
0
Descent and induction principle of identity types of coequalizers
#1140
VojtechStep
opened
1 month ago
0
subsequences and asymptotical properties
#1139
malarbol
opened
1 month ago
5
Add interactive library explorer
#1138
VojtechStep
opened
1 month ago
0
Refactor coproduct equivalences
#1137
morphismz
opened
1 month ago
1
Define null-homotopic maps
#1136
fredrik-bakke
opened
1 month ago
2
Fixing a link
#1135
FernandoChu
closed
1 month ago
0
Functoriality of the pullback-hom
#1134
fredrik-bakke
opened
1 month ago
0
Eckmann-Hilton Updates
#1133
morphismz
opened
1 month ago
5
Document external dependencies for building the website
#1132
VojtechStep
opened
1 month ago
0
Pin macOS version to one with Intel runners
#1131
VojtechStep
closed
1 month ago
0
Functoriality of morphisms of arrows
#1130
fredrik-bakke
opened
2 months ago
1
Zigzags of sequential diagrams
#1129
VojtechStep
closed
1 month ago
2
Add reference to MRR88 in files about apartness relations
#1128
fredrik-bakke
closed
1 month ago
0
Quasiidempotence is not a proposition
#1127
fredrik-bakke
closed
3 weeks ago
0
chore: Universal properties of colimits quantify over all universe levels
#1126
fredrik-bakke
closed
2 months ago
0
chore: Remove redundant parentheses in universe level expressions
#1125
fredrik-bakke
closed
2 months ago
0
chore: Fix arrowheads in character diagrams
#1124
fredrik-bakke
closed
2 months ago
0
Prove uniqueness of homotopy and equivalence induction
#1123
fredrik-bakke
opened
2 months ago
0
Postulating colimits
#1122
fredrik-bakke
opened
2 months ago
2
Rename `canonical-coequalizer` to `standard-coequalizer`
#1121
fredrik-bakke
closed
2 months ago
0
Construct `compute-glue-cogap` from appropriate infrastructure
#1120
fredrik-bakke
opened
2 months ago
0
Postulate components of coherent two-sided inverses for function extensionality and univalence
#1119
fredrik-bakke
closed
2 months ago
0
Simplicial Type Theory
#1118
fredrik-bakke
opened
2 months ago
0
Equivalences are closed under "transfinite composition"
#1117
VojtechStep
closed
2 months ago
0
Central H-spaces
#1116
EgbertRijke
opened
2 months ago
2
The loop of any circle is nontrivial
#1115
EgbertRijke
closed
2 months ago
3
Fix line height in lists
#1114
VojtechStep
closed
2 months ago
0
Acyclic maps are closed under retracts
#1113
tomdjong
closed
2 months ago
1
Hereditary W-types
#1112
EgbertRijke
closed
2 months ago
3
The discrete field of rational numbers
#1111
malarbol
closed
2 months ago
13
Plane trees
#1110
EgbertRijke
closed
2 months ago
1
Descent data for sequential colimits and its version of the flattening lemma
#1109
VojtechStep
closed
2 months ago
1
chore: Rename `universal-property-surj` to `universal-property-surjection`
#1108
fredrik-bakke
closed
2 months ago
0
The commutative ring of rational numbers
#1107
malarbol
closed
2 months ago
6
Next