Contents

# Contents

## Idea

In homotopy type theory a square type is the product type of the interval type with itself.