# Article

## Initial Object

```
data list (A: U) = nil
| cons (a: A) (xs: list A)
```

## Representing Functor F

`F`_{A} = 1 + A * X

## Construct corresponding F-Algebra

```
record listAlg (A: Type) : Type :=
(X: 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))
```

## Precise Encoding

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

### Unit Parameters

Like for Bool or Nil constructors encoding.

### Fixed Type Parameters

Like for Cons first parameter.

### Recursive Parameters

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

## Identity Functor Encoding

As known as predicative encoding

## Identity Functor Limit Encoding

As known as impredicative encoding