Ну, точнее не то чтобы никуда. Никуда без слабой версии высших индуктивных типов под названием Inductive Quotient Types и без пропозициональной и функциональной экстенциональности. Без них вещественный анализ просто превращается в тыкву.

Без унивалентности жить сколько-то можно. Но грустно. Как и без propositional resizing/impredicative PROP.

Ну мне чисто с практической точки зрения интересно как примитив.. Алгебру алгебраических типов наконец можно забацать "внутри"

It may be of interest to some readers to know that CDLE validates axiom K for equality types(Hofmann&Streicher,1998).K,whichisequivalenttouniquenessofidentityproofs, is all one must add to Martin-L¨of Type Theory (MLTT) to support dependent patternmatching, and thus is desirable for practical programming with dependent types (Goguen et al., 2006). But K is incompatible with Homotopy Type Theory (HoTT) (Univalent Foundations Program, 2013), where distinguishing proofs of the same equality is essential to the approach.

короче в Cedille есть UIP

отказать!

Разумеется. Цедиль это зародыш, а не панацея.

Там есть интересная идея, которая меня интересует. Одна.

последний quotient.ctt кстати не чекается, можешь поправить? ;-)

[ (i = 0) -> ? (a = a, b = b, r = r, i = 0), (i = 1) -> ? (a = a, b = b, r = r, i = 1) ]
but expected
[ (i = 0) -> rem3 a, (i = 1) -> rem3 b ]

ща я тут пертурбацию затеял

обнаружил что оказывается у нас есть pi.ctt :)

data setquot (A : U) (R : A -> A -> U) =
   quot (a : A)
 | identification (a b : A) (r : R a b) <i> [ (i = 0) -> quot a, (i = 1) -> quot b ]
 | setTruncation (a b : setquot A R) (p q : Path (setquot A R) a b) <i j>
      [ (i = 0) -> p @ j
      , (i = 1) -> q @ j
      , (j = 0) -> a
      , (j = 1) -> b ]

ну сам мортберг говорит что там зачатки, недоделано и не работает :)

но что-то конечно работает

все работает, кроме test

судя по сему проблемы в тайпчекере

когда <i> Path лямбды в рекурсивных типах (aka HITs)

его ж HIT интересуют как инструмент

"когда топчик". так она сразу в интернете всплывает "Brunerie HoTT". Он же корреспондент блога HTT:

https://homotopytypetheory.org/2012/09/16/truncations-and-truncated-higher-inductive-types/