akuklev: (ДР Цертуса 2011)
[personal profile] akuklev
Предлагается трактовать обозначения [T :> Nat] и [T <: Nat] как [T : NNO] и [T : CoNNO] соответственно, где
@Structure NNO:
  @on N : Type
  zero : N
  succ : N -> N

@Structure CoNNO:
  @on N
  rec[T : NNO](n : N) : T
  rec[:T](zero) = T.zero
  rec[:T](succ(:n)) = T.succ(rec[T](n))


Отметим, что если N1 N2 : NNO ∧ CoNNO, то между типами N1 и N2 имеется изоморфизм, причём каноническим представителем этого класса эквивалентности типов является
@Family Nat:
  zero : Nat
  succ : Nat -> Nat


Для любого индуктивного типа IndT можно автоматически генерировать структуры IND-T и CoIND-T, таким образом проясняя что подразумевается под [T :> IndT] и [T <: IndT]. Наличие таких обозначений позволяет в общем виде описать тип рекурсора для любых индуктивных типов:
IndT.rec[X <: IndT <: Y](x : X) : Y

* * *

В присутствии унивалентности или аксиомы K из обычного рекурсора можно сделать зависимый:
Сперва определим вот такой подтип NNO:
@Structure IndexedNNO:
  @on N : Type
  zero : N
  succ : N -> N
  |(n : N)| : Nat
  |zero| = zero
  |succ(:n)| = succ(|n|)


Разумеется Nat.rec можно примерять и к N : IndexedNNO, более того, для таковых несложно будет показать что lemma1(n : Nat) : |Nat.rec[N](n)| = n. А с другой стороны можно определить
@Structure NatMotive:
  N(n : Nat) -> Type
  zero : N(zero)
  succ(n : Nat) : N(n) -> N(succ(n))


и для любого m : NatMotive снабдить сигма-тип (n : Nat, m.N(n)) структурой inno(m) : IndexedNNO c m.|p| = fst(p), что позволит нам ввести
@def Nat.elim(m : NatMotive, n : Nat): m.N(n)
  apply-path-to-fst(lemma1(n))(Nat.rec[inno(m)](n))


* * *

При всей этой красоте у меня остаются существенные вопросы по семантике.
Если для структуры NNO семантика понятна (NNO-алгебры суть диалгебры для функторов F(N : Type): (Unit, N) и G(N : Type): (N, N)), то со структурой CoNNO семантика мне пока не вполне понятна из-за полифорфности операции rec. Т.е. если зафиксировать конкретную вселенную Type_n, то вполне работает та же диалгебраическая семантика, а если не фиксировать, то вместо одной категории диалгебр у нас будет целое гротендиково расслоение таковых над категорией NNO-алгебр. Аналогичным образом надо бы понять, что такое семантически NNO ∧ CoNNO.

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 20th, 2017 10:37 pm
Powered by Dreamwidth Studios