English
Set is a LawfulFunctor, i.e., identity and composition laws hold for the map operation: map id = id and map(g ∘ f) = map g ∘ map f.
Русский
Set является законным функтором: выполняются законы идентичности и композиции для отображения map: map id = id и map(g ∘ f) = map g ∘ map f.
LaTeX
$$$\mathrm{map\ id} = \mathrm{id} \land \mathrm{map}(g \circ f) = (\mathrm{map}(g)) \circ (\mathrm{map}(f)).$$$
Lean4
instance : LawfulFunctor Set
where
id_map _ := funext fun _ ↦ propext ⟨fun ⟨_, sb, rfl⟩ ↦ sb, fun sb ↦ ⟨_, sb, rfl⟩⟩
comp_map g h
_ :=
funext <| fun c ↦
propext
⟨fun ⟨a, ⟨h₁, h₂⟩⟩ ↦ ⟨g a, ⟨⟨a, ⟨h₁, rfl⟩⟩, h₂⟩⟩, fun ⟨_, ⟨⟨a, ⟨h₁, h₂⟩⟩, h₃⟩⟩ ↦
⟨a, ⟨h₁, show h (g a) = c from h₂ ▸ h₃⟩⟩⟩
map_const := rfl
