module manifold where
import etale

HomogeneousStructure (V: U): U = undefined
et (A B: U): EtaleMap A B -> (A -> B) = undefined
isSurjective (A B: U) (f: A -> B): U = undefined

manifold (V': U) (V: HomogeneousStructure V'): U
  = (M: U)
  * (W: U)
  * (w: EtaleMap W M)
  * (covers: isSurjective W M (et W M w))
  * (   EtaleMap W V')