Lean4
/-- The opposite category of `WithInitial C` is equivalent to `WithTerminal Cᵒᵖ`. -/
@[simps!]
def opEquiv : (WithInitial C)ᵒᵖ ≌ WithTerminal Cᵒᵖ
where
functor :=
{ obj := fun ⟨x⟩ ↦
match x with
| of x => .of <| op x
| star => .star
map := fun {x y} ⟨f⟩ ↦
match x, y, f with
| op (of x), op (of y), f => (WithTerminal.down f).op
| op (of _), op star, _ => WithTerminal.starTerminal.from _
| op star, op star, _ => 𝟙 _
map_id := fun ⟨x⟩ ↦ by cases x <;> rfl
map_comp := fun {x y z} ⟨f⟩ ⟨g⟩ ↦
match x, y, z, f, g with
| op (of x), op (of y), op (of z), f, g => rfl
| _, op star, op (of y), f, g => (g : PEmpty).elim
| op star, op (of x), _, f, _ => (f : PEmpty).elim
| _, _, op star, f, g => by subsingleton }
inverse :=
{ obj := fun x ↦
match x with
| .of x => op <| .of <| x.unop
| .star => op .star
map := fun {x y} f ↦
match x, y, f with
| .of (op x), .of (op y), f => WithInitial.down f
| .of (op _), .star, _ => op <| WithInitial.starInitial.to _
| .star, .star, _ => 𝟙 _
map_id := fun x ↦ by cases x <;> rfl
map_comp := fun {x y z} f g ↦
match x, y, z, f, g with
| .of (op x), .of (op y), .of (op z), f, g => rfl
| _, .star, .of (op y), f, g => (g : PEmpty).elim
| .star, .of (op x), _, f, _ => (f : PEmpty).elim
| _, _, .star, f, g => by rfl }
unitIso :=
NatIso.ofComponents
(fun ⟨x⟩ ↦
match x with
| .of x => Iso.refl _
| .star => Iso.refl _)
(fun {x y} f ↦
match x, y, f with
| op (of x), op (of y), f =>
by
simp only [Functor.id_obj, Functor.comp_obj, Functor.id_map, Iso.refl_hom, Category.comp_id, Functor.comp_map,
Category.id_comp]
rfl
| op (of _), op star, _ => rfl
| _, op star, _ => rfl)
counitIso :=
NatIso.ofComponents
(fun x ↦
match x with
| .of x => Iso.refl _
| .star => Iso.refl _)
functor_unitIso_comp := fun ⟨x⟩ ↦
match x with
| .of x =>
by
simp only [op_unop, Functor.id_obj, Functor.comp_obj, NatIso.ofComponents_hom_app, Iso.refl_hom, Category.comp_id]
rfl
| .star => rfl
