Library CT.Section
Require
Import
CT.Category
.
Section
Given objects \(a, b\) in a category \(C\), a "section" of a \(C\)-morphism \(f : a \to b\) is a right-inverse \(g : b \to a\) such that \(f \circ g = id_b\).
Record
Section
{
C
:
Category
} {
a
b
:
ob
C
} (
f
:
mor
a
b
) :=
{
section
:
mor
b
a
;
section_law
:
comp
section
f
=
id
b
}.