## Initial Object

```
let I = data List (A:*) :=
nil: () -> List A
cons: A -> List A -> List A
```

## Representing Functor F

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

## Construct corresponding F-Algebra

```
record ListAlg (A: *) :=
X: *
nil: () -> X
cons: A -> X -> X
```

## Introduce List Morphisms

```
record ListMor (A: *) (x1 x2: ListAlg A) :=
map: x1.X -> x2.X
mapNil: Setoid.Mor.Eq (map x1.nil) x2.nil
mapCons: (a: A) (x: x1.X) ->
map x1.cons a x = x2.cons a (map x)
```

## Introduce connected points of List type

```
record ListPoint (A: *) :=
point: (x: ListAlg A) -> x.X
transport: (x1 x2: ListAlg A) (m: ListMor A x1 x2) ->
Setoid.Ob.Equ (m.map point x1) (point x2)
```

## Theorem

```
def ⓪ := Cat.mk ()
def ① := Cat.mk 𝟙
```_{ListAlg}
record Theorem := *
(intro: colim ⓪ = lim ①)

## 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