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
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)
def ⓪ := Cat.mk () def ① := Cat.mk 𝟙ListAlg record Theorem := * (intro: colim ⓪ = lim ①)
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.
Identity Functor Encoding
As known as predicative encoding
Identity Functor Limit Encoding
As known as impredicative encoding
- Om archives.
- Inf archives.
- Git sources.
- Inf git sources.