record listAlg (A: Type) : Type :=
(nil: Unit -> X)
(cons: A -> X -> X)
Introduce List Morphisms
record listMor (A: Type) (x1,x2: ListAlg A) : Type :=
(map: x1.X -> x2.X)
(mapNil: Path x2.X (map (x1.nil unit)) (x2.nil unit))
(mapCons: ∀ (a: A) -> ∀ (x: x1) ->
Path x2.X (map (x1.cons a x)) (x2.cons a (map x)))
Introduce connected points of List type
record listPoint (A: Type) : Type :=
(point: ∀ (x: ListAlg A) -> x.X)
(map: ∀ (x1,x2: listAlg A) -> (m: ListMor A x1 x2) ->
Path x2.X (m.map (point x1)) (point x2))
Our encoding allows you to precise control the type of encoded parameter.
There is only three cases and three equations: 1) for unit; 2) particular functorial
type over a parameter type and 3) recursive embedding such as in Cons constructor.
q — is a limit in Dialg P category. The constructor body is calculated
with q applied to forgetful functor U.
Like for Bool or Nil constructors encoding.
Fixed Type Parameters
Like for Cons first parameter.
Like for Cons second parameter. This case is a key in encoding recursive
data types such as Lists and recursive record types such as Streams.