maxsnew/cubical-categorical-logic

Issues

• Redundancy

  #116 opened 2 months ago by maxsnew
  0

• Better Elimination principles for Local Sections?

  #70 opened 3 months ago by maxsnew
  1

• CI is Broken

  #113 opened 3 months ago by maxsnew
  4

• Agda bug

  #114 opened 3 months ago by maxsnew
  1

• Displayed Reasoning changes upstream

  #110 opened 4 months ago by maxsnew
  2

• Add caching to the CI

  #109 opened 4 months ago by stschaef
  0

• Gluing for CCCs

  #6 opened 2 years ago by maxsnew
  5

• Wide Subcategories

  #54 opened 5 months ago by maxsnew
  2

• Update UMP.agda, NaturalModels/, Syntax/ to build again

  #91 opened 8 months ago by hejohns
  2

• Cartesian Closed Structure on Presheaf Category

  #97 opened 5 months ago by bond15
  4

• citation file

  #103 opened 6 months ago by maxsnew
  0

• Free Cartesian Category

  #60 opened 7 months ago by maxsnew
  1

• Properties of Reindexing

  #61 opened 7 months ago by maxsnew
  5

• Properties of SETᴰ

  #62 opened 7 months ago by maxsnew
  2

• Recursor for free cartesian categories

  #75 opened 7 months ago by maxsnew
  1

• Check Line Length error

  #98 opened 7 months ago by maxsnew
  17

• Move CI line length check to a tracked script?

  #85 opened 8 months ago by hejohns
  2

• Relative Monad Theory

  #77 opened 8 months ago by maxsnew
  1

• incremental Makefile

  #89 opened 8 months ago by maxsnew
  3

• Sync with cubical

  #87 opened 8 months ago by maxsnew
  1

• Peg CI to specific commits

  #84 opened 8 months ago by maxsnew
  4

• Adjoints

  #18 opened 8 months ago by maxsnew
  3

• Some Equivalences of Categories

  #8 opened 8 months ago by maxsnew
  6

• Worlds for the Schanuel Topos

  #72 opened 9 months ago by maxsnew
  1

• Day Convolution Monoidal Structure

  #71 opened 9 months ago by maxsnew
  1

• Displayed Category of Displayed Functors

  #68 opened 10 months ago by maxsnew
  2

• Add a LICENSE

  #64 opened 10 months ago by maxsnew
  1

• Collect recent things in a PR to Cubical

  #16 opened 10 months ago by maxsnew
  4

• Modular Formulation of Preorders, Posets, HeytAlg, etc

  #32 opened 10 months ago by GenericMonkey
  4

• Use Preorder and Preorder^D Less

  #52 opened 10 months ago by maxsnew
  1

• Functor Comprehension Principle/Principle of Unique Choice

  #36 opened 10 months ago by maxsnew
  5

• Identity Systems

  #58 opened a year ago by maxsnew
  0

• Gluing Posets

  #56 opened a year ago by maxsnew
  0

• Eliminators for Stdlib Data Typs

  #55 opened a year ago by maxsnew
  0

• CI Broken

  #50 opened a year ago by maxsnew
  1

• Construct the Presheaf of Subobjects

  #34 opened a year ago by maxsnew
  8

• Reindexing a displayed category

  #46 opened a year ago by maxsnew
  1

• Completeness for CT Structure Semantics of STT

  #5 opened a year ago by maxsnew
  1

• Distributive Coproducts

  #4 opened a year ago by maxsnew
  6

• Define Typal Universal properties for CT Structures

  #2 opened a year ago by maxsnew
  1

• Applications of Univalence

  #1 opened a year ago by maxsnew
  2

• Changes in Upstream Cubical

  #38 opened a year ago by stschaef
  3

• Set up some CI

  #26 opened 2 years ago by maxsnew
  6

• Alt Binary Product of Categories

  #30 opened 2 years ago by maxsnew
  2

• Monad from Adjunction

  #23 opened 2 years ago by GenericMonkey
  4

• Environment Comonad

  #21 opened 2 years ago by maxsnew
  1

• Exponentials

  #3 opened 2 years ago by maxsnew
  3

• Category Solver Bug?

  #20 opened 2 years ago by stschaef
  2

• Prove Parameterized Representability =~ NatIso

  #7 opened 2 years ago by maxsnew
  6

• Tactics/Solvers

  #9 opened 2 years ago by maxsnew
  6