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
  }.