diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt
index 038f01f256a2303cacf1474c1aa5d1d098796abb..6a830ccba8812df2dd44a7d70159fabf63a672ca 100644
--- a/source/MetaTheories.mmt
+++ b/source/MetaTheories.mmt
@@ -373,6 +373,16 @@ theory CuboidType =
   cuboidCons : Rectangle ⟶ point ⟶ Cuboid ❘ # CuboidCons 1 2 ❙
 ❚
 
+theory CylinderType =
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
+  include ?FrameITBasics ❙
+  include ?FrameITCircle ❙
+
+  cylinderType : type ❘ # Cylinder ❙
+  cylinderCons : circle ⟶ point ⟶ Cylinder ❘ # CylinderCons 1 2 ❙
+❚
+
 theory FrameITTheories =
   include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
   include ☞http://mathhub.info/MitM/core/geometry?Planes ❙