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
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