All pull requests

Pull requests

• use with…in for maybe-injective

  #659·plt-amy opened Sep 8, 2026Member·

  ·
  1

• fixup: use ℓ for all type indicies in 1Lab.Path

  #657·sapphire-arches opened Aug 17, 2026·

  ·
  2

• Weighted colimits

  #652·TOTBWF opened Jul 21, 2026Collaborator·

  ·
  4

• Dependent products in categories

  #634·finegeometer opened Jun 17, 2026Contributor·

  ·
  2

• Refactor Cat.Displayed.Univalence.Thin

  #622·aathn opened Apr 20, 2026Contributor·

  ·
  4

• wip: lax slices of bicategories

  #617·plt-amy opened Apr 3, 2026Member·

  ·
  2

• Sorted Maps

  #581·olynch opened Jan 14, 2026·

  ·
  25

• defn: extensionality for ↯

  #569·plt-amy opened Sep 20, 2025Member·

  ·
  7

• Displayed Bicategories

  #549·mmcqd opened Aug 20, 2025Contributor·

  ·
  11

• Ordinals

  #545·finegeometer opened Aug 16, 2025Contributor·

  ·
  19

• Sigma bases

  #505·TOTBWF opened Jun 6, 2025Collaborator·

  ·
  1

• Stlc theory

  #454·jake-87 opened Jan 8, 2025Contributor·

  ·
  92

• Point-set topology

  #424·TOTBWF opened Aug 8, 2024Collaborator·

  ·

• Simplex Category

  #375·TOTBWF opened Apr 12, 2024Collaborator·

  ·
  3

• Left and right lifts along a displayed cat.

  #343·patrick-nicodemus opened Jan 14, 2024Contributor·

  ·
  18

• defn: two point circle

  #324·KevOrr opened Dec 19, 2023·

  ·
  9

• Isbell duality

  #322·formrre opened Dec 18, 2023·

  ·
  1

• Rewrite theory

  #238·TOTBWF opened Jul 1, 2023Collaborator·

  ·
  1

• Adjoint solver

  #235·TOTBWF opened Jun 1, 2023Collaborator·

  ·

• Left/Right Vertical Adjoints are (Op)Fibred, Optimize Diagram Fibration

  #223·TOTBWF opened May 5, 2023Collaborator·

  ·

• Allow using $source$ inside Markdown files

  #219·SquidDev opened Apr 30, 2023Collaborator·

  ·
  1

  3

• lambeks lemma without math prose

  #192·DavidWe9mann opened Feb 11, 2023·

  ·

• Duskin's Monadicity Theorem

  category-theoryenhancement
  #76·TOTBWF opened May 15, 2022Collaborator·

  ·
  1

  9