Single-object quiver #
Single object quiver with a given arrows type.
Main definitions #
Given a type α
, SingleObj α
is the Unit
type, whose single object is called star α
, with
Quiver
structure such that star α ⟶ star α
is the type α
.
An element x : α
can be reinterpreted as an element of star α ⟶ star α
using
toHom
.
More generally, a list of elements of a
can be reinterpreted as a path from star α
to
itself using pathEquivList
.
Type tag on Unit
used to define single-object quivers.
Instances For
The single object in SingleObj α
.
Instances For
Equip SingleObj α
with a reverse operation.
Instances For
Equip SingleObj α
with an involutive reverse operation.
Instances For
The type of arrows from star α
to itself is equivalent to the original type α
.
Instances For
Prefunctors between two SingleObj
quivers correspond to functions between the corresponding
arrows types.
Instances For
Auxiliary definition for quiver.SingleObj.pathEquivList
.
Converts a path in the quiver single_obj α
into a list of elements of type a
.
Instances For
Auxiliary definition for quiver.SingleObj.pathEquivList
.
Converts a list of elements of type α
into a path in the quiver SingleObj α
.
Equations
- Quiver.SingleObj.listToPath [] = Quiver.Path.nil
- Quiver.SingleObj.listToPath (a :: l) = Quiver.Path.cons (Quiver.SingleObj.listToPath l) a
Instances For
Paths in SingleObj α
quiver correspond to lists of elements of type α
.