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

```
infix '=' := Setoid.Ob.Equ
record ListMor: (A: *) -> (x1 x2: ListAlg A) -> * :=
(map: x1.X -> x2.X)
(okNil: Eq (map x1.nil) x2.nil)
(okCons: ∀ (a: A) -> ∀ (x: x1)
-> 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)
(pointOk: ∀ (x1 x2: ListAlg A)
-> ∀ (m: ListMor A x1 x2)
-> Setoid.Ob.Equ (map m 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