issues
search
maxsnew
/
cubical-categorical-logic
Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
25
stars
5
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Create LICENSE
#66
stschaef
closed
8 months ago
1
spin off Weaken, Reindex files. Implement a usable version of reindex
#65
maxsnew
closed
8 months ago
0
Add a LICENSE
#64
maxsnew
closed
8 months ago
1
Prove SETᴰ is a fibration
#63
maxsnew
closed
8 months ago
1
Properties of SETᴰ
#62
maxsnew
closed
5 months ago
2
Properties of Reindexing
#61
maxsnew
closed
5 months ago
5
Free Cartesian Category
#60
maxsnew
closed
5 months ago
1
Functor comprehension simplification
#59
maxsnew
closed
8 months ago
0
Identity Systems
#58
maxsnew
opened
9 months ago
0
Free Cartesian Category
#57
hejohns
closed
5 months ago
7
Gluing Posets
#56
maxsnew
opened
9 months ago
0
Eliminators for Stdlib Data Typs
#55
maxsnew
opened
9 months ago
0
Wide Subcategories
#54
maxsnew
closed
3 months ago
2
Rezk by hit
#53
maxsnew
opened
9 months ago
0
Use Preorder and Preorder^D Less
#52
maxsnew
closed
8 months ago
1
New profunctors
#51
maxsnew
closed
9 months ago
2
CI Broken
#50
maxsnew
closed
9 months ago
1
New free functor
#49
maxsnew
closed
9 months ago
2
Right adjoints in product category
#48
stschaef
closed
9 months ago
5
Alternative definition of Free Functor that avoids needing Eq
#47
maxsnew
closed
1 year ago
1
Reindexing a displayed category
#46
maxsnew
closed
9 months ago
1
Displayed Universal Properties
#45
maxsnew
closed
1 year ago
1
fix line lengths
#44
maxsnew
closed
1 year ago
0
Adding workaround and refactor monotone
#43
GenericMonkey
closed
1 year ago
0
Freecat refactor
#42
maxsnew
closed
1 year ago
0
Preorder Refactor
#41
GenericMonkey
closed
1 year ago
0
Universal element prop
#40
maxsnew
closed
1 year ago
0
update to cubical HEAD
#39
maxsnew
closed
1 year ago
0
Changes in Upstream Cubical
#38
stschaef
closed
1 year ago
3
Grothendieck forgetful functor
#37
stschaef
closed
1 year ago
4
Functor Comprehension Principle/Principle of Unique Choice
#36
maxsnew
closed
8 months ago
5
Refactor of Poset Cat with Grothendieck Construction
#35
GenericMonkey
closed
1 year ago
5
Construct the Presheaf of Subobjects
#34
maxsnew
closed
9 months ago
8
CI: Ignoring Paths to Documentation
#33
GenericMonkey
closed
1 year ago
0
Modular Formulation of Preorders, Posets, HeytAlg, etc
#32
GenericMonkey
closed
8 months ago
4
Defining Hyperdoctrine
#31
GenericMonkey
closed
1 year ago
5
Alt Binary Product of Categories
#30
maxsnew
closed
1 year ago
2
fix ANOTHER typo
#29
stschaef
closed
1 year ago
0
Finish CI setup : fix typo in main.yml
#28
stschaef
closed
1 year ago
0
Set Up CI
#27
stschaef
closed
1 year ago
3
Set up some CI
#26
maxsnew
closed
1 year ago
6
Bifunctor prof
#25
stschaef
closed
1 year ago
1
Monad From Adjunction
#24
stschaef
closed
1 year ago
0
Monad from Adjunction
#23
GenericMonkey
closed
1 year ago
4
Rezk by HIT
#22
hejohns
closed
9 months ago
1
Environment Comonad
#21
maxsnew
closed
1 year ago
1
Category Solver Bug?
#20
stschaef
closed
1 year ago
2
Profunctor Equivalence Isos
#19
GenericMonkey
closed
1 year ago
1
Adjoints
#18
maxsnew
closed
6 months ago
3
Profunctor function defs merged in
#17
stschaef
closed
1 year ago
0
Previous
Next