import Applicative import CoherentlyConstant import DeMorKan import FirstGroupCohomology import Hats import MonoidalFibres import NatChurchMonoid import ObjectClassifier import PointwiseMonoidal import Shapes import TangentBundles import Torus import Untruncate