case mp
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ LocallySmall C → LocallySmall D

case mpr
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ LocallySmall D → LocallySmall C
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ LocallySmall C ↔ LocallySmall D
fconstructor
case mp.mk
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : C), Small (X ⟶ Y)
⊢ LocallySmall D
case mp
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ LocallySmall C → LocallySmall D
rintro ⟨L⟩
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : C), Small (X ⟶ Y)
⊢ autoParam (∀ (X Y : D), Small (X ⟶ Y)) _auto✝
case mp.mk
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : C), Small (X ⟶ Y)
⊢ LocallySmall D
fconstructor
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : C), Small (X ⟶ Y)
X Y : D
⊢ Small (X ⟶ Y)
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : C), Small (X ⟶ Y)
⊢ autoParam (∀ (X Y : D), Small (X ⟶ Y)) _auto✝
intro X Y
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
X Y : D
L : Small (e.inverse.obj X ⟶ e.inverse.obj Y)
⊢ Small (X ⟶ Y)
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : C), Small (X ⟶ Y)
X Y : D
⊢ Small (X ⟶ Y)
specialize L (e.inverse.obj X) (e.inverse.obj Y)
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
X Y : D
L : Small (e.inverse.obj X ⟶ e.inverse.obj Y)
⊢ (X ⟶ Y) ≃ (e.inverse.obj X ⟶ e.inverse.obj Y)
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
X Y : D
L : Small (e.inverse.obj X ⟶ e.inverse.obj Y)
⊢ Small (X ⟶ Y)
refine' (small_congr _).mpr L
no goals
case mp.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
X Y : D
L : Small (e.inverse.obj X ⟶ e.inverse.obj Y)
⊢ (X ⟶ Y) ≃ (e.inverse.obj X ⟶ e.inverse.obj Y)
exact equivOfFullyFaithful e.inverse
case mpr.mk
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : D), Small (X ⟶ Y)
⊢ LocallySmall C
case mpr
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
⊢ LocallySmall D → LocallySmall C
rintro ⟨L⟩
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : D), Small (X ⟶ Y)
⊢ autoParam (∀ (X Y : C), Small (X ⟶ Y)) _auto✝
case mpr.mk
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : D), Small (X ⟶ Y)
⊢ LocallySmall C
fconstructor
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : D), Small (X ⟶ Y)
X Y : C
⊢ Small (X ⟶ Y)
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : D), Small (X ⟶ Y)
⊢ autoParam (∀ (X Y : C), Small (X ⟶ Y)) _auto✝
intro X Y
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
X Y : C
L : Small (e.functor.obj X ⟶ e.functor.obj Y)
⊢ Small (X ⟶ Y)
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
L : ∀ (X Y : D), Small (X ⟶ Y)
X Y : C
⊢ Small (X ⟶ Y)
specialize L (e.functor.obj X) (e.functor.obj Y)
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
X Y : C
L : Small (e.functor.obj X ⟶ e.functor.obj Y)
⊢ (X ⟶ Y) ≃ (e.functor.obj X ⟶ e.functor.obj Y)
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
X Y : C
L : Small (e.functor.obj X ⟶ e.functor.obj Y)
⊢ Small (X ⟶ Y)
refine' (small_congr _).mpr L
no goals
case mpr.mk.hom_small
C✝ : Type u
inst✝² : Category C✝
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
e : C ≌ D
X Y : C
L : Small (e.functor.obj X ⟶ e.functor.obj Y)
⊢ (X ⟶ Y) ≃ (e.functor.obj X ⟶ e.functor.obj Y)
exact equivOfFullyFaithful e.functor