diff --git a/Mathlib.lean b/Mathlib.lean
index be073f34caf9ad..126eabbc4fd9d8 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1950,6 +1950,8 @@ import Mathlib.CategoryTheory.Category.PartialFun
 import Mathlib.CategoryTheory.Category.Pointed
 import Mathlib.CategoryTheory.Category.Preorder
 import Mathlib.CategoryTheory.Category.Quiv
+import Mathlib.CategoryTheory.Category.Quiv.Shapes
+import Mathlib.CategoryTheory.Category.Quiv.WalkingQuiver
 import Mathlib.CategoryTheory.Category.ReflQuiv
 import Mathlib.CategoryTheory.Category.RelCat
 import Mathlib.CategoryTheory.Category.TwoP
diff --git a/Mathlib/CategoryTheory/Category/Quiv/Shapes.lean b/Mathlib/CategoryTheory/Category/Quiv/Shapes.lean
new file mode 100644
index 00000000000000..e20841d0536cde
--- /dev/null
+++ b/Mathlib/CategoryTheory/Category/Quiv/Shapes.lean
@@ -0,0 +1,207 @@
+/-
+Copyright (c) 2025 Robert Maxton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Robert Maxton
+-/
+
+import Mathlib.CategoryTheory.Category.Quiv
+import Mathlib.CategoryTheory.Limits.Shapes.Terminal
+import Mathlib.CategoryTheory.Generator.Basic
+
+/-!# Shapes in Quiv
+
+In this file, we define a number of quivers, most of which have corresponding notations:
+* The `Empty` quiver, which is initial
+* The single-vertex zero-edge quiver `Vert`, with the notation `⋆`
+* The single-vertex single-edge quiver `Point`, with the notation `⭮`, which is terminal
+* The `Interval` quiver, with the notation `𝕀`
+
+All notations are duplicated: once for when universe levels can be inferred, and once to
+allow explicit universe levels to be given.
+
+## TODO
+* The subobject classifier in `Quiv`
+
+-/
+
+namespace CategoryTheory.Quiv
+universe v u v₁ u₁ v₂ u₂
+open Limits
+
+/-- The empty quiver, with no vertices and no edges. -/
+def Empty := let _ := PUnit.{v}; PEmpty.{u + 1}
+
+instance : Quiver.{v + 1} Empty.{v} where
+  Hom _ _ := PEmpty
+
+instance : IsEmpty Empty where
+  false := PEmpty.elim
+
+/-- The single-vertex quiver, with one vertex and no edges. -/
+def Vert := let _ := PUnit.{v}; PUnit.{u + 1}
+
+instance : Quiver.{v + 1} Vert.{v} where
+  Hom _ _ := PEmpty
+
+@[inherit_doc Vert] scoped notation "⋆" => Vert
+set_option quotPrecheck false in
+@[inherit_doc Vert] scoped notation "⋆.{" v ", " u "}" => Vert.{v, u}
+
+/-- Prefunctors out of `⋆` are just single objects. -/
+def Vert.prefunctor {V : Type u₂} [Quiver.{v₂} V] (v : V) : ⋆.{v₁, u₁} ⥤q V :=
+  {obj := fun _ ↦ v, map := nofun}
+
+/-- Prefunctors out of `⋆` are equal if they point to the same object. -/
+@[ext]
+lemma Vert.prefunctor.ext {V : Type u₂} [Quiver.{v₂} V] {F G : ⋆.{v₁, u₁} ⥤q V}
+    (h : F.obj ⟨⟩ = G.obj ⟨⟩) : F = G := by
+  rcases F with ⟨F_obj, F_map⟩; rcases G with ⟨G_obj, G_map⟩
+  simp at h
+  rw [Prefunctor.mk.injEq]
+  constructor
+  · ext ⟨⟩; exact h
+  · apply Function.hfunext rfl
+    rintro ⟨⟩ ⟨⟩ -
+    apply Function.hfunext rfl
+    rintro ⟨⟩ ⟨⟩ -
+    apply Function.hfunext rfl
+    rintro ⟨⟩
+
+/-- The interval quiver, with two points and a single edge `.left ⟶ .right`. -/
+def Interval := let _ := PUnit.{v}; ULift.{u} WalkingPair
+
+instance : Quiver.{v + 1} Interval.{v} where
+  Hom
+  | .up .left, .up .right => PUnit
+  | _, _ => PEmpty
+
+@[inherit_doc Interval] scoped notation "𝕀" => Interval
+set_option quotPrecheck false in
+@[inherit_doc Interval] scoped notation "𝕀.{" v ", " u "}" => Interval.{v, u}
+
+/-- The left point of `𝕀`. -/
+@[match_pattern] def Interval.left : 𝕀 := .up .left
+/-- The right point of `𝕀`. -/
+@[match_pattern] def Interval.right : 𝕀 := .up .right
+
+@[match_pattern] alias 𝕀.left := Interval.left
+@[match_pattern] alias 𝕀.right := Interval.right
+
+@[simps] instance : Zero 𝕀 := ⟨Interval.left⟩
+@[simps] instance : One 𝕀 := ⟨Interval.right⟩
+
+/-- The single edge of `𝕀`. -/
+@[simp, match_pattern] def Interval.hom : (0 : 𝕀.{v, u}) ⟶ 1 := ⟨⟩
+
+alias 𝕀.hom := Interval.hom
+
+/-- Convenience eliminator for building data on `𝕀.hom`.
+
+Can't be a `cases_eliminator` or Lean will try to use it on every morphism in every quiver. -/
+@[elab_as_elim]
+def Interval.casesOn_hom {motive : {X Y : 𝕀} → (X ⟶ Y) → Sort*}
+    {X Y : 𝕀} (f : X ⟶ Y) (hom : motive Interval.hom) : motive f :=
+  match X, Y, f with
+  | Interval.left, Interval.right, _ => hom
+
+/-- Prefunctors out of `𝕀` are just single homs. -/
+def Interval.prefunctor {V : Type u₂} [Quiver.{v₂} V] {X Y : V} (f : X ⟶ Y) : 𝕀.{u₁, v₁} ⥤q V :=
+  { obj := fun | Interval.left => X | Interval.right => Y,
+    map := @fun | Interval.left, Interval.right, Interval.hom => f }
+
+/-- Prefunctors out of `𝕀` are equal if they point to the same hom. -/
+@[ext (iff := false)]
+lemma Interval.prefunctor.ext {V : Type u₂} [Quiver.{v₂} V] {F G : 𝕀.{u₁, v₁} ⥤q V}
+    (h₀ : F.obj 0 = G.obj 0) (h₁ : F.obj 1 = G.obj 1)
+    (h : F.map Interval.hom = Quiver.homOfEq (G.map Interval.hom) h₀.symm h₁.symm) : F = G := by
+  rcases F with ⟨F_obj, F_map⟩; rcases G with ⟨G_obj, G_map⟩
+  -- simp at h₀ h₁ h
+  rw [Prefunctor.mk.injEq]
+  constructor
+  · ext (Interval.left | Interval.right) <;> simpa
+  · apply Function.hfunext rfl
+    rintro X X' ⟨⟩
+    apply Function.hfunext rfl
+    rintro Y Y' ⟨⟩
+    apply Function.hfunext rfl
+    simp_rw [heq_eq_eq, forall_eq']
+    rintro f
+    cases f using Interval.casesOn_hom
+    simp at h
+    simp [h, Quiver.homOfEq_heq]
+
+lemma Interval.prefunctor.ext_iff {V : Type u₂} [Quiver.{v₂} V] {F G : 𝕀.{u₁, v₁} ⥤q V} :
+    F = G ↔ ∃ (h₀ : F.obj 0 = G.obj 0) (h₁ : F.obj 1 = G.obj 1),
+      F.map Interval.hom = Quiver.homOfEq (G.map Interval.hom) h₀.symm h₁.symm := by
+  refine ⟨fun h => ?_, fun ⟨h₀, h₁, h⟩ => Interval.prefunctor.ext h₀ h₁ h⟩
+  subst h; simp
+
+/-- The topos-theory point as a quiver, with a single point (vertex with a self-loop) and no other
+vertices or edges. -/
+def Point := let _ := PUnit.{v}; PUnit.{u + 1}
+
+instance : Quiver.{v + 1} Point.{v} where
+  Hom _ _ := PUnit
+
+@[inherit_doc Point] scoped notation "⭮" => Point
+set_option quotPrecheck false in
+@[inherit_doc Point] scoped notation "⭮.{" v ", " u "}" => Point.{v, u}
+
+/-- Prefunctors out of `⭮` are just single self-arrows. -/
+def Point.prefunctor {V : Type u₂} [Quiver.{v₂} V] {v : V} (α : v ⟶ v) : ⭮.{v₁, u₁} ⥤q V :=
+  {obj := fun _ ↦ v, map := fun _ => α}
+
+/-- Prefunctors out of `⭮` are equal if they point to the same self-arrow. -/
+@[ext (iff := false)]
+lemma Point.prefunctor.ext {V : Type u₂} [Quiver.{v₂} V] {F G : ⭮.{v₁, u₁} ⥤q V}
+    (h_obj : F.obj ⟨⟩ = G.obj ⟨⟩)
+    (h_map : F.map ⟨⟩ = Quiver.homOfEq (G.map ⟨⟩) h_obj.symm h_obj.symm) : F = G := by
+  rcases F with ⟨F_obj, F_map⟩; rcases G with ⟨G_obj, G_map⟩
+  rw [Prefunctor.mk.injEq]
+  constructor
+  · ext ⟨⟩; exact h_obj
+  · apply Function.hfunext rfl
+    rintro ⟨⟩ ⟨⟩ -
+    apply Function.hfunext rfl
+    rintro ⟨⟩ ⟨⟩ -
+    apply Function.hfunext rfl
+    simp only [heq_eq_eq, forall_eq']
+    rintro ⟨⟩
+    simp at h_map
+    simp [h_map, Quiver.homOfEq_heq]
+
+lemma Point.prefunctor.ext_iff {V : Type u₂} [Quiver.{v₂} V] {F G : ⭮.{v₁, u₁} ⥤q V} :
+    F = G ↔ ∃ h_obj : F.obj ⟨⟩ = G.obj ⟨⟩,
+      F.map ⟨⟩ = Quiver.homOfEq (G.map ⟨⟩) h_obj.symm h_obj.symm := by
+  refine ⟨fun h => ?_, fun ⟨h_obj, h_map⟩ => Point.prefunctor.ext h_obj h_map⟩
+  subst h; simp
+
+/-- `Empty` is initial in **`Quiv`**. -/
+def emptyIsInitial : IsInitial (of Empty) :=
+  IsInitial.ofUniqueHom (fun X ↦ Prefunctor.mk PEmpty.elim PEmpty.elim)
+    fun X ⟨obj, map⟩ ↦ by
+      congr
+      · ext ⟨⟩
+      · apply Function.hfunext rfl
+        rintro ⟨⟩
+
+instance : HasInitial Quiv := emptyIsInitial.hasInitial
+
+/-- The initial object in **Quiv** is `Empty`. -/
+noncomputable def initialIsoEmpty : ⊥_ Quiv ≅ of Empty :=
+  initialIsoIsInitial emptyIsInitial
+
+/-- `⭮` is terminal in **Quiv**. -/
+def pointIsTerminal : IsTerminal (of ⭮) :=
+  IsTerminal.ofUniqueHom
+    (fun X ↦ Prefunctor.mk (fun _ ↦ ⟨⟩) (fun _ ↦ ⟨⟩))
+    fun X ⟨obj, map⟩ ↦ by congr
+
+instance : HasTerminal Quiv := pointIsTerminal.hasTerminal
+
+/-- The terminal object in **Quiv** is ⭮. -/
+noncomputable def terminalIsoPoint : ⊤_ Quiv ≅ of ⭮ :=
+  terminalIsoIsTerminal pointIsTerminal
+
+end Quiv
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Category/Quiv/WalkingQuiver.lean b/Mathlib/CategoryTheory/Category/Quiv/WalkingQuiver.lean
new file mode 100644
index 00000000000000..2b321004a2881b
--- /dev/null
+++ b/Mathlib/CategoryTheory/Category/Quiv/WalkingQuiver.lean
@@ -0,0 +1,156 @@
+import Mathlib.CategoryTheory.Category.Quiv
+import Mathlib.Data.Fintype.Basic
+import Mathlib.CategoryTheory.ConcreteCategory.Basic
+
+import Mathlib.Tactic.ApplyFun
+-- import Mathlib.Tactic.finCases
+
+open CategoryTheory
+
+inductive WalkingQuiver where | zero | one deriving Inhabited
+
+-- instance : Fintype WalkingQuiver := Fin.fintype 2
+
+instance : OfNat WalkingQuiver 0 := ⟨WalkingQuiver.zero⟩
+instance : OfNat WalkingQuiver 1 := ⟨WalkingQuiver.one⟩
+
+-- set `0` and `1` as simp normal forms
+@[simp]
+lemma zero_eq : WalkingQuiver.zero = 0 := rfl
+@[simp]
+lemma one_eq : WalkingQuiver.one = 1 := rfl
+
+-- instance : Zero WalkingQuiver := ⟨WalkingQuiver.zero⟩
+-- instance : One WalkingQuiver := ⟨WalkingQuiver.one⟩
+
+-- Delaborators to use `0` and `1` instead of `WalkingQuiver.zero` and `WalkingQuiver.one`
+
+@[delab app.WalkingQuiver.zero]
+def delabWalkingQuiverZero : Lean.PrettyPrinter.Delaborator.Delab := do
+  return ← `(0)
+
+@[delab app.WalkingQuiver.one]
+def delabWalkingQuiverOne : Lean.PrettyPrinter.Delaborator.Delab := do
+  return ← `(1)
+
+
+
+
+inductive WalkingQuiver.Hom : WalkingQuiver → WalkingQuiver → Type
+| id X : WalkingQuiver.Hom X X
+| source : WalkingQuiver.Hom .one .zero
+| target: WalkingQuiver.Hom .one .zero
+
+def WalkingQuiver.forget : WalkingQuiver → Type
+  | .zero => Bool
+  | .one => Unit
+
+instance (X Y : WalkingQuiver) :
+    FunLike (WalkingQuiver.Hom X Y) (WalkingQuiver.forget X) (WalkingQuiver.forget Y) where
+  coe
+  | .id X => id
+  | .source => fun _ => false
+  | .target => fun _ => true
+  coe_injective' X Y f := by
+    cases X <;> cases Y <;> simp_all [funext_iff, WalkingQuiver.forget]
+
+instance : Category WalkingQuiver where
+  Hom := WalkingQuiver.Hom
+  id := WalkingQuiver.Hom.id
+  comp
+    | WalkingQuiver.Hom.id _, g => g
+    | f, WalkingQuiver.Hom.id _ => f
+  id_comp f := by cases f <;> rfl
+  comp_id f := by cases f <;> rfl
+  assoc {W X Y Z} f g h := by
+    cases Z; swap
+    · cases h; cases g; cases f; rfl
+    · cases Y; swap
+      · cases g; cases f; cases h <;> rfl
+      · cases h
+        cases X; swap
+        · cases f; cases g <;> rfl
+        · cases g; cases f <;> rfl
+
+#check instCategoryWalkingQuiver.match_1
+
+instance : ConcreteCategory WalkingQuiver WalkingQuiver.Hom where
+  hom := id
+  ofHom := id
+  comp_apply {X Y Z} f g X' := by
+    simp [instCategoryWalkingQuiver]
+    cases Y
+    · cases X
+      · cases f; simp; rfl
+      · cases Z
+        · cases g; cases f <;> {simp; rfl}
+        · cases g
+    · cases X
+      · cases f
+      · cases f; cases g <;> {simp; rfl}
+
+namespace WalkingQuiver
+
+/-- Convenience recursor for `WalkingQuiver` in terms of the notation `0` and `1`. -/
+@[elab_as_elim, cases_eliminator]
+def casesOn' {motive : WalkingQuiver → Sort*}
+    (m : WalkingQuiver) (zero : motive 0) (one : motive 1) : motive m :=
+  match m with | 0 => zero | 1 => one
+
+@[simp]
+lemma id_def (X : WalkingQuiver) : WalkingQuiver.Hom.id X = 𝟙 X := rfl
+
+@[simp]
+lemma hom₀₁_empty : IsEmpty ((0 : WalkingQuiver) ⟶ 1) := ⟨by rintro ⟨⟩⟩
+
+/-- Any function out of `WalkingQuiver` can be represented as a pair of values for `0` and `1`. -/
+def funByCases {α : WalkingQuiver → Sort*} : ((m : WalkingQuiver) → α m) ≃ (α 0 ×' α 1) :=
+  { toFun := fun f => ⟨f 0, f 1⟩,
+    invFun := fun ⟨f₀, f₁⟩ => fun | 0 => f₀ | 1 => f₁,
+    left_inv := fun f => by ext x; cases x <;> rfl,
+    right_inv := fun ⟨f₀, f₁⟩ => by simp }
+
+
+@[elab_as_elim]
+def casesOn_fun {α : WalkingQuiver → Sort*} {motive : ((m : WalkingQuiver) → α m) → Sort*}
+    (f : (m : WalkingQuiver) → α m) (split : motive (fun | 0 => f 0 | 1 => f 1)) :
+    motive f := by
+  convert split with m; cases m <;> simp
+
+lemma funByCases_eq {α : WalkingQuiver → Sort*} (f : (m : WalkingQuiver) → α m) :
+    f = fun | 0 => f 0 | 1 => f 1 := by
+  ext x; cases x <;> rfl
+
+lemma forall_byCases {p : WalkingQuiver → Prop}  :
+    (∀ m, p m) ↔ p 0 ∧ p 1 where
+  mp h := by simp [h]
+  mpr := fun ⟨h₀, h₁⟩ m ↦ by cases m <;> assumption
+
+@[simp]
+lemma forall₀₀ {p : ((0 : WalkingQuiver) ⟶ 0) → Prop} : (∀ f, p f) ↔ p (𝟙 0) where
+  mp h := h _
+  mpr h := fun f ↦ by cases f; exact h
+
+@[simp]
+lemma forall₁₁ {p : ((1 : WalkingQuiver) ⟶ 1) → Prop} : (∀ f, p f) ↔ p (𝟙 1) where
+  mp h := h _
+  mpr h := fun f ↦ by cases f; exact h
+
+@[simp]
+lemma forall₀₁ {p : ((0 : WalkingQuiver) ⟶ 1) → Prop} : (∀ f, p f) ↔ True where
+  mp _ := trivial
+  mpr _ := nofun
+
+@[simp]
+lemma forall₁₀ {p : ((1 : WalkingQuiver) ⟶ 0) → Prop} : (∀ f, p f) ↔ p .source ∧ p .target where
+  mp h := by simp [h]
+  mpr := fun ⟨h₀, h₁⟩ f ↦ by cases f <;> assumption
+
+@[simp]
+lemma forallHom_byCases {p : {m₁ m₂ : WalkingQuiver} → (m₁ ⟶ m₂) → Prop} :
+    (∀ {m₁ m₂} (f : m₁ ⟶ m₂), p f) ↔ (∀ m, p (𝟙 m)) ∧ p .source ∧ p .target where
+  mp h := by simp [h]
+  mpr := fun ⟨h_id, h_src, h_tgt⟩ m₁ m₂ f ↦ by
+    cases f with
+    | id => cases m₁ <;> simp_all
+    | _ => simp_all
diff --git a/Mathlib/Logic/Small/Defs.lean b/Mathlib/Logic/Small/Defs.lean
index 4b86d17a588d47..66b03ed9489b31 100644
--- a/Mathlib/Logic/Small/Defs.lean
+++ b/Mathlib/Logic/Small/Defs.lean
@@ -46,6 +46,11 @@ def Shrink (α : Type v) [Small.{w} α] : Type w :=
 noncomputable def equivShrink (α : Type v) [Small.{w} α] : α ≃ Shrink α :=
   Nonempty.some (Classical.choose_spec (@Small.equiv_small α _))
 
+/-- Extract the underlying element of a `Shrink` object using projection notation. -/
+@[simp]
+noncomputable def Shrink.out {α : Type v} [Small.{w} α] (x : Shrink α) : α :=
+  (equivShrink α).symm x
+
 @[ext]
 theorem Shrink.ext {α : Type v} [Small.{w} α] {x y : Shrink α}
     (w : (equivShrink _).symm x = (equivShrink _).symm y) : x = y := by