diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -6,6 +6,21 @@
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.7.7 — 2025-11-04
+
+Important fixes:
+
+- Fix subtyping (automatic coercion for extension types and tope disjunction elimination) (see [#207](https://github.com/rzk-lang/rzk/pull/207))
+
+  1. Do not assume variance for the argument of function/type family application (fixes #206).
+  2. Separately check tope families and extension types (and $\Pi$-types), since, for tope families, variance of the argument is different.
+  3. Fix `refl` to check for equality, not subtyping.
+  4. Fix `inferAs` to perform `typecheck` instead (where appropriate).
+
+Minor fix:
+
+- Add version bounds for successful Hackage upload (see [`9aba39c`](https://github.com/rzk-lang/rzk/commit/9aba39c9d63799a00438774e947a986fe8bb9d69))
+
 ## v0.7.6 — 2025-08-14
 
 Minor fixes:
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.24
 
--- This file has been generated from package.yaml by hpack version 0.38.0.
+-- This file has been generated from package.yaml by hpack version 0.38.1.
 --
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.7.6
+version:        0.7.7
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 category:       Dependent Types
@@ -73,7 +73,7 @@
     , bifunctors >=5.5.3
     , bytestring >=0.10.8.2
     , directory >=1.2.7.0
-    , mtl >=2.2.2
+    , mtl >=2.3.1
     , template-haskell >=2.14.0.0
     , text >=1.2.3.1
     , yaml >=0.11.0.0
@@ -119,7 +119,7 @@
     , bifunctors >=5.5.3
     , bytestring >=0.10.8.2
     , directory >=1.2.7.0
-    , mtl >=2.2.2
+    , mtl >=2.3.1
     , rzk
     , template-haskell >=2.14.0.0
     , text >=1.2.3.1
@@ -154,7 +154,7 @@
     , bytestring >=0.10.8.2
     , directory >=1.2.7.0
     , doctest >=0.21.0
-    , mtl >=2.2.2
+    , mtl >=2.3.1
     , template-haskell >=2.14.0.0
     , text >=1.2.3.1
     , yaml >=0.11.0.0
@@ -187,7 +187,7 @@
     , directory >=1.2.7.0
     , hspec
     , hspec-discover
-    , mtl >=2.2.2
+    , mtl >=2.3.1
     , rzk
     , template-haskell >=2.14.0.0
     , text >=1.2.3.1
diff --git a/src/Language/Rzk/VSCode/Handlers.hs b/src/Language/Rzk/VSCode/Handlers.hs
--- a/src/Language/Rzk/VSCode/Handlers.hs
+++ b/src/Language/Rzk/VSCode/Handlers.hs
@@ -21,7 +21,8 @@
 import           Control.Monad                 (forM_, when)
 import           Control.Monad.Except          (ExceptT (ExceptT),
                                                 MonadError (throwError),
-                                                modifyError, runExceptT)
+                                                runExceptT)
+import           Control.Monad.Error.Class     (modifyError)
 import           Control.Monad.IO.Class        (MonadIO (..))
 import           Data.Default.Class
 import           Data.List                     (isSuffixOf, sort, (\\))
diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs
--- a/src/Rzk/TypeCheck.hs
+++ b/src/Rzk/TypeCheck.hs
@@ -523,9 +523,9 @@
     , "  " <> show (untyped term) ]
 
   ActionUnifyTerms expected actual ->
-    [ "unifying term"
+    [ "unifying term (expected)"
     , "  " <> show expected
-    , "with term"
+    , "with term (actual)"
     , "  " <> show actual ]
 
   ActionInfer term ->
@@ -609,7 +609,8 @@
 
 data Covariance
   = Covariant     -- ^ Positive position.
-  | Contravariant -- ^ Negative position
+  | Contravariant -- ^ Negative position.
+  | Invariant     -- ^ Unknown position.
 
 data RenderBackend
   = RenderSVG
@@ -1328,7 +1329,12 @@
     where
       switch Covariant     = Contravariant
       switch Contravariant = Covariant
+      switch Invariant     = Invariant
 
+setVariance :: Covariance -> TypeCheck var a -> TypeCheck var a
+setVariance variance = local $ \Context{..} -> Context
+  { covariance = variance, .. }
+
 enterScopeContext :: Maybe VarIdent -> TermT var -> Context var -> Context (Inc var)
 enterScopeContext orig ty context =
   addVarInCurrentScope Z VarInfo
@@ -1859,7 +1865,7 @@
 unifyViaDecompose expected actual | expected == actual = return ()
 unifyViaDecompose (AppT _ f x) (AppT _ g y) = do
   unify Nothing f g
-  unify Nothing x y
+  setVariance Invariant $ unify Nothing x y
 unifyViaDecompose _ _ = issueTypeError (TypeErrorOther "cannot decompose")
 
 unifyInCurrentContext :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var ()
@@ -1867,205 +1873,223 @@
   unifyViaDecompose expected actual `catchError` \_ -> do      -- NOTE: this gives a small, but noticeable speedup
     expectedVal <- whnfT expected
     actualVal <- whnfT actual
-    (expected', actual') <- asks covariance >>= \case
-      Covariant     -> etaMatch mterm expectedVal actualVal
-      Contravariant -> swap <$> etaMatch mterm actualVal expectedVal
-    unless (expected' == actual') $ do  -- NOTE: this gives a small, but noticeable speedup
-      case actual' of
-        RecBottomT{} -> return ()
-        RecOrT _ty rs' ->
-          case expected' of
-            RecOrT _ty rs -> sequence_ $
-              checkCoherence <$> rs <*> rs'
-            _ -> do
-              forM_ rs' $ \(tope, term) ->
-                localTope tope $
-                  unifyTerms expected' term
-        _ -> typeOf expected' >>= typeOf >>= \case
-          UniverseCubeT{} -> contextEntails (topeEQT expected' actual')
-          _ -> do
-            let def = unless (expected' == actual') err
-                err =
-                  case mterm of
-                    Nothing   -> issueTypeError (TypeErrorUnifyTerms expected' actual')
-                    Just term -> issueTypeError (TypeErrorUnify term expected' actual')
-                errS = do
-                  let expectedS = S <$> expected'
-                      actualS = S <$> actual'
-                  case mterm of
-                    Nothing   -> issueTypeError (TypeErrorUnifyTerms expectedS actualS)
-                    Just term -> issueTypeError (TypeErrorUnify (S <$> term) expectedS actualS)
-            case expected' of
-              Pure{} -> def
-
-              UniverseT{} -> def
-              UniverseCubeT{} -> def
-              UniverseTopeT{} -> def
+    mea <- asks covariance >>= \case
+      Covariant     -> Just <$> etaMatch mterm expectedVal actualVal
+      Contravariant -> Just . swap <$> etaMatch mterm actualVal expectedVal
+      Invariant     -> traceTypeCheck Debug "invariant" $ do
+        -- FIXME: inefficient
+        traceTypeCheck Debug "invariant->covariant" $ 
+          setVariance Covariant     $ unifyInCurrentContext mterm expectedVal actualVal
+        traceTypeCheck Debug "invariant->contravariant" $ 
+          setVariance Contravariant $ unifyInCurrentContext mterm expectedVal actualVal
+        return Nothing
+    case mea of
+      Nothing -> return ()
+      Just (expected', actual') ->
+        unless (expected' == actual') $ do  -- NOTE: this gives a small, but noticeable speedup
+          case actual' of
+            RecBottomT{} -> return ()
+            RecOrT _ty rs' ->
+              case expected' of
+                RecOrT _ty rs -> sequence_ $
+                  checkCoherence <$> rs <*> rs'
+                _ -> do
+                  forM_ rs' $ \(tope, term) ->
+                    localTope tope $
+                      unifyTerms expected' term
+            _ -> typeOf expected' >>= typeOf >>= \case
+              UniverseCubeT{} -> contextEntails (topeEQT expected' actual')
+              _ -> do
+                let def = unless (expected' == actual') err
+                    err =
+                      case mterm of
+                        Nothing   -> issueTypeError (TypeErrorUnifyTerms expected' actual')
+                        Just term -> issueTypeError (TypeErrorUnify term expected' actual')
+                    errS = do
+                      let expectedS = S <$> expected'
+                          actualS = S <$> actual'
+                      case mterm of
+                        Nothing   -> issueTypeError (TypeErrorUnifyTerms expectedS actualS)
+                        Just term -> issueTypeError (TypeErrorUnify (S <$> term) expectedS actualS)
+                case expected' of
+                  Pure{} -> def
 
-              TypeUnitT{} -> def
-              UnitT{} -> return ()  -- Unit always unifies!
+                  UniverseT{} -> def
+                  UniverseCubeT{} -> def
+                  UniverseTopeT{} -> def
 
-              CubeUnitT{} -> def
-              CubeUnitStarT{} -> def
-              Cube2T{} -> def
-              Cube2_0T{} -> def
-              Cube2_1T{} -> def
-              CubeProductT _ l r ->
-                case actual' of
-                  CubeProductT _ l' r' -> do
-                    unifyTerms l l'
-                    unifyTerms r r'
-                  _ -> err
+                  TypeUnitT{} -> def
+                  UnitT{} -> return ()  -- Unit always unifies!
 
-              PairT _ty l r ->
-                case actual' of
-                  PairT _ty' l' r' -> do
-                    unifyTerms l l'
-                    unifyTerms r r'
+                  CubeUnitT{} -> def
+                  CubeUnitStarT{} -> def
+                  Cube2T{} -> def
+                  Cube2_0T{} -> def
+                  Cube2_1T{} -> def
+                  CubeProductT _ l r ->
+                    case actual' of
+                      CubeProductT _ l' r' -> do
+                        unifyTerms l l'
+                        unifyTerms r r'
+                      _ -> err
 
-                  -- one part of eta-expansion for pairs
-                  -- FIXME: add symmetric version!
-                  _ -> err
+                  PairT _ty l r ->
+                    case actual' of
+                      PairT _ty' l' r' -> do
+                        unifyTerms l l'
+                        unifyTerms r r'
 
-              FirstT _ty t ->
-                case actual' of
-                  FirstT _ty' t' -> unifyTerms t t'
-                  _              -> err
+                      -- one part of eta-expansion for pairs
+                      -- FIXME: add symmetric version!
+                      _ -> err
 
-              SecondT _ty t ->
-                case actual' of
-                  SecondT _ty' t' -> unifyTerms t t'
-                  _               -> err
+                  FirstT _ty t ->
+                    case actual' of
+                      FirstT _ty' t' -> unifyTerms t t'
+                      _              -> err
 
-              TopeTopT{}    -> unifyTopes expected' actual'
-              TopeBottomT{} -> unifyTopes expected' actual'
-              TopeEQT{}     -> unifyTopes expected' actual'
-              TopeLEQT{}    -> unifyTopes expected' actual'
-              TopeAndT{}    -> unifyTopes expected' actual'
-              TopeOrT{}     -> unifyTopes expected' actual'
+                  SecondT _ty t ->
+                    case actual' of
+                      SecondT _ty' t' -> unifyTerms t t'
+                      _               -> err
 
-              RecBottomT{} -> return () -- unifies with anything
-              RecOrT _ty rs ->
-                case actual' of
-                  -- ----------------------------------------------
-                  -- IMPORTANT: this pattern matching is redundant,
-                  -- but it is not obvious, so
-                  -- take care when refactoring!
-                  -- ----------------------------------------------
-  --                RecOrT _ty rs' -> sequence_ $
-  --                  checkCoherence <$> rs <*> rs'
-                  -- ----------------------------------------------
-                  _ -> do
-                    forM_ rs $ \(tope, term) ->
-                      localTope tope $
-                        unifyTerms term actual'
+                  TopeTopT{}    -> unifyTopes expected' actual'
+                  TopeBottomT{} -> unifyTopes expected' actual'
+                  TopeEQT{}     -> unifyTopes expected' actual'
+                  TopeLEQT{}    -> unifyTopes expected' actual'
+                  TopeAndT{}    -> unifyTopes expected' actual'
+                  TopeOrT{}     -> unifyTopes expected' actual'
 
-              TypeFunT _ty _orig cube mtope ret ->
-                case actual' of
-                  TypeFunT _ty' orig' cube' mtope' ret' -> do
-                    switchVariance $  -- unifying in the negative position!
-                      unifyTerms cube cube' -- FIXME: unifyCubes
-                    enterScope orig' cube $ do
-                      case ret' of
-                        -- UniverseTopeT{} ->
-                        --   (Just tope, Just tope') -> do
-                        --     topeNF <- nfT tope
-                        --     topeNF' <- nfT tope'
-                        --     unifyTopes topeNF topeNF'
-                        --   (Nothing, Nothing)      -> return ()
-                        --   (Just tope, Nothing)    -> nfT tope >>= (`unifyTopes` topeTopT)
-                        --   (Nothing, Just tope)    -> nfT tope >>= unifyTopes topeTopT
-                        _ -> case (mtope, mtope') of
-                          (Just tope, Just tope') -> do
-                            topeNF <- nfT tope
-                            topeNF' <- nfT tope'
-                            unifyTopes topeNF topeNF'
-                          (Nothing, Nothing)      -> return ()
-                          (Just tope, Nothing)    -> nfT tope >>= (`unifyTopes` topeTopT)
-                          (Nothing, Just tope)    -> nfT tope >>= unifyTopes topeTopT
-                      case mterm of
-                        Nothing -> unifyTerms ret ret'
-                        Just term -> unifyTypes (appT ret' (S <$> term) (Pure Z)) ret ret'
-                  _ -> err
+                  RecBottomT{} -> return () -- unifies with anything
+                  RecOrT _ty rs ->
+                    case actual' of
+                      -- ----------------------------------------------
+                      -- IMPORTANT: this pattern matching is redundant,
+                      -- but it is not obvious, so
+                      -- take care when refactoring!
+                      -- ----------------------------------------------
+      --                RecOrT _ty rs' -> sequence_ $
+      --                  checkCoherence <$> rs <*> rs'
+                      -- ----------------------------------------------
+                      _ -> do
+                        forM_ rs $ \(tope, term) ->
+                          localTope tope $
+                            unifyTerms term actual'
 
-              TypeSigmaT _ty _orig a b ->
-                case actual' of
-                  TypeSigmaT _ty' orig' a' b' -> do
-                    unify Nothing a a'
-                    enterScope orig' a $ unify Nothing b b'
-                  _ -> err
+                  TypeFunT _ty _orig cube mtope ret ->
+                    case actual' of
+                      TypeFunT _ty' orig' cube' mtope' ret' -> do
+                        switchVariance $  -- unifying in the negative position!
+                          unifyTerms cube cube' -- FIXME: unifyCubes
+                        enterScope orig' cube $ do
+                          case ret' of
+                            UniverseTopeT{} -> do
+                              -- This is the case for tope families (shapes)
+                              --
+                              -- (Λ → TOPE) <: (Δ → TOPE)
+                              -- since if φ : Λ → TOPE
+                              -- then φ ⊢ Δ
+                              --
+                              -- we DO NOT take tope context Φ into account!
+                              expectedTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope
+                              actualTopeNF   <- fromMaybe topeTopT <$> traverse nfT mtope'
+                              actualEntailsExpected <- [actualTopeNF] `entailM` expectedTopeNF
+                              unless actualEntailsExpected $
+                                issueTypeError (TypeErrorTopeNotSatisfied [actualTopeNF] expectedTopeNF)
+                            _ -> do
+                              -- this is the case for Π-types and extension types
+                              --
+                              -- Ξ | Φ | Γ   ⊢   {t : I | φ} → A t   <:   {s : J | ψ} → B s
+                              -- when
+                              -- Ξ | Φ, ψ ⊢ φ
+                              expectedTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope
+                              actualTopeNF   <- fromMaybe topeTopT <$> traverse nfT mtope'
+                              localTope expectedTopeNF $
+                                contextEntails actualTopeNF
+                          case mterm of
+                            Nothing -> unifyTerms ret ret'
+                            Just term -> unifyTypes (appT ret' (S <$> term) (Pure Z)) ret ret'
+                      _ -> err
 
-              TypeIdT _ty x _tA y ->
-                case actual' of
-                  TypeIdT _ty' x' _tA' y' -> do
-                    -- unify Nothing tA tA' -- TODO: do we need this check?
-                    unify Nothing x x'
-                    unify Nothing y y'
-                  _ -> err
+                  TypeSigmaT _ty _orig a b ->
+                    case actual' of
+                      TypeSigmaT _ty' orig' a' b' -> do
+                        unify Nothing a a'
+                        enterScope orig' a' $ unify Nothing b b'
+                      _ -> err
 
-              AppT _ty f x ->
-                case actual' of
-                  AppT _ty' f' x' -> do
-                    unify Nothing f f'
-                    unify Nothing x x'
-                  _ -> err
+                  TypeIdT _ty x _tA y ->
+                    case actual' of
+                      TypeIdT _ty' x' _tA' y' -> do
+                        -- unify Nothing tA tA' -- TODO: do we need this check?
+                        unify Nothing x x'
+                        unify Nothing y y'
+                      _ -> err
 
-              LambdaT ty _orig _mparam body ->
-                case stripTypeRestrictions (infoType ty) of
-                  TypeFunT _ty _origF param mtope _ret ->
+                  AppT _ty f x ->
                     case actual' of
-                      LambdaT ty' orig' _mparam' body' -> do
-                        case stripTypeRestrictions (infoType ty') of
-                          TypeFunT _ty' _origF' param' mtope' _ret' -> do
-                            unify Nothing param param'
-                            enterScope orig' param $ do
-                              case (mtope, mtope') of
-                                (Just tope, Just tope') -> do
-                                  unify Nothing tope tope'
-                                  localTope tope $ unify Nothing body body'
-                                (Nothing, Nothing) -> do
-                                  unify Nothing body body'
-                                _ -> errS
+                      AppT _ty' f' x' -> do
+                        unify Nothing f f'
+                        setVariance Invariant $
+                          unify Nothing x x'
+                      _ -> err
+
+                  LambdaT ty _orig _mparam body ->
+                    case stripTypeRestrictions (infoType ty) of
+                      TypeFunT _ty _origF param mtope _ret ->
+                        case actual' of
+                          LambdaT ty' orig' _mparam' body' -> do
+                            case stripTypeRestrictions (infoType ty') of
+                              TypeFunT _ty' _origF' param' mtope' _ret' -> do
+                                unify Nothing param param' -- we (should) have already checked this in types!
+                                enterScope orig' param $ do
+                                  case (mtope, mtope') of
+                                    (Just tope, Just tope') -> do
+                                      unify Nothing tope tope' -- we (should) have already checked this in types!
+                                      localTope tope $ unify Nothing body body'
+                                    (Nothing, Nothing) -> do
+                                      unify Nothing body body'
+                                    _ -> errS
+                              _ -> err
                           _ -> err
                       _ -> err
-                  _ -> err
 
-              ReflT ty _x | TypeIdT _ty x _tA y <- infoType ty ->
-                case actual' of
-                  ReflT ty' _x' | TypeIdT _ty' x' _tA' y' <- infoType ty' -> do
-                    -- unify Nothing tA tA' -- TODO: do we need this check?
-                    unify Nothing x x'
-                    unify Nothing y y'
-                  _ -> err
-              ReflT{} -> panicImpossible "refl with a non-identity type!"
+                  ReflT ty _x | TypeIdT _ty x _tA y <- infoType ty ->
+                    case actual' of
+                      ReflT ty' _x' | TypeIdT _ty' x' _tA' y' <- infoType ty' -> do
+                        -- unify Nothing tA tA' -- TODO: do we need this check?
+                        unify Nothing x x'
+                        unify Nothing y y'
+                      _ -> err
+                  ReflT{} -> panicImpossible "refl with a non-identity type!"
 
-              IdJT _ty a b c d e f ->
-                case actual' of
-                  IdJT _ty' a' b' c' d' e' f' -> do
-                    unify Nothing a a'
-                    unify Nothing b b'
-                    unify Nothing c c'
-                    unify Nothing d d'
-                    unify Nothing e e'
-                    unify Nothing f f'
-                  _ -> err
+                  IdJT _ty a b c d e f ->
+                    case actual' of
+                      IdJT _ty' a' b' c' d' e' f' -> do
+                        unify Nothing a a'
+                        unify Nothing b b'
+                        unify Nothing c c'
+                        unify Nothing d d'
+                        unify Nothing e e'
+                        unify Nothing f f'
+                      _ -> err
 
-              TypeAscT{} -> panicImpossible "type ascription at the root of WHNF"
+                  TypeAscT{} -> panicImpossible "type ascription at the root of WHNF"
 
-              TypeRestrictedT _ty ty rs ->
-                case actual' of
-                  TypeRestrictedT _ty' ty' rs' -> do
-                    unify mterm ty ty'
-                    sequence_
-                      [ localTope tope $ do
-                          -- FIXME: can do less entails checks?
-                          contextEntails (foldr topeOrT topeBottomT (map fst rs')) -- expected is less specified than actual
-                          forM_ rs' $ \(tope', term') -> do
-                            localTope tope' $
-                              unify Nothing term term'
-                      | (tope, term) <- rs
-                      ]
-                  _ -> err    -- FIXME: need better unification for restrictions
+                  TypeRestrictedT _ty ty rs ->
+                    case actual' of
+                      TypeRestrictedT _ty' ty' rs' -> do
+                        unify mterm ty ty'
+                        sequence_
+                          [ localTope tope $ do
+                              -- FIXME: can do less entails checks?
+                              contextEntails (foldr topeOrT topeBottomT (map fst rs')) -- expected is less specified than actual
+                              forM_ rs' $ \(tope', term') -> do
+                                localTope tope' $
+                                  unify Nothing term term'
+                          | (tope, term) <- rs
+                          ]
+                      _ -> err    -- FIXME: need better unification for restrictions
 
   where
     action = case mterm of
@@ -2460,10 +2484,10 @@
                 xty' <- typecheck xty universeT
                 unifyTerms tA xty'
               x' <- typecheck x tA
-              unifyTerms x' y
-              unifyTerms x' z
+              unifyTerms x' y >> unifyTerms y x'
+              unifyTerms x' z >> unifyTerms z x'
             when (isNothing mx) $
-              unifyTerms y z
+              unifyTerms y z >> unifyTerms z y
             return (reflT ty' (Just (y, Just tA)))
           _ -> issueTypeError $ TypeErrorUnexpectedRefl term ty
 
@@ -2517,7 +2541,15 @@
     lt <- typeOf l'
     rt <- typeOf r'
     typeOf lt >>= \case
+      --    Γ ⊢ l ⇒ (I : CUBE)
+      --    Γ ⊢ r ⇒ (J : CUBE)
+      -- ———————————————————————————
+      -- Γ ⊢ (l, r) ⇒ (I × J : CUBE)
       UniverseCubeT{} -> return (pairT (cubeProductT lt rt) l' r')
+      --    Γ ⊢ l ⇒ (A : U)
+      --    Γ ⊢ r ⇒ (B : U)
+      -- ———————————————————————————
+      -- Γ ⊢ (l, r) ⇒ (A × B : U)             where A × B = Σ (_ : A), B
       _ -> do
         -- NOTE: infer as a non-dependent pair!
         return (pairT (typeSigmaT Nothing lt (S <$> rt)) l' r')
@@ -2573,6 +2605,11 @@
     contextEntails topeBottomT
     return recBottomT
 
+  -- Γ ⊢ t ⇒ (T : K)
+  -- Γ ⊢ K ≡ U
+  -- —————————————
+  -- Γ ⊢ t ⇒ T ⇐ U
+
   RecOr rs -> do
     ttts <- forM rs $ \(tope, term) -> do
       tope' <- typecheck tope topeT
@@ -2598,12 +2635,12 @@
             issueTypeError $ TypeErrorOther "tope params are illegal"
           _ -> do
             mapM_ checkNameShadowing orig
-            b' <- enterScope orig a' $ inferAs universeT b
+            b' <- enterScope orig a' $ typecheck b universeT
             return (typeFunT orig a' Nothing b')
       -- an argument can be a cube
       UniverseCubeT{} -> do
         mapM_ checkNameShadowing orig
-        b' <- enterScope orig a' $ inferAs universeT b
+        b' <- enterScope orig a' $ typecheck b universeT
         return (typeFunT orig a' Nothing b')
       -- an argument can be a shape
       TypeFunT _ty _orig cube mtope UniverseTopeT{} -> do
@@ -2611,7 +2648,7 @@
         enterScope orig cube $ do
           let tope' = appT topeT (S <$> a') (Pure Z)  -- eta expand a'
           localTope tope' $ do
-            b' <- inferAs universeT b
+            b' <- typecheck b universeT
             case mtope of
               Nothing -> return (typeFunT orig cube (Just tope') b')
               Just tope'' -> return (typeFunT orig cube (Just (topeAndT tope'' tope')) b')
@@ -2623,13 +2660,13 @@
     enterScope orig cube' $ do
       tope' <- typecheck tope topeT
       localTope tope' $ do
-        ret' <- inferAs universeT ret
+        ret' <- typecheck ret universeT
         return (typeFunT orig cube' (Just tope') ret')
 
   TypeSigma orig a b -> do
-    a' <- inferAs universeT a  -- FIXME: separate universe of universes from universe of types
+    a' <- typecheck a universeT
     mapM_ checkNameShadowing orig
-    b' <- enterScope orig a' $ inferAs universeT b
+    b' <- enterScope orig a' $ typecheck b universeT
     return (typeSigmaT orig a' b')
 
   TypeId x (Just tA) y -> do
@@ -2647,7 +2684,6 @@
   App f x -> do
     f' <- inferAs universeT f
     fmap stripTypeRestrictions (typeOf f') >>= \case
-      RecBottomT{} -> pure recBottomT -- FIXME: is this ok?
       TypeFunT _ty _orig a mtope b -> do
         x' <- typecheck x a
         let result = appT (substituteT x' b) f' x'
@@ -2732,7 +2768,7 @@
     return (idJT ret tA' a' tC' d' x' p')
 
   TypeAsc term ty -> do
-    ty' <- inferAs universeT ty
+    ty' <- inferAs universeT ty -- this works on types AND cubes
     term' <- typecheck term ty'
     return (typeAscT term' ty')