Cubical Set(oid)s in Agda
This is a direct agda definition of the nominal presentation of cubical sets, roughly following descriptions from Cohen, Coquand, Huber, Mortberg, and Pitts.
Because these are defined directly in Agda we use a representation similar to
families of setoids (as a flattened E-functor Cat[Cubesα΅α΅, Setoids]). Another
difference is that our category of cubes uses a kind of defunctionalized
substitution for morphisms Cubes[J, I] rather than the function space Set[I, deMorgan(J)].
We can define the interval in HIT style as follows:
data Interval (I : Sym) : Set where
west : Interval I
east : Interval I
walk : (Ο : π I) β Interval I
interval : β‘Set
obj interval = Interval
hom interval I west west = T.π
hom interval I east east = T.π
hom interval I west (walk Οβ) = Οβ π.β
#0
hom interval I east (walk Οβ) = Οβ π.β
#1
hom interval I (walk Οβ) west = Οβ π.β
#0
hom interval I (walk Οβ) east = Οβ π.β
#1
hom interval I (walk Οβ) (walk Οβ) = Οβ π.β
Οβ
β¦
Now we can reason about relatedness of the interval operators:
-- walk "a" β
west (under {"a" β #0})
Οβ :
hom interval []
(sub interval ("a" β #0 β· []) (walk βͺ "a" β«))
west
Οβ = π.idn refl
-- walk (Β¬ "a" β¨ "b") β
east (under {"a" β #0; "b" β #0})
Οβ :
hom interval []
(sub interval ("a" β #0 β· "b" β #0 β· []) (walk (Β¬ βͺ "a" β« β¨ βͺ "b" β«)))
east
Οβ = π.seq π.β¨-uni π.Β¬-#0