Lean4
/-- The opposite category of `WithTerminal C` is equivalent to `WithInitial Cᵒᵖ`. -/
@[simps!]
def opEquiv : (WithTerminal C)ᵒᵖ ≌ WithInitial 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 star, op (of _), _ => WithInitial.starInitial.to _
| 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 (of y), op star, f, g => (g : PEmpty).elim
| op (of x), op star, _, f, _ => (f : PEmpty).elim
| op star, _, _, f, g => rfl }
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
| .star, .of (op _), _ => op <| WithTerminal.starTerminal.from _
| .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
| _, .of (op y), .star, f, g => (g : PEmpty).elim
| .of (op x), .star, _, f, _ => (f : PEmpty).elim
| .star, _, _, f, g => by subsingleton }
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 star, op (of _), _ => rfl
| op star, 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
