Refinement rules

Booleans

bool/eqtype

H >> bool = bool in (U #l #k)

bool/eq/tt

H >> tt = tt in bool

bool/eq/ff

H >> ff = ff in bool

bool/eq/if

H >> (if [x] (#c0 x) #m0 #t0 #f0) = (if [x] (#c1 x) #m1 #t1 #f1) in #ty
where H >> #m0 = #m1 synth ~> bool, psi
| H >> #t0 = #t1 in (#c0 tt)
| H >> #f0 = #f1 in (#c0 ff)
| H, x:bool >> (#c0 x) = (#c1 x) type
| psi
| H >> (#c0 #m0) <= #ty type

Natural numbers and integers

nat/eqtype

H >> nat = nat in (U #l #k)

nat/eq/zero

H >> (nat 0) = (nat 0) in nat

nat/eq/succ

H >> (succ #n) = (succ #m) in nat
| H >> #n = #m in nat

nat/eq/nat-rec

H >> (nat-rec [x] (#c0 x) #m0 #n0 [a b] (#p0 a b)) = (nat-rec [x] (#c1 x) #m1 #n1 [a b] (#p1 a b)) in #ty
| H >> #m0 = #m1 in nat
| H >> #n0 = #n1 in (#c0 (nat 0))
| H, a:nat, b:(#c0 a) >> #p0 a b = #p1 a b in (#c0 (succ a))
| H, x:nat >> (#c0 x) = (#c1 x) type
| H >> (#c0 #m0) <= #ty type

int/eqtype

H >> int = int in (U #l #k)

int/eq/pos

H >> (pos #m) = (pos #n) in int
| H >> #m = #n in nat

int/eq/negsucc

H >> (negsucc #m) = (negsucc #n) in int
| H >> #m = #n in nat

int/eq/int-rec

H >> (int-rec [x] (#e0 x) #m0 [a] (#n0 a) [b] (#p0 b)) = (int-rec [x] (#e1 x) #m1 [a] (#n1 a) [b] (#p1 b)) in #ty
| H >> #m0 = #m1 in int
| H, b:nat >> (#p0 b) = (#p1 b) in #e0 (pos b)
| H, a:nat >> (#n0 a) = (#n1 a) in #e0 (negsucc a)
| H, x:int >> (#e0 x) = (#e1 x) type
| H >> (#e0 m0) <= #ty type

Void

void/eqtype

H >> void = void in (U #l #k)

Circle

s1/eqtype

H >> S1 = S1 in (U #l #k)
where kan <= #k universe

s1/eq/base

H >> base = base in S1

s1/eq/loop

H >> loop #r = loop #r in S1

s1/eq/fcom

H >> (fcom #i~>#j #cap0 [#r/0=#s/0 [k] (#t0/0 k)] ... [#r/n=#s/n [k] (#t0/n k)])
     = (fcom #i~>#j #cap1 [#r/0=#s/0 [k] (#t1/0 k)] ... [#r/n=#s/n [k] (#t1/n k)]) in S1
| H >> #cap0 = #cap1 in S1
| H, k:dim, #r/0=#s/0 >> (#t0/0 k) = (#t1/0 k) in S1
| ...
| H, k:dim, #r/n=#s/n >> (#t0/n k) = (#t1/n k) in S1
| H, k:dim, #r/0=#s/0, #r/1=#s/1 >> (#t0/0 k) = (#t1/1 k) in S1
| H, k:dim, #r/0=#s/0, #r/2=#s/2 >> (#t0/0 k) = (#t1/2 k) in S1
| ...
| H, k:dim, #r/n-1=#s/n-1, #r/n=#s/n >> (#t0/n-1 k) = (#t1/n k) in S1
| H, #r/0=#s/0 >> #cap0 = (#t0/0 #i) in S1
| ...
| H, #r/n=#s/n >> #cap0 = (#t0/n #i) in S1

s1/eq/s1-rec

H >> (S1-rec [x] (#c0 x) #m0 #b0 [u] #l0) = (S1-rec [x] (#c1 x) #m1 #b1 [u] #l1) in #ty
| H >> #m0 = #m1 in S1
| H >> #b0 = #b1 in (#c0 base)
| H, u:dim >> (#l0 u) = (#l1 u) in (#c0 (loop u))
| H >> (#l0 0) = #b0 in (#c0 base)
| H >> (#l0 1) = #b0 in (#c0 base)
| H, x:S1 >> (#c0 x) = (#c1 x) kan type
| H >> (#c0 #m0) <= #ty type

s1/beta/loop

H >> (S1-rec [x] (#c x) (loop #r) #b [u] (#l u)) = #m in #ty
| H >> (#l #r) = #m in #ty
| H, #r=0 >> #b = #m in #ty
| H, #r=1 >> #b = #m in #ty

Dependent functions

fun/eqtype

H >> (-> [x : #a0] (#b0 x)) = (-> [x : #a1] (#b1 x)) in (U #l #k)
where
  (#k/dom, #k/cod) <-
    (discrete, discrete) if #k == discrete
    (coe, kan) if #k == kan
    (pre, hcom) if #k == hcom
    (coe, coe) if #k == coe
    (pre, pre) if #k == pre
| H >> #a0 = #a1 in (U #l #k/dom)
| H, x:#a0 >> (#b0 x) = (#b1 x) in (U #l #k/cod)

fun/eq/lam

H >> (lam [x] (#e0 x)) = (lam [x] (#e1 x)) in (-> [x : #a] (#b x))
| H, x:#a >> (#e0 x) = (#e1 x) in (#b x)
| H >> #a type

fun/intro

H >> (-> [x : #a] (#b x)) ext (lam [x] (#e x))
| H, x:#a >> (#b x) ext (#e x)
| H >> #a type

fun/eq/eta

H >> #e = #f in (-> [x : #a] (#b x))
| H >> (lam [x] ($ #e x)) = #f in (-> [x : #a] (#b x))
| H >> #e = #e in (-> [x : #a] (#b x))

fun/eq/app

H >> ($ #f0 #e0) = ($ #f1 #e1) in #ty
where H >> #f0 = #f1 synth ~> (-> [x : #a] (#b x)), psi
| H >> #e0 = #e1 in #a
| psi
| H >> (#cod #e0) <= #ty type

Records

record/eqtype

H >> (record [lbl/a : #a0] ... [lbl/b : (#b0 lbl/a ...)])
     = (record [lbl/a : #a1] ... [lbl/b : (#b1 lbl/a ...)])
     in (U #l #k)
where
  (#k/hd, #kltl) <-
    (discrete, discrete) if #k == discrete
    (kan, kan) if #k == kan
    (hcom, kan) if #k == hcom
    (coe, coe) if #k == coe
    (pre, pre) if #k == pre
| H >> #a0 = #a1 in (U #l #k/hd)
| ...
| H, x : #a0, ... >> (#b0 x ...) = (#b1 x ...) in (U #l #k/tl)

Todo

The choice of kinds #k/hd and #k/tl looks a little fishy; is this exactly what would be generated if a record were encoded as an iterated sigma type?

record/eq/tuple

H >> (tuple [lbl/a #p0] ... [lbl/b #q0])
     = (tuple [lbl/a #p1] ... [lbl/b #q1])
     in (record [lbl/a : #a] ... [lbl/b : (#b lbl/a ...)])
| H >> #p0 = #p1 in #a
| ...
| H >> #q0 = #q1 in (#b #p0 ...)
| ...
| H, x:#a, ... >> (#b x ...) type

record/eq/eta

H >> #e0 = #e1 in (record [lbl/a : #a] ... [lbl/b : (#b lbl/a ...)])
| H >> (tuple [lbl/a (! lbl/a #e0)] ... [lbl/b (! lbl/b #e0)])
|      = #e1 in (record [lbl/a : #a] ... [lbl/b : (#b lbl/a ...)])
| H >> #e0 in (record [lbl/a : #a] ... [lbl/b : (#b lbl/a ...)])

record/eq/proj

H >> (! lbl #e0) = (! lbl #e1) in #ty
where H >> #e0 = #e1 synth ~> (record [lbl0 : #a0] ... [lbl : (#a ...)] ...), psi
| psi
| H >> (#a (! lbl0  #e0) ...) <= #ty type

record/intro

H >> (record [lbl/a : #a] ... [lbl/b : (#b lbl/a ...)])
     ext (tuple [lbl/a #p/a] ... [lbl/b #p/b])
| H >> #a ext #p/a
| ...
| H >> (#b #p/a ...) ext #p/b
| ...
| H, x:#a, ... >> (#b x ...) type

Paths

path/eqtype

H >> (path [u] (#a0 u) #m0 #n0) = (path [u] (#a1 u) #m1 #n1) in (U #l #k)
where
  #ka <-
    discrete if #k == discrete
    kan if #k == kan
    hcom if #k == hcom
    kan if #k == coe
    pre if #k == pre
| H, u:dim >> (#a0 u) = (#a1 u) in (U #l #ka)
| H >> #m0 = #m1 in (#a0 0)
| H >> #n0 = #n1 in (#a0 1)

path/eq/abs

H >> (abs [v] (#m0 v)) = (abs [v] (#m1 v)) in (path [v] (#a v) #p0 #p1)
| H, v:dim >> #m0 v = #m1 v in (#a v)
| H >> (#m0 0) = #p0 in (#a 0)
| H >> (#m0 1) = #p1 in (#a 1)

path/intro

H >> (path [u] (#a u) #p0 #p1) ext (abs [u] (#m u))
| H, u:dim >> (#a u) ext (#m u)
| H >> (#m 0) = #p0 in (#a 0)
| H >> (#m 1) = #p1 in (#a 1)

path/eq/eta

H >> #m = #n in (path [u] (#a u) #p0 #p1)
| H >> (abs [u] (#m u)) = #n in (path [u] (#a u) #p0 #p1)
| H >> #m = #m in (path [u] (#a u) #p0 #p1)

path/eq/app

H >> (@ #m0 #r) = (@ #m1 #r) in #ty
where H >> #m0 = #m1 synth ~> (path [u] (#a u) #p0 #p1), psi
| psi
| H >> (#a #r) = #ty type

path/eq/app/const

H >> (@ #m #r) = #p in #a
where
  H >> #m = #m synth ~> (path [x] (#ty x) #p0 #p1), psi
  #pr <-
    #p0 if #r == 0
    #p1 if #r == 1
| H >> #pr = #p in #a
| psi
| H >> #ty #r <= #a type

path/eq/from-line

H >> #m0 = #m1 in (path [x] (#ty x) #n0 #n1)
| H >> #m0 = #m1 in (line [x] (#ty x))
| H >> #n0 = (@ #m0 0) in (#ty 0)
| H >> #n1 = (@ #m1 1) in (#ty 1)

Lines

line/eqtype

H >> (line [u] (#a0 u)) = (line [u] (#a1 u)) in (U #l #k)
where
  #ka <-
    discrete if #k == discrete
    kan if #k == kan
    hcom if #k == hcom
    kan if #k == coe
    pre if #k == pre
| H, u:dim >> (#a0 u) = (#a1 u) in (U #l #ka)

line/eq/abs

H >> (abs [u] (#m0 u)) = (abs [u] (#m1 u)) in (line [u] (#a u))
| H, u:dim >> #m0 u = #m1 u in (#a u)

line/intro

H >> (line [u] (#a u)) ext (abs [u] (#m u))
| H, u:dim >> (#a u) ext (#m u)

line/eq/eta

H >> #m = #n in (line [u] (#a u))
| H >> #m in (line [u] (#a u))
| H >> (abs [u] (@ m u)) = #n in (line [u] (#a u))

line/eq/app

H >> (@ #m0 #r) = (@ #m0 #r) in #ty
where H >> #m0 = #m1 synth ~> (line [u] (#a u)), psi
| psi
| H >> (#a #r) <= #ty type

Pushouts

pushout/eqtype

H >> (pushout #a0 #b0 #c0 [x] (#f0 x) [x] (#g0 x)) = (pushout #a1 #b1 #c1 [x] (#f1 x) [x] (#g1 x)) in (U #l #k)
where
  (#k/end, #k/apex) <-
    (coe, coe) if #k == kan
    (coe, coe) if #k == coe
    (pre, pre) if #k == hcom
    (pre, pre) if #k == pre
| H, x:#c0 >> (#f0 x) = (#f1 x) in #a0
| H, x:#c0 >> (#g0 x) = (#g1 x) in #b0
| H >> #a0 = #a1 in (U #l #k/end)
| H >> #b0 = #b1 in (U #l #k/end)
| H >> #c0 = #c1 in (U #l #k/apex)

pushout/eq/left

H >> (left #m0) = (left #m1) in (pushout #a #b #c [x] (#f x) [x] (#g x))
| H >> #m0 = #m1 in #a
| H, x:#c >> (#f x) in #a
| H, x:#c >> (#g x) in #b
| H >> #b type
| H >> #c type

pushout/eq/right

H >> (right #m0) = (right #m1) in (pushout #a #b #c [x] (#f x) [x] (#g x))
| H >> #m0 = #m1 in #b
| H, x:#c >> (#f x) in #a
| H, x:#c >> (#g x) in #b
| H >> #a type
| H >> #c type

pushout/eq/glue

H >> (glue #r #m0 #fm0 #gm0) = (glue #r #m1 #fm1 #gm1) in (pushout #a #b #c [x] (#f x) [x] (#g x))
| H >> #m0 = #m1 in #c
| H >> #fm0 = #fm1 in #a
| H >> #gm0 = #gm1 in #b
| H >> (#f #m0) = #fm0 in #a
| H >> (#g #m0) = #gm0 in #b
| H, x:#c >> (#f x) in #a
| H, x:#c >> (#g x) in #b

pushout/eq/fcom

H >> (fcom #i~>#j #cap0 [#r/0=#s/0 [k] (#t0/0 k)] ... [#r/n=#s/n [k] (#t0/n k)])
     = (fcom #i~>#j #cap1 [#r/0=#s/0 [k] (#t1/0 k)] ... [#r/n=#s/n [k] (#t1/n k)])
     in (pushout #a #b #c [x] (#f x) [x] (#g x))
where
  #ty <- (pushout #a #b #c [x] (#f x) [x] (#g x))
| H, x:#c >> (#f x) in #a
| H, x:#c >> (#g x) in #b
| H >> #a type
| H >> #b type
| H >> #c type
| H >> #cap0 = #cap1 in #ty
| H, k:dim, #r/0=#s/0 >> (#t0/0 k) = (#t1/0 k) in #ty
| ...
| H, k:dim, #r/n=#s/n >> (#t0/n k) = (#t1/n k) in #ty
| H, k:dim, #r/0=#s/0, #r/1=#s/1 >> (#t0/0 k) = (#t1/1 k) in #ty
| H, k:dim, #r/0=#s/0, #r/2=#s/2 >> (#t0/0 k) = (#t1/2 k) in #ty
| ...
| H, k:dim, #r/n-1=#s/n-1, #r/n=#s/n >> (#t0/n-1 k) = (#t1/n k) in #ty
| H, #r/0=#s/0 >> #cap0 = (#t0/0 #i) in #ty
| ...
| H, #r/n=#s/n >> #cap0 = (#t0/n #i) in #ty

pushout/eq/pushout-rec

H >> (pushout-rec [p] (#d0 p) #m0 [a] (#n0 a) [b] (#p0 b) [v x] (#q0 v x))
     = (pushout-rec [x] (#d1 x) #m1 [a] (#n1 a) [b] (#p1 b) [v x] (#q1 v x)) in #ty
where H >> #m0 = #m1 synth ~> (pushout #a #b #c [x] (#f x) [x] (#g x)), psi
| H, a:#a >> (#n0 a) = (#n1 a) in (#d0 (left a))
| H, b:#b >> (#p0 b) = (#p1 b) in (#d1 (right b))
| H, v:dim, x:#c >> (#q0 v x) = (#q1 v x) in (#d0 (glue v x (#f x) (#g x)))
| H, x:#c >> (#q0 0 x) = (#n0 (#f x)) in (#d0 (left (#f x)))
| H, x:#c >> (#q0 1 x) = (#p0 (#g x)) in (#d0 (right (#g x)))
| H, p:(pushout #a #b #c [x] (#f x) [x] (#g x)) >> (#d0 p) = (#d1 p) kan type
| psi
| H >> (#d0 #m0) <= #ty type

pushout/beta/glue

H >> (pushout-rec [p] (#d p) (glue #r #t #ft #gt) [a] (#n a) [b] (#p b) [v x] (#q v x)) = #s in #ty
| H >> (#q #r #t) = #s in #ty
| H, #r=0 >> (#n #ft) = #s in #ty
| H, #r=1 >> (#p #gt) = #s in #ty

Coequalizers

coeq/eqtype

H >> (coeq #a0 #b0 [x] (#f0 x) [x] (#g0 x)) = (coeq #a1 #b1 [x] (#f1 x) [x] (#g1 x)) in (U #l #k)
where
  (#k/cod, #k/dom) <-
    (coe, coe) if #k == kan
    (coe, coe) if #k == coe
    (pre, pre) if #k == hcom
    (pre, pre) if #k == pre
| H, x:#a0 >> (#f0 x) = (#f1 x) in #b0
| H, x:#a0 >> (#g0 x) = (#g1 x) in #b0
| H >> #a0 = #a1 in (U #l #k/dom)
| H >> #b0 = #b1 in (U #l #k/cod)

coeq/eq/cod

H >> (cecod #m0) = (cecod #m1) in (coeq #a #b [x] (#f x) [x] (#g x))
| H >> #m0 = #m1 in #b
| H, x:#a >> (#f x) in #b
| H, x:#a >> (#g x) in #b
| H >> #a type

coeq/eq/dom

H >> (cedom #r #m0 #fm0 #gm0) = (cedom #r #m0 #fm0 #gm0) in (coeq #a #b [x] (#f x) [x] (#g x))
| H >> #m0 = #m1 in #a
| H >> #fm0 = #fm1 in #b
| H >> #gm0 = #gm1 in #b
| H >> (#f #m0) = #fm0 in #b
| H >> (#g #m0) = #gm0 in #b
| H, x:#a >> (#f x) in #b
| H, x:#a >> (#g x) in #b

coeq/eq/fcom

H >> (fcom #i~>#j #cap0 [#r/0=#s/0 [k] (#t0/0 k)] ... [#r/n=#s/n [k] (#t0/n k)])
     = (fcom #i~>#j #cap1 [#r/0=#s/0 [k] (#t1/0 k)] ... [#r/n=#s/n [k] (#t1/n k)])
     in (coeq #a #b [x] (#f x) [x] [x] (#g x))
where
  #ty <- (coeq #a #b [x] (#f x) [x] [x] (#g x))
| H, x:#a >> (#f x) in #b
| H, x:#a >> (#g x) in #b
| H >> #a type
| H >> #b type
| H >> #cap0 = #cap1 in #ty
| H, k:dim, #r/0=#s/0 >> (#t0/0 k) = (#t1/0 k) in #ty
| ...
| H, k:dim, #r/n=#s/n >> (#t0/n k) = (#t1/n k) in #ty
| H, k:dim, #r/0=#s/0, #r/1=#s/1 >> (#t0/0 k) = (#t1/1 k) in #ty
| H, k:dim, #r/0=#s/0, #r/2=#s/2 >> (#t0/0 k) = (#t1/2 k) in #ty
| ...
| H, k:dim, #r/n-1=#s/n-1, #r/n=#s/n >> (#t0/n-1 k) = (#t1/n k) in #ty
| H, #r/0=#s/0 >> #cap0 = (#t0/0 #i) in #ty
| ...
| H, #r/n=#s/n >> #cap0 = (#t0/n #i) in #ty

coeq/beta/dom

H >> (coeq-rec [c] (#p c) (cedom #r #t #ft #gt) [b] (#n b) [v a] (#q v a)) = #s in #ty
| H >> (#q #r #t) = #s in #ty
| H, #r=0 >> (#n #ft) = #s in #ty
| H, #r=1 >> (#n #gt) = #s in #ty

coeq/eq/coeq-rec

H >> (coeq-rec [c] (#p0 c) #m0 [b] (#n0 b) [v a] (#q0 v a))
     = (coeq-rec [c] (#p1 c) #m1 [b] (#n1 b) [v a] (#q1 v a)) in #ty
where H >> #m0 = #m1 synth (coeq #a #b [x] (#f x) [x] (#g x)), psi
| H, b:#b >> (#n0 b) = (#n1 b) in (#p0 (cecod b))
| H, v:dim, a:#a >> (#q0 v a) = (#q1 v a) in (#p0 (cedom v a (#f a) (#g a))
| H, a:#a >> (#q0 0 a) = (#n0 (#f a)) in (#p0 (cecod (#f a)))
| H, a:#a >> (#q0 1 a) = (#n0 (#g a)) in (#p0 (cecod (#g a)))
| H, c:(coeq #a #b [x] (#f x) [x] (#g x)) >> (#p0 c) = (#p1 c) kan type
| psi
| H >> (#p0 #m0) <= #ty type

Exact equalities

eq/eqtype

H >> (= #a0 #m0 #n0) = (= #a1 #m1 #n1) in (U #l #k)
where
  #ka <-
    discrete if #k == discrete
    discrete if #k == kan
    pre if #k == hcom
    discrete if #k == coe
    pre if #k == pre
| H >> #m0 = #m1 in #a0
| H >> #n0 = #n1 in #a0
| H >> #a0 = #a1 in (U #l #ka)

eq/eq/ax

H >> ax = ax in (= #a #m #n)
| H >> #m = #n in #a

eq/eta

H >> #x = #y in (= #a #m #n)
| H >> ax = #y in (= #a #m #n)
| H >> #x in (= #a #m #n)

Composite types

fcom/eqtype

H >> (fcom #i~>#j #Cap0 [#r/0=#s/0 [k] (#T0/0 k)] ... [#r/n=#s/n [k] (#T0/n k)])
     = (fcom #i~>#j #Cap1 [#r/0=#s/0 [k] (#T1/0 k)] ... [#r/n=#s/n [k] (#T1/n k)])
     in (U #l #k)
where
  (#k/cap, #k/tube) <-
    (kan, kan) if #k == kan
    (hcom, kan) if #k == hcom
    (kan, kan) if #k == coe
    (pre, coe) if #k == pre
| H >> #Cap0 = #Cap1 in (U #l #k/cap)
| H, k:dim, #r/0=#s/0 >> (#T0/0 k) = (#T1/0 k) in (U #l #k/tube)
| ...
| H, k:dim, #r/n=#s/n >> (#T0/n k) = (#T1/n k) in (U #l #k/tube)
| H, k:dim, #r/0=#s/0, #r/1=#s/1 >> (#T0/0 k) = (#T1/1 k) in (U #l #k/tube)
| H, k:dim, #r/0=#s/0, #r/2=#s/2 >> (#T0/0 k) = (#T1/2 k) in (U #l #k/tube)
| ...
| H, k:dim, #r/n-1=#s/n-1, #r/n=#s/n >> (#T0/n-1 k) = (#T1/n k) in (U #l #k/tube)
| H, #r/0=#s/0 >> #Cap0 = (#T0/0 #i) in (U #l #k/cap)
| ...
| H, #r/n=#s/n >> #Cap0 = (#T0/n #i) in (U #l #k/cap)

fcom/eq/box

H >> (box #i~>#j #cap0 [#r/0=#s/0 #b0/0] ... [#r/n=#s/n #b0/n])
     = (box #i~>#j #cap1 [#r/0=#s/0 #b1/0] ... [#r/n=#s/n #b1/n])
     in (fcom #i~>#j #Cap [#r/0=#s/0 [k] (#T/0 k)] ... [#r/n=#s/n [k] (#T/n k)])
| H >> #cap0 = #cap1 in #Cap
| H, #r/0=#s/0 >> #b0/0 = #b1/0 in (#T/0 #j)
| ...
| H, #r/n=#s/n >> #b0/n = #b1/n in (#T/n #j)
| H, #r/0=#s/0, #r/1=#s/1 >> #b0/0 = #b1/1 in (#T/0 #j)
| H, #r/0=#s/0, #r/2=#s/2 >> #b0/0 = #b1/2 in (#T/0 #j)
| ...
| H, #r/n-1=#s/n-1, #r/n=#s/n >> #b0/n-1 = #b1/n in (#T/n-1 #j)
| H, #r/0=#s/0 >> #cap0 = (coe #j~>#i #T/0 #b0/0) in #Cap
| ...
| H, #r/n=#s/n >> #cap0 = (coe #j~>#i #T/n #b0/n) in #Cap
| H, k:dim, #r/0=#s/0 >> (#T/0 k) coe type
| ...
| H, k:dim, #r/n=#s/n >> (#T/n k) coe type
| H, k:dim, #r/0=#s/0, #r/1=#s/1 >> (#T/0 k) = (#T/1 k) coe type
| H, k:dim, #r/0=#s/0, #r/2=#s/2 >> (#T/0 k) = (#T/2 k) coe type
| ...
| H, k:dim, #r/n-1=#s/n-1, #r/n=#s/n >> (#T/n-1 k) = (#T/n k) coe type
| H, #r/0=#s/0 >> #Cap = (#T/0 #i) type
| ...
| H, #r/n=#s/n >> #Cap = (#T/n #i) type

fcom/intro

H >> (fcom #i~>#j #Cap [#r/0=#s/0 [k] (#T/0 k)] ... [#r/n=#s/n [k] (#T/n k)])
     ext (box #i~>#j #cap [#r/0=#s/0 #b/0] ... [#r/n=#s/n #b/n])
| H >> #Cap ext #cap
| H, #r/0=#s/0 >> (#T/0 #j) ext #b/0
| ...
| H, #r/n=#s/n >> (#T/n #j) ext #b/n
| H, #r/0=#s/0, #r/1=#s/1 >> #b/0 = #b/1 in (#T/0 #j)
| H, #r/0=#s/0, #r/2=#s/2 >> #b/0 = #b/2 in (#T/0 #j)
| ...
| H, #r/n-1=#s/n-1, #r/n=#s/n >> #b/n-1 = #b/n in (#T/n-1 #j)
| H, #r/0=#s/0 >> #cap = (coe #j~>#i #T/0 #b/0) in #Cap
| ...
| H, #r/n=#s/n >> #cap = (coe #j~>#i #T/n #b/n) in #Cap
| H, k:dim, #r/0=#s/0 >> (#T/0 k) coe type
| ...
| H, k:dim, #r/n=#s/n >> (#T/n k) coe type
| H, k:dim, #r/0=#s/0, #r/1=#s/1 >> (#T/0 k) = (#T/1 k) coe type
| H, k:dim, #r/0=#s/0, #r/2=#s/2 >> (#T/0 k) = (#T/2 k) coe type
| ...
| H, k:dim, #r/n-1=#s/n-1, #r/n=#s/n >> (#T/n-1 k) = (#T/n k) coe type
| H, #r/0=#s/0 >> #Cap = (#T/0 #i) type
| ...
| H, #r/n=#s/n >> #Cap = (#T/n #i) type

V types

v/eqtype

H >> (V #r #a0 #b0 #e0) = (V #r #a1 #b1 #e1) in (U #l #k)
where
  (#ka, #kb) <-
    (kan, kan) if #k == kan
    (hcom, hcom) if #k == hcom
    (coe, com) if #k == coe
    (pre, pre) if #k == pre
| H, #r=0 >> #e0 = #e1 in (Equiv #a0 #b0)
| H, #r=0 >> #a0 = #a1 in (U #l #ka)
| H >> #b0 = #b1 in (U #l #kb)

where Equiv is defined by

define HasAllPathsTo (#C,#c) = (-> [center : #C] (path [_] #C center #c)).
define IsContr (#C) = (* [c : #C] (HasAllPathsTo #C c)).
define Fiber (#A,#B,#f,#b) = (* [a : #A] (path [_] #B ($ #f a) #b)).
define IsEquiv (#A,#B,#f) = (-> [b : #B] (IsContr (Fiber #A #B #f b))).
define Equiv (#A,#B) = (* [f : (-> #A #B)] (IsEquiv #A #B f)).

v/eq/vin

H >> (vin #r #m0 #n0) = (vin #r #m1 #n1) in (V #r #a #b #e)
| H, #r=0 >> #m0 = #m1 in #a
| H >> #n0 = #n1 in #b
| H, #r=0 >> ($ (! proj1 #e) #m0) = #n0 in #b
| H, #r=0 >> #e in (Equiv #a #b)

v/intro

H >> (V #r #a #b #e) ext (vin #r #m #n)
| H, #r=0 >> #a ext #m
| H >> #b ext #n
| H, #r=0 >> ($ (! proj1 #e) #m) = #n in #b
| H, #r=0 >> #e in (Equiv #a #b)

v/eq/proj

H >> (vproj #r #m0 #f0) = (vproj #r #m1 #f1) in #ty
where
  #r /= 0 and #r /= 1
  H >> #m0 = #m1 synth ~> (v #r #a #b #e), psi
| H, #r=0 >> #f0 = #f1 in (-> #a #b)
| H, #r=0 >> #f0 = (! proj1 #e) in (-> #a #b)
| psi
| H >> #b <= #ty type

Kan operations

hcom/eq

H >> (hcom #i~>#j #ty0 #cap0 [#r/0=#s/0 [k] (#t0/0 k)] ... [#r/n=#s/n [k] (#t0/n k)])
     = (hcom #i~>#j #ty1 #cap1 [#r/0=#s/0 [k] (#t1/0 k)] ... [#r/n=#s/n [k] (#t1/n k)]) in #ty
| H >> #cap0 = #cap1 in #ty0
| H, k:dim, #r/0=#s/0 >> (#t0/0 k) = (#t1/0 k) in #ty0
| ...
| H, k:dim, #r/n=#s/n >> (#t0/n k) = (#t1/n k) in #ty0
| H, k:dim, #r/0=#s/0, #r/1=#s/1 >> (#t0/0 k) = (#t1/1 k) in #ty0
| H, k:dim, #r/0=#s/0, #r/2=#s/2 >> (#t0/0 k) = (#t1/2 k) in #ty0
| ...
| H, k:dim, #r/n-1=#s/n-1, #r/n=#s/n >> (#t0/n-1 k) = (#t1/n k) in #ty0
| H, #r/0=#s/0 >> #cap0 = (#t0/0 #i) in #ty0
| ...
| H, #r/n=#s/n >> #cap0 = (#t0/n #i) in #ty0
| H >> #ty0 = #ty1 hcom type
| H >> #ty0 <= #ty type

hcom/eq/cap

H >> (hcom #i~>#i #ty' #cap [#r/0=#s/0 [k] (#t/0 k)] ... [#r/n=#s/n [k] (#t/n k)]) = #m in #ty
| H >> #cap = #m in #ty
| H, k:dim, #r/0=#s/0 >> (#t/0 k) in #ty'
| ...
| H, k:dim, #r/n=#s/n >> (#t/n k) in #ty'
| H, k:dim, #r/0=#s/0, #r/1=#s/1 >> (#t0 k) = (#t1 k) in #ty'
| H, k:dim, #r/0=#s/0, #r/2=#s/2 >> (#t0 k) = (#t2 k) in #ty'
| ...
| H, k:dim, #r/n-1=#s/n-1, #r/n=#s/n >> (#t/n-1 k) = (#t/n k) in #ty'
| H, #r/0=#s/0 >> #cap = (#t/0 #i) in #ty'
| ...
| H, #r/n=#s/n >> #cap = (#t/n #i) in #ty'
| H >> #ty' hcom type
| H >> #ty' <= #ty type

hcom/eq/tube

H >> (hcom #i~>#j #ty' #cap [#r/0=#s/0 [k] (#t/0 k)] ... [#r/n=#s/n [k] (#t/n k)]) = #m in #ty
where
  #r/0 /= #s/0, ..., #r/l-1 /= #s/l-1 and #r/l = #s/l
| H >> (#t/l #j) = #m in #ty'
| H, k:dim, #r/0=#s/0 >> (#t/0 k) in #ty'
| ...
| H, k:dim, #r/n=#s/n >> (#t/n k) in #ty'
| H, k:dim, #r/0=#s/0, #r/1=#s/1 >> (#t/0 k) = (#t/1 k) in #ty'
| H, k:dim, #r/0=#s/0, #r/2=#s/2 >> (#t/0 k) = (#t/2 k) in #ty'
| ...
| H, k:dim, #r/n-1=#s/n-1, #rn=#sn >> (#t/n-1 k) = (#tn k) in #ty'
| H, #r/0=#s/0 >> #cap = (#t/0 #i) in #ty'
| ...
| H, #r/n=#s/n >> #cap = (#t/n #i) in #ty'
| H >> #ty' hcom type
| H >> #ty' <= #ty type

coe/eq

H >> (coe #i~>#j [u] (#a0 u) #m0) = (coe #i~>#j [u] (#a1 u) #m1) in #ty
| H >> #m0 = #m1 in (#a0 #i)
| H, u:dim >> #a0 = #a1 coe type
| H >> (#a0 #j) <= #ty type

coe/eq/cap

H >> (coe #i~>#i [u] (#a u) #m) = #n in #ty
| H >> #m = #n in #ty
| H, u:dim >> (#a u) coe type
| H >> (#a #i) <= #ty type

Universes

subtype/eq

H >> #a <= #b type
| H >> #a = #b type

universe/eqtype

H >> (U #l #k) = (U #l #k) in (U #l' #k')
where
  #k/univ <-
    discrete if #k == discrete
    kan if #k == kan
    kan if #k == hcom
    coe if #k == coe
    kan if #k == pre
  #l < #l'
  #k/univ <= #k'

universe/subtype

H >> (U #l0 #k0) <= (U #l1 #k1) type
where
  #l0 <= #l1
  #k0 <= #k1