# Lambek Encoding

## Initial Object

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

## Representing Functor F

FA = 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