Что такое 3 и чем оно существенно отличается от 5 я пока не знаю.

Ну и Пашину кодировку я не то чтобы вкурил.

Паша эти детали вроде как сам понимает очень хорошо, но извлечь из него информацию затруднительно.

счас скину код!

Ну вот посмотрю, что смогу разобрать.

там только важно, что кодировка дагана использует встроенный фикс. Т.е. это "просто" конструктор алгебраиков, и напрямую с Пашей и Спейтом сравнивать нельзя

listAlg (A : U) : U
   = (X: U)
   * (nil: X)
   * (cons: A -> X -> X)
   * Unit

listMor (A: U) (x1 x2: listAlg A) : U
   = (map: x1.1 -> x2.1)
   * (mapNil: Path x2.1 (map (x1.2.1)) (x2.2.1))
   * (mapCons: (a:A) (x: x1.1) -> Path x2.1 (map (x1.2.2.1 a x)) (x2.2.2.1 a (map x)))
   * Unit

listObject (A: U) : U
   = (point: (x: listAlg A) -> x.1)
   * (map: (x1 x2: listAlg A)
           (m: listMor A x1 x2) ->
           Path x2.1 (m.1 (point x1)) (point x2))
   * Unit

listCategory (A: U) (o: listObject A): U = undefined

ну там не какой-то а "правильный", т.е. наименьший, фикспоинт. "нерекурсивные" кодировки его сразу правильный конструируют, а рекурсивные читят и лепят из "неправильного"

в этом плане даган ценен только тем (имхо) что имея правильный мю позволяет сконструировать всё остальное

record ℝ : Set where
 constructor _,_
 field
   f : ℕ -> ℚ
   reg : {n m : ℕ} -> (∣ (f n) ℚ.- (f m) ∣ ≤ (+ 1 ÷ (suc n))  {fromWitness (λ {i} → 1-coprimeTo (suc n))} ℚ.+ (+ 1 ÷ (suc m))  {fromWitness (λ {i} → 1-coprimeTo (suc m))})

вот его репорт по линейным типам

Вот кстати @akuklev кинул в ЖЖ вброс про Шульмана. Вот его код на Агде HoTT-овских HIR, можно к нам портировать, тем более что групоиды у нас совместимы:

module Universe {i j} {T : Type i} (E : T → Type j) where

 private
   data #U : Type (lmax i j)

   #El : #U → Type j

   data #U where
     #name : (t : T) → #U
     #sig : (A : #U) → (#El A → #U) → #U
     #pi : (A : #U) → (#El A → #U) → #U
     #path : (A : #U) → #El A → #El A → #U

   #El (#name t) = E t
   #El (#sig A B) = Σ (#El A) (λ a → #El (B a))
   #El (#pi A B) = Π (#El A) (λ a → #El (B a))
   #El (#path A a b) = (a == b)

https://github.com/mikeshulman/HoTT-Agda/blob/hiruniv/experimental/HIRUniverse.agda#L77-L93

Так что, типа IR самое компактное встраивание категорной семантики в теорию типов? как инициальный объект, как протокол?

record Glob (i : ULevel) : Type (suc i) where
 coinductive
 constructor glob
 field
   Ob : Type i
   Hom : (a b : Ob) → Glob i
open Glob public

7. Гомотопическая IR Кодировка, инфинити-групоиды https://homotopytypetheory.org/2014/06/08/hiru-tdd/ [Shulman]

Вот, кстати отец IR, Питер Дыбьер: http://www.cse.chalmers.se/~peterd/papers/InductionRecursionInitialAlgebras.pdf

Дыбьер есть в списке обязательного изучения на сайте :-)