Commits

Breadcrumbs

History for

on25075fe

User selector

All users

All time

Commit History

Commits on Feb 26, 2026

• chore: remove no-longer-needed backwards compatibility options (#35737)

  Show description for f6a1b6e
  kim-em

  committed
  f6a1b6e

  Copy full SHA for f6a1b6e

Commits on Feb 24, 2026

• chore: bump toolchain to v4.29.0-rc2 (#35708)

  kim-em

  committed
  0c08ce9

  Copy full SHA for 0c08ce9

Commits on Jan 30, 2026

• feat(CategoryTheory/Iso): use `to_dual` for `X ≅ Y` (#34008)

  Show description for 52e75dc
  JovanGerb

  committed
  52e75dc

  Copy full SHA for 52e75dc

Commits on Jan 14, 2026

• feat(CategoryTheory/Functor): use `@[to_dual]` (#33237)

  Show description for 1d5e557
  JovanGerb

  committed
  1d5e557

  Copy full SHA for 1d5e557

Commits on Jan 7, 2026

• chore(CategoryTheory): fix whitespace (#33730)

  Show description for a1ecced
  harahu

  committed
  a1ecced

  Copy full SHA for a1ecced

Commits on Dec 31, 2025

• chore(CategoryTheory/Groupoid): replace `Groupoid.invFunctor` by `Groupoid.invEquivalence` (#33432)

  Show description for 7c25e87
  robin-carlier

  committed
  7c25e87

  Copy full SHA for 7c25e87

Commits on Dec 13, 2025

• chore: use `Category*` everywhere (#32842)

  Show description for dd97bd1
  robin-carlier

  committed
  dd97bd1

  Copy full SHA for dd97bd1

Commits on Nov 19, 2025

• chore: move Mathlib to the module system (#31786)

  Show description for 6a54a80
  

  kim-em

  and

  Kha

  committed
  6a54a80

  Copy full SHA for 6a54a80

Commits on Nov 15, 2025

• feat: free groupoid on a category, free-forgetful adjunction (#29279)

  Show description for d07fa9a
  

  Jlh18

  and

  joelriou

  committed
  d07fa9a

  Copy full SHA for d07fa9a

Commits on Oct 18, 2025

• chore(AlgebraicTopology): clean up FundamentalGroupoid (#28234)

  Show description for 2c2d756
  alreadydone

  committed
  2c2d756

  Copy full SHA for 2c2d756

Commits on Oct 9, 2025

• chore(*): rename note 'CategoryTheory universes' to 'category theory universes' (#30360)

  Show description for d12bacd
  Vierkantor

  committed
  d12bacd

  Copy full SHA for d12bacd

Commits on Aug 11, 2025

• refactor(CategoryTheory): have Functor not extend Prefunctor (#28106)

  Show description for ba407fd
  kim-em

  committed
  ba407fd

  Copy full SHA for ba407fd

Commits on Aug 5, 2025

• feat: replace aesop_cat with a configurable discharger (#27938)

  Show description for 9845f69
  kim-em

  committed
  9845f69

  Copy full SHA for 9845f69

Commits on Jun 13, 2025

• feat: add autoparams for proof fields of `Equiv` (#25350)

  Show description for e9bca4f
  thorimur

  committed
  e9bca4f

  Copy full SHA for e9bca4f

Commits on Apr 23, 2025

• refactor(CategoryTheory): redefine full subcategories using `ObjectProperty` (#22574)

  Show description for 0d61790
  joelriou

  committed
  0d61790

  Copy full SHA for 0d61790

Commits on Apr 2, 2025

• feat(CategoryTheory/Core): functors and natural transformations induced on cores (#23436)

  Show description for b581493
  robin-carlier

  committed
  b581493

  Copy full SHA for b581493

Commits on Mar 29, 2025

• feat(CategoryTheory/Groupoid): `IsGroupoid` typeclass (#23307)

  Show description for 40f3d5c
  robin-carlier

  committed
  40f3d5c

  Copy full SHA for 40f3d5c

Commits on Mar 3, 2025

• chore: bump toolchain to v4.18.0-rc1 (#22500)

  Show description for 6cecf71
  

  kim-em

  and

  jcommelin

  committed
  6cecf71

  Copy full SHA for 6cecf71

Commits on Jan 5, 2025

• chore: replace `aesop` with `simp` where possible (#20483)

  Show description for 95cdc7a
  kim-em

  committed
  95cdc7a

  Copy full SHA for 95cdc7a

Commits on Oct 14, 2024

• chore: unused arguments (#17348)

  kim-em

  committed
  2ed7908

  Copy full SHA for 2ed7908

Commits on Sep 24, 2024

• chore: update name in copyrights (#17074)

  kim-em

  committed
  30c481f

  Copy full SHA for 30c481f

Commits on Jul 19, 2024

• chore: remove `#align` and `#align_import` statements (#14887)

  Show description for 465f26f
  

  kim-em

  and

  mattrobball

  committed
  465f26f

  Copy full SHA for 465f26f

Commits on May 25, 2024

• RFC: normalise copyright headers (#13212)

  Show description for 6139350
  grunweg

  committed
  6139350

  Copy full SHA for 6139350

Commits on Aug 10, 2023

• chore: banish `Type _` and `Sort _` (#6499)

  Show description for 32de3f6
  mattrobball

  committed
  32de3f6

  Copy full SHA for 32de3f6

Commits on Jul 26, 2023

• chore: tidy various files (#5999)

  Ruben-VandeVelde

  committed
  415165e

  Copy full SHA for 415165e

Commits on Jul 19, 2023

• chore: script to replace headers with #align_import statements (#5979)

  Show description for 89aa3a3
  

  kim-em

  and

  eric-wieser

  committed
  89aa3a3

  Copy full SHA for 89aa3a3

Commits on Jun 9, 2023

• chore: review of automation in category theory (#4793)

  Show description for 5b95861
  

  kim-em

  and

  Scott Morrison

  committed
  5b95861

  Copy full SHA for 5b95861

Commits on Apr 10, 2023

• chore: forward port of #18742, no simps lemmas for Category.Hom (#3340)

  Show description for e44913f
  

  kim-em

  and

  joelriou

  committed
  e44913f

  Copy full SHA for e44913f

Commits on Mar 12, 2023

• chore: strip trailing spaces in lean files (#2828)

  Show description for 6ceb594
  eric-wieser

  committed
  6ceb594

  Copy full SHA for 6ceb594

Commits on Feb 15, 2023

• feat: port CategoryTheory.Groupoid (#2282)

  Show description for 8609239
  

  mattrobball

  and

  jcommelin

  committed
  8609239

  Copy full SHA for 8609239

Loading