What is the reasoning behind the interval type being non-inductively defined? about cubical HOT 3 CLOSED

The "real line" analogy is just supposed to convey that I represents something continuous – in particular, a continuous path between two endpoints. Following this intuition, for a discrete type like Bool we therefore shouldn't be able to define a function like:

f : I → Bool
f i0 = false
f i1 = true

because it would be 'discontinuous' on I. Not defining I as an inductive type ensures that we cannot pattern match and 'break' continuity when defining maps I → A.

Side-note: Interpreting maps I → A as equalities, the ability to define functions like f would be disastrous since it would allow us to prove that any two terms of any type are equal. For a general p : I → A, no pattern matching means the only thing we can do is define reflexivity p i = x for some x : A, which I think is quite nice.

Side-note 2: Assuming one believes that I is 'continuous', higher inductive types are what allow us to define types which are not discrete, since adding a path constructor is exactly adding a nontrivial (continuous) map out of I -- a continuous line in our type.

from cubical.

Indeed, if we could define functions by pattern-matching on I like that then we can construct

p : Path U Unit Empty
p i0 = Unit
p i1 = Empty

making the theory inconsistent (transporting tt along this path would give you an inhabitant of Empty). It is hence important that the interval is connected.

from cubical.

Thank you for the replies. The reasons given make sense to me.

from cubical.