feat: port/CategoryTheory.StructuredArrow (#2486)

Co-authored-by: adamtopaz <github@adamtopaz.com>
leanprover-community · Mar 2, 2023 · 064dbd9 · 064dbd9
1 parent 3ea0b02
commit 064dbd9
Show file tree

Hide file tree

Showing 3 changed files with 631 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -310,6 +310,7 @@ import Mathlib.CategoryTheory.Products.Bifunctor
 import Mathlib.CategoryTheory.Quotient
 import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.Skeletal
+import Mathlib.CategoryTheory.StructuredArrow
 import Mathlib.CategoryTheory.Sums.Associator
 import Mathlib.CategoryTheory.Sums.Basic
 import Mathlib.CategoryTheory.Thin

diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -105,6 +105,9 @@ instance [Subsingleton α] : Subsingleton (Discrete α) :=
     ext
     apply Subsingleton.elim⟩
 
+instance (X Y : Discrete α) : Subsingleton (X ⟶ Y) :=
+  show Subsingleton (ULift (PLift _)) from inferInstance
+
 /-
 Porting note: It seems that `aesop` currently has no way to add lemmas locally.