case mp
C : Type u
inst✝ : Category C
⊢ Nonempty (C ≌ Discrete PUnit) → Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

case mpr
C : Type u
inst✝ : Category C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit)
C : Type u
inst✝ : Category C
⊢ Nonempty (C ≌ Discrete PUnit) ↔ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
constructor
case mp.intro
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
case mp
C : Type u
inst✝ : Category C
⊢ Nonempty (C ≌ Discrete PUnit) → Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
rintro ⟨h⟩
case mp.intro
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
⊢ Unique (x ⟶ y)
case mp.intro
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
refine' ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro _⟩
case mp.intro
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
⊢ Unique (x ⟶ y)
case mp.intro
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
⊢ Unique (x ⟶ y)
let f : x ⟶  y := by
  have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert h.unit.app x
  have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert h.unitInv.app y
  exact hx ≫ hy
case mp.intro
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
⊢ Subsingleton (x ⟶ y)
case mp.intro
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
⊢ Unique (x ⟶ y)
suffices sub : Subsingleton (x ⟶  y) from uniqueOfSubsingleton f
case mp.intro.allEq
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
⊢ ∀ (a b : x ⟶ y), a = b
case mp.intro
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
⊢ Subsingleton (x ⟶ y)
apply Subsingleton.intro
case mp.intro.allEq
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ a = b
case mp.intro.allEq
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
⊢ ∀ (a b : x ⟶ y), a = b
intro a b
case mp.intro.allEq
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map a ≫ (Equivalence.unitInv h).app y =
    (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map b ≫ (Equivalence.unitInv h).app y
case mp.intro.allEq
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ a = b
rw [this a, this b]
case mp.intro.allEq
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ (Equivalence.unit h).app x ≫ h.inverse.map (h.functor.map a) ≫ (Equivalence.unitInv h).app y =
    (Equivalence.unit h).app x ≫ h.inverse.map (h.functor.map b) ≫ (Equivalence.unitInv h).app y
case mp.intro.allEq
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map a ≫ (Equivalence.unitInv h).app y =
    (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map b ≫ (Equivalence.unitInv h).app y
simp only [Functor.comp_map]
case mp.intro.allEq.e_a.e_a.e_a
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ h.functor.map a = h.functor.map b
case mp.intro.allEq
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ (Equivalence.unit h).app x ≫ h.inverse.map (h.functor.map a) ≫ (Equivalence.unitInv h).app y =
    (Equivalence.unit h).app x ≫ h.inverse.map (h.functor.map b) ≫ (Equivalence.unitInv h).app y
congr 3
case mp.intro.allEq.e_a.e_a.e_a.h
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ (h.functor.map a).down = (h.functor.map b).down
case mp.intro.allEq.e_a.e_a.e_a
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ h.functor.map a = h.functor.map b
apply ULift.ext
no goals
case mp.intro.allEq.e_a.e_a.e_a.h
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
a b : x ⟶ y
⊢ (h.functor.map a).down = (h.functor.map b).down
simp
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ x ⟶ y
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
⊢ x ⟶ y
have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert h.unit.app x
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
hy : h.inverse.obj { as := PUnit.unit } ⟶ y
⊢ x ⟶ y
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ x ⟶ y
have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert h.unitInv.app y
no goals
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
hy : h.inverse.obj { as := PUnit.unit } ⟶ y
⊢ x ⟶ y
exact hx ≫ hy
no goals
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
⊢ x ⟶ h.inverse.obj { as := PUnit.unit }
convert h.unit.app x
no goals
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ h.inverse.obj { as := PUnit.unit } ⟶ y
convert h.unitInv.app y
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
z : x ⟶ y
⊢ z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
C : Type u
inst✝ : Category C
h : C ≌ Discrete PUnit
x y : C
f : x ⟶ y :=
  let_fun hx :=
    Eq.mpr (_ : (x ⟶ h.inverse.obj { as := PUnit.unit }) = ((𝟭 C).obj x ⟶ (h.functor ⋙ h.inverse).obj x))
      ((Equivalence.unit h).app x);
  let_fun hy :=
    Eq.mpr (_ : (h.inverse.obj { as := PUnit.unit } ⟶ y) = ((h.functor ⋙ h.inverse).obj y ⟶ (𝟭 C).obj y))
      ((Equivalence.unitInv h).app y);
  hx ≫ hy
⊢ ∀ (z : x ⟶ y), z = (Equivalence.unit h).app x ≫ (h.functor ⋙ h.inverse).map z ≫ (Equivalence.unitInv h).app y
intro z
case mpr.intro.intro
C : Type u
inst✝ : Category C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
⊢ Nonempty (C ≌ Discrete PUnit)
case mpr
C : Type u
inst✝ : Category C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit)
rintro ⟨⟨p⟩, h⟩
case mpr.intro.intro
C : Type u
inst✝ : Category C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ Nonempty (C ≌ Discrete PUnit)
case mpr.intro.intro
C : Type u
inst✝ : Category C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
⊢ Nonempty (C ≌ Discrete PUnit)
haveI := fun x y => (h x y).some
case mpr.intro.intro
C : Type u
inst✝ : Category C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ 𝟭 C ≅ (Functor.const C).obj { as := PUnit.unit } ⋙ (Functor.const (Discrete PUnit)).obj p
case mpr.intro.intro
C : Type u
inst✝ : Category C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ Nonempty (C ≌ Discrete PUnit)
refine'
  Nonempty.intro
    (CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩)
      ((@Functor.const <| Discrete PUnit).obj p) ?_ (by apply Functor.pUnitExt))
no goals
case mpr.intro.intro
C : Type u
inst✝ : Category C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ 𝟭 C ≅ (Functor.const C).obj { as := PUnit.unit } ⋙ (Functor.const (Discrete PUnit)).obj p
exact
  NatIso.ofComponents fun _ =>
    { hom := default
      inv := default }
no goals
C : Type u
inst✝ : Category C
h : ∀ (x y : C), Nonempty (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ (Functor.const (Discrete PUnit)).obj p ⋙ (Functor.const C).obj { as := PUnit.unit } ≅ 𝟭 (Discrete PUnit)
apply Functor.pUnitExt