    -- | Implementations of the basic primitives of Cubical Agda: The
    -- interval and its operations.

    module Agda.TypeChecking.Primitive.Cubical.Base
      ( requireCubical
      , primIntervalType
      , primIMin', primIMax', primINeg'
      , imax, imin, ineg

      , Command(..), KanOperation(..), kanOpName, TermPosition(..), headStop
      , FamilyOrNot(..), familyOrNot

        -- * Helper functions for building terms
      , combineSys, combineSys'
      , fiber, hfill
      , decomposeInterval', decomposeInterval
      , reduce2Lam
      , isCubicalSubtype
      )
      where

    import Control.Monad        ( msum, mzero )
    import Control.Monad.Except ( MonadError )

    import qualified Data.IntMap as IntMap
    import Data.IntMap (IntMap)
    import Data.String (IsString (fromString))
    import Data.Bifunctor (second)
    import Data.Either (partitionEithers)
    import Data.Maybe (fromMaybe, maybeToList)

    import qualified Agda.Utils.BoolSet as BoolSet
    import Agda.Utils.Impossible (__IMPOSSIBLE__)
    import Agda.Utils.BoolSet (BoolSet)
    import Agda.Utils.Functor

    import Agda.TypeChecking.Monad.Signature (HasConstInfo)
    import Agda.TypeChecking.Monad.Debug (__IMPOSSIBLE_VERBOSE__)
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Monad.Context
    import Agda.TypeChecking.Monad.Pure
    import Agda.TypeChecking.Monad.Base

    import Agda.TypeChecking.Substitute.Class (absBody, raise, apply)

    import Agda.TypeChecking.Reduce (Reduce(..), reduceB', reduce', reduce)
    import Agda.TypeChecking.Names (NamesT, runNamesT, ilam, lam)

    import Agda.Syntax.Common
      (Cubical(..), Arg(..), relevant, irrelevant, setRelevance, defaultArgInfo, hasQuantity0)

    import Agda.TypeChecking.Primitive.Base
      (SigmaKit(..), (-->), nPi', pPi', (<@>), (<#>), (<..>), argN, getSigmaKit)

    import Agda.Syntax.Internal

    -- | Checks that the correct variant of Cubical Agda is activated.
    -- Note that @--erased-cubical@ \"counts as\" @--cubical@ in erased
    -- contexts.
    requireCubical
      :: Cubical -- ^ Which variant of Cubical Agda is required?
      -> TCM ()
    requireCubical :: Cubical -> TCM ()
    requireCubical Cubical
    wanted = Cubical -> String -> TCM ()
    requireCubical' Cubical
    wanted String
    ""

    -- | Generalization of 'requireCubical' supplying a reason.
    requireCubical'
      :: Cubical -- ^ Which variant of Cubical Agda is required?
      -> String  -- ^ Why, exactly, do we need Cubical to be enabled?
      -> TCM ()
    requireCubical' :: Cubical -> String -> TCM ()
    requireCubical' Cubical
    wanted String
    reason = do
      cubical         <- TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption
      inErasedContext <- hasQuantity0 <$> viewTC eQuantity
      case cubical of
        Just Cubical
    CFull -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Just Cubical
    CErased | Cubical
    wanted Cubical -> Cubical -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cubical
    CErased Bool -> Bool -> Bool
    || Bool
    inErasedContext -> () -> TCM ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Maybe Cubical
    _ -> TypeError -> TCM ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ Cubical -> String -> TypeError
    NeedOptionCubical Cubical
    wanted String
    reason

    -- | Our good friend the interval type.
    primIntervalType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Type
    primIntervalType :: forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType = Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    intervalSort (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInterval

    -- | Negation on the interval. Negation satisfies De Morgan's laws, and
    -- their implementation is handled here.
    primINeg' :: TCM PrimitiveImpl
    primINeg' :: TCM PrimitiveImpl
    primINeg' = do
      Cubical -> TCM ()
    requireCubical Cubical
    CErased
      t <- TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType TCMT IO Type -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 1 $ \case
        [Arg Term
    x] -> do
          unview <- ReduceM (IntervalView -> Term)
    forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
    intervalUnview'
          view <- intervalView'
          sx <- reduceB' x
          ix <- intervalView (unArg $ ignoreBlocking sx)

          -- Apply De Morgan's laws.
          let
            ineg :: Arg Term -> Arg Term
            ineg = (Term -> Term) -> Arg Term -> Arg Term
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (IntervalView -> Term
    unview (IntervalView -> Term) -> (Term -> IntervalView) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntervalView -> IntervalView
    f (IntervalView -> IntervalView)
    -> (Term -> IntervalView) -> Term -> IntervalView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> IntervalView
    view)

            f IntervalView
    ix = case IntervalView
    ix of
              IntervalView
    IZero    -> IntervalView
    IOne
              IntervalView
    IOne     -> IntervalView
    IZero
              IMin Arg Term
    x Arg Term
    y -> Arg Term -> Arg Term -> IntervalView
    IMax (Arg Term -> Arg Term
    ineg Arg Term
    x) (Arg Term -> Arg Term
    ineg Arg Term
    y)
              IMax Arg Term
    x Arg Term
    y -> Arg Term -> Arg Term -> IntervalView
    IMin (Arg Term -> Arg Term
    ineg Arg Term
    x) (Arg Term -> Arg Term
    ineg Arg Term
    y)
              INeg Arg Term
    x   -> Term -> IntervalView
    OTerm (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    x)
              OTerm Term
    t  -> Arg Term -> IntervalView
    INeg (ArgInfo -> Term -> Arg Term
    forall e. ArgInfo -> e -> Arg e
    Arg ArgInfo
    defaultArgInfo Term
    t)

          -- We force the argument in case it happens to be an interval
          -- expression, but it's quite possible that it's _not_. In those
          -- cases, negation is stuck.
          case ix of
            OTerm Term
    t -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced MaybeReducedArgs Term
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall no yes. no -> Reduced no yes
    NoReduction [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    sx]
            IntervalView
    _       -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (IntervalView -> Term
    unview (IntervalView -> Term) -> IntervalView -> Term
    forall a b. (a -> b) -> a -> b
    $ IntervalView -> IntervalView
    f IntervalView
    ix)
        [Arg Term]
    _ -> String -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ String
    "implementation of primINeg called with wrong arity"

    -- | Internal helper for constructing binary operations on the interval,
    -- parameterised by their unit and absorbing elements.
    primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl
    primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl
    primIBin IntervalView
    unit IntervalView
    absorber = do
      Cubical -> TCM ()
    requireCubical Cubical
    CErased
      t <- TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType TCMT IO Type -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType TCMT IO Type -> TCMT IO Type -> TCMT IO Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> TCMT IO Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 2 $ \case
        [Arg Term
    x,Arg Term
    y] -> do
          -- Evaluation here is short-circuiting: If the LHS is either the
          -- absorbing or unit element, then the RHS does not matter.
          sx <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    x
          ix <- intervalView (unArg $ ignoreBlocking sx)
          case ix of
            IntervalView
    ix | IntervalView
    ix IntervalView -> IntervalView -> Bool
    ==% IntervalView
    absorber -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IntervalView -> ReduceM Term
    forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
    intervalUnview IntervalView
    absorber
            IntervalView
    ix | IntervalView
    ix IntervalView -> IntervalView -> Bool
    ==% IntervalView
    unit     -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced MaybeReducedArgs Term
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ Simplification -> Term -> Reduced MaybeReducedArgs Term
    forall no yes. Simplification -> yes -> Reduced no yes
    YesReduction Simplification
    YesSimplification (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    y)
            IntervalView
    _ -> do
              -- And in the case where the LHS is stuck, we can make
              -- progress by comparing the LHS to the absorbing/unit
              -- elements.
              sy <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    y
              iy <- intervalView (unArg $ ignoreBlocking sy)
              case iy of
                IntervalView
    iy | IntervalView
    iy IntervalView -> IntervalView -> Bool
    ==% IntervalView
    absorber -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< IntervalView -> ReduceM Term
    forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
    intervalUnview IntervalView
    absorber
                IntervalView
    iy | IntervalView
    iy IntervalView -> IntervalView -> Bool
    ==% IntervalView
    unit     -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced MaybeReducedArgs Term
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ Simplification -> Term -> Reduced MaybeReducedArgs Term
    forall no yes. Simplification -> yes -> Reduced no yes
    YesReduction Simplification
    YesSimplification (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    x)
                IntervalView
    _                    -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Reduced MaybeReducedArgs Term
     -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall no yes. no -> Reduced no yes
    NoReduction [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    sx,Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    sy]
        [Arg Term]
    _ -> String -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ String
    "binary operation on the interval called with incorrect arity"
      where
        ==% :: IntervalView -> IntervalView -> Bool
    (==%) IntervalView
    IZero IntervalView
    IZero = Bool
    True
        (==%) IntervalView
    IOne IntervalView
    IOne = Bool
    True
        (==%) IntervalView
    _ IntervalView
    _ = Bool
    False
    {-# INLINE primIBin #-}

    -- | Implements both the @min@ connection /and/ conjunction on the
    -- cofibration classifier.
    primIMin' :: TCM PrimitiveImpl
    primIMin' :: TCM PrimitiveImpl
    primIMin' = do
      Cubical -> TCM ()
    requireCubical Cubical
    CErased
      IntervalView -> IntervalView -> TCM PrimitiveImpl
    primIBin IntervalView
    IOne IntervalView
    IZero

    -- | Implements both the @max@ connection /and/ disjunction on the
    -- cofibration classifier.
    primIMax' :: TCM PrimitiveImpl
    primIMax' :: TCM PrimitiveImpl
    primIMax' = do
      Cubical -> TCM ()
    requireCubical Cubical
    CErased
      IntervalView -> IntervalView -> TCM PrimitiveImpl
    primIBin IntervalView
    IZero IntervalView
    IOne

    -- | A helper for evaluating @max@ on the interval in TCM&co.
    imax :: HasBuiltins m => m Term -> m Term -> m Term
    imax :: forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
    imax m Term
    x m Term
    y = do
      x' <- m Term
    x
      y' <- y
      intervalUnview (IMax (argN x') (argN y'))

    -- | A helper for evaluating @min@ on the interval in TCM&co.
    imin :: HasBuiltins m => m Term -> m Term -> m Term
    imin :: forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
    imin m Term
    x m Term
    y = do
      x' <- m Term
    x
      y' <- y
      intervalUnview (IMin (argN x') (argN y'))

    -- | A helper for evaluating @neg@ on the interval in TCM&co.
    ineg :: HasBuiltins m => m Term -> m Term
    ineg :: forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg m Term
    x = do
      x' <- m Term
    x
      intervalUnview (INeg (argN x'))

    data Command = DoTransp | DoHComp
      deriving (Command -> Command -> Bool
    (Command -> Command -> Bool)
    -> (Command -> Command -> Bool) -> Eq Command
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Command -> Command -> Bool
    == :: Command -> Command -> Bool
    $c/= :: Command -> Command -> Bool
    /= :: Command -> Command -> Bool
    Eq, Arity -> Command -> ShowS
    [Command] -> ShowS
    Command -> String
    (Arity -> Command -> ShowS)
    -> (Command -> String) -> ([Command] -> ShowS) -> Show Command
    forall a.
    (Arity -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Arity -> Command -> ShowS
    showsPrec :: Arity -> Command -> ShowS
    $cshow :: Command -> String
    show :: Command -> String
    $cshowList :: [Command] -> ShowS
    showList :: [Command] -> ShowS
    Show)

    -- | The built-in name associated with a particular Kan operation.
    kanOpName :: KanOperation -> String
    kanOpName :: KanOperation -> String
    kanOpName TranspOp{} = PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    PrimTrans
    kanOpName HCompOp{}  = PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    PrimHComp

    -- | Our Kan operations are @transp@ and @hcomp@. The KanOperation
    -- record stores the data associated with a Kan operation on arbitrary
    -- types: A cofibration and an element of that type.
    data KanOperation
      -- | A transport problem consists of a cofibration, marking where the
      -- transport is constant, and a term to move from the fibre over i0 to
      -- the fibre over i1.
      = TranspOp
        { KanOperation -> Blocked (Arg Term)
    kanOpCofib :: Blocked (Arg Term)
          -- ^ When this cofibration holds, the transport must
          -- definitionally be the identity. This is handled generically by
          -- 'primTransHComp' but specific Kan operations may still need it.
        , KanOperation -> Arg Term
    kanOpBase :: Arg Term
          -- ^ This is the term in @A i0@ which we are transporting.
        }
      -- | A composition problem consists of a partial element and a base.
      -- Semantically, this is justified by the types being Kan fibrations,
      -- i.e., having the lifting property against trivial cofibrations.
      -- While the specified cofibration may not be trivial, (φ ∨ ~ r) for r
      -- ∉ φ is *always* a trivial cofibration.
      | HCompOp
        { kanOpCofib :: Blocked (Arg Term)
          -- ^ Extent of definition of the partial element we are lifting
          -- against.
        , KanOperation -> Arg Term
    kanOpSides :: Arg Term
          -- ^ The partial element itself
        , kanOpBase  :: Arg Term
          -- ^ The base.
        }

    -- | Are we looking at a family of things, or at a single thing?
    data FamilyOrNot a
      = IsFam { forall a. FamilyOrNot a -> a
    famThing :: a }
      | IsNot { famThing :: a }
      deriving (FamilyOrNot a -> FamilyOrNot a -> Bool
    (FamilyOrNot a -> FamilyOrNot a -> Bool)
    -> (FamilyOrNot a -> FamilyOrNot a -> Bool) -> Eq (FamilyOrNot a)
    forall a. Eq a => FamilyOrNot a -> FamilyOrNot a -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall a. Eq a => FamilyOrNot a -> FamilyOrNot a -> Bool
    == :: FamilyOrNot a -> FamilyOrNot a -> Bool
    $c/= :: forall a. Eq a => FamilyOrNot a -> FamilyOrNot a -> Bool
    /= :: FamilyOrNot a -> FamilyOrNot a -> Bool
    Eq,Arity -> FamilyOrNot a -> ShowS
    [FamilyOrNot a] -> ShowS
    FamilyOrNot a -> String
    (Arity -> FamilyOrNot a -> ShowS)
    -> (FamilyOrNot a -> String)
    -> ([FamilyOrNot a] -> ShowS)
    -> Show (FamilyOrNot a)
    forall a. Show a => Arity -> FamilyOrNot a -> ShowS
    forall a. Show a => [FamilyOrNot a] -> ShowS
    forall a. Show a => FamilyOrNot a -> String
    forall a.
    (Arity -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Arity -> FamilyOrNot a -> ShowS
    showsPrec :: Arity -> FamilyOrNot a -> ShowS
    $cshow :: forall a. Show a => FamilyOrNot a -> String
    show :: FamilyOrNot a -> String
    $cshowList :: forall a. Show a => [FamilyOrNot a] -> ShowS
    showList :: [FamilyOrNot a] -> ShowS
    Show,(forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b)
    -> (forall a b. a -> FamilyOrNot b -> FamilyOrNot a)
    -> Functor FamilyOrNot
    forall a b. a -> FamilyOrNot b -> FamilyOrNot a
    forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b
    fmap :: forall a b. (a -> b) -> FamilyOrNot a -> FamilyOrNot b
    $c<$ :: forall a b. a -> FamilyOrNot b -> FamilyOrNot a
    <$ :: forall a b. a -> FamilyOrNot b -> FamilyOrNot a
    Functor,(forall m. Monoid m => FamilyOrNot m -> m)
    -> (forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m)
    -> (forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m)
    -> (forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b)
    -> (forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b)
    -> (forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b)
    -> (forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b)
    -> (forall a. (a -> a -> a) -> FamilyOrNot a -> a)
    -> (forall a. (a -> a -> a) -> FamilyOrNot a -> a)
    -> (forall a. FamilyOrNot a -> [a])
    -> (forall a. FamilyOrNot a -> Bool)
    -> (forall a. FamilyOrNot a -> Arity)
    -> (forall a. Eq a => a -> FamilyOrNot a -> Bool)
    -> (forall a. Ord a => FamilyOrNot a -> a)
    -> (forall a. Ord a => FamilyOrNot a -> a)
    -> (forall a. Num a => FamilyOrNot a -> a)
    -> (forall a. Num a => FamilyOrNot a -> a)
    -> Foldable FamilyOrNot
    forall a. Eq a => a -> FamilyOrNot a -> Bool
    forall a. Num a => FamilyOrNot a -> a
    forall a. Ord a => FamilyOrNot a -> a
    forall m. Monoid m => FamilyOrNot m -> m
    forall a. FamilyOrNot a -> Bool
    forall a. FamilyOrNot a -> Arity
    forall a. FamilyOrNot a -> [a]
    forall a. (a -> a -> a) -> FamilyOrNot a -> a
    forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
    forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
    forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Arity)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => FamilyOrNot m -> m
    fold :: forall m. Monoid m => FamilyOrNot m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> FamilyOrNot a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> FamilyOrNot a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> FamilyOrNot a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
    foldr1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
    foldl1 :: forall a. (a -> a -> a) -> FamilyOrNot a -> a
    $ctoList :: forall a. FamilyOrNot a -> [a]
    toList :: forall a. FamilyOrNot a -> [a]
    $cnull :: forall a. FamilyOrNot a -> Bool
    null :: forall a. FamilyOrNot a -> Bool
    $clength :: forall a. FamilyOrNot a -> Arity
    length :: forall a. FamilyOrNot a -> Arity
    $celem :: forall a. Eq a => a -> FamilyOrNot a -> Bool
    elem :: forall a. Eq a => a -> FamilyOrNot a -> Bool
    $cmaximum :: forall a. Ord a => FamilyOrNot a -> a
    maximum :: forall a. Ord a => FamilyOrNot a -> a
    $cminimum :: forall a. Ord a => FamilyOrNot a -> a
    minimum :: forall a. Ord a => FamilyOrNot a -> a
    $csum :: forall a. Num a => FamilyOrNot a -> a
    sum :: forall a. Num a => FamilyOrNot a -> a
    $cproduct :: forall a. Num a => FamilyOrNot a -> a
    product :: forall a. Num a => FamilyOrNot a -> a
    Foldable,Functor FamilyOrNot
    Foldable FamilyOrNot
    (Functor FamilyOrNot, Foldable FamilyOrNot) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        FamilyOrNot (f a) -> f (FamilyOrNot a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        FamilyOrNot (m a) -> m (FamilyOrNot a))
    -> Traversable FamilyOrNot
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    FamilyOrNot (m a) -> m (FamilyOrNot a)
    forall (f :: * -> *) a.
    Applicative f =>
    FamilyOrNot (f a) -> f (FamilyOrNot a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    FamilyOrNot (f a) -> f (FamilyOrNot a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    FamilyOrNot (f a) -> f (FamilyOrNot a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    FamilyOrNot (m a) -> m (FamilyOrNot a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    FamilyOrNot (m a) -> m (FamilyOrNot a)
    Traversable)

    familyOrNot :: IsString p => FamilyOrNot a -> p
    familyOrNot :: forall p a. IsString p => FamilyOrNot a -> p
    familyOrNot (IsFam a
    x) = p
    "IsFam"
    familyOrNot (IsNot a
    x) = p
    "IsNot"

    instance Reduce a => Reduce (FamilyOrNot a) where
      reduceB' :: FamilyOrNot a -> ReduceM (Blocked (FamilyOrNot a))
    reduceB' FamilyOrNot a
    x = (Blocked' Term a -> Blocked' Term a)
    -> FamilyOrNot (Blocked' Term a) -> Blocked (FamilyOrNot a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
    traverse Blocked' Term a -> Blocked' Term a
    forall a. a -> a
    id (FamilyOrNot (Blocked' Term a) -> Blocked (FamilyOrNot a))
    -> ReduceM (FamilyOrNot (Blocked' Term a))
    -> ReduceM (Blocked (FamilyOrNot a))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (a -> ReduceM (Blocked' Term a))
    -> FamilyOrNot a -> ReduceM (FamilyOrNot (Blocked' Term a))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
    traverse a -> ReduceM (Blocked' Term a)
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' FamilyOrNot a
    x
      reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a)
    reduce' FamilyOrNot a
    x = (a -> ReduceM a) -> FamilyOrNot a -> ReduceM (FamilyOrNot a)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)
    traverse a -> ReduceM a
    forall t. Reduce t => t -> ReduceM t
    reduce' FamilyOrNot a
    x

    -- | For the Kan operations in @Glue@ and @hcomp {Type}@, we optimise
    -- evaluation a tiny bit by differentiating the term produced when
    -- evaluating a Kan operation by itself vs evaluating it under @unglue@.
    -- (See @headStop@ below.)
    data TermPosition
      = Head
      | Eliminated
      deriving (TermPosition -> TermPosition -> Bool
    (TermPosition -> TermPosition -> Bool)
    -> (TermPosition -> TermPosition -> Bool) -> Eq TermPosition
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: TermPosition -> TermPosition -> Bool
    == :: TermPosition -> TermPosition -> Bool
    $c/= :: TermPosition -> TermPosition -> Bool
    /= :: TermPosition -> TermPosition -> Bool
    Eq,Arity -> TermPosition -> ShowS
    [TermPosition] -> ShowS
    TermPosition -> String
    (Arity -> TermPosition -> ShowS)
    -> (TermPosition -> String)
    -> ([TermPosition] -> ShowS)
    -> Show TermPosition
    forall a.
    (Arity -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Arity -> TermPosition -> ShowS
    showsPrec :: Arity -> TermPosition -> ShowS
    $cshow :: TermPosition -> String
    show :: TermPosition -> String
    $cshowList :: [TermPosition] -> ShowS
    showList :: [TermPosition] -> ShowS
    Show)

    -- | Kan operations for the "unstable" type formers (@Glue@, @hcomp {Type}@) are
    -- computed "negatively": they never actually produce a @glue φ t a@ term. Instead,
    -- we block the computation unless such a term would reduce further, which happens
    -- in two cases:
    --
    -- * when the formula @φ@ is i1, in which case we reduce to @t@;
    -- * when we're under an @unglue@, i.e. in 'Eliminated' 'TermPosition', in which case
    --   we reduce to @a@.
    headStop :: PureTCM m => TermPosition -> m Term -> m Bool
    headStop :: forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
    headStop TermPosition
    tpos m Term
    phi
      | TermPosition
    Head <- TermPosition
    tpos = do
        phi <- Term -> m IntervalView
    forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
    intervalView (Term -> m IntervalView) -> m Term -> m IntervalView
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Term -> m Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m Term
    phi)
        return $ not $ isIOne phi
      | Bool
    otherwise = Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | Build a partial element. The type of the resulting partial element
    -- can depend on the computed extent, which we denote by @φ@ here. Note
    -- that @φ@ is the n-ary disjunction of all the @ψ@s.
    combineSys
      :: HasBuiltins m
      => NamesT m Term -- The level @l : Level@
      -> NamesT m Term -- The type @A : Partial φ (Type l)@.
      -> [(NamesT m Term, NamesT m Term)]
      -- ^ A list of @(ψ, PartialP ψ λ o → A (... o ...))@ mappings. Note
      -- that by definitional proof-irrelevance of @IsOne@, the actual
      -- injection can not matter here.
      -> NamesT m Term
    combineSys :: forall (m :: * -> *).
    HasBuiltins m =>
    NamesT m Term
    -> NamesT m Term
    -> [(NamesT m Term, NamesT m Term)]
    -> NamesT m Term
    combineSys NamesT m Term
    l NamesT m Term
    ty [(NamesT m Term, NamesT m Term)]
    xs = (Term, Term) -> Term
    forall a b. (a, b) -> b
    snd ((Term, Term) -> Term) -> NamesT m (Term, Term) -> NamesT m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT m Term
    -> NamesT m Term
    -> [(NamesT m Term, NamesT m Term)]
    -> NamesT m (Term, Term)
    forall (m :: * -> *).
    HasBuiltins m =>
    NamesT m Term
    -> NamesT m Term
    -> [(NamesT m Term, NamesT m Term)]
    -> NamesT m (Term, Term)
    combineSys' NamesT m Term
    l NamesT m Term
    ty [(NamesT m Term, NamesT m Term)]
    xs

    -- | Build a partial element, and compute its extent. See 'combineSys'
    -- for the details.
    combineSys'
      :: forall m. HasBuiltins m
      => NamesT m Term -- The level @l@
      -> NamesT m Term -- The type @A@
      -> [(NamesT m Term, NamesT m Term)]
      -> NamesT m (Term,Term)
    combineSys' :: forall (m :: * -> *).
    HasBuiltins m =>
    NamesT m Term
    -> NamesT m Term
    -> [(NamesT m Term, NamesT m Term)]
    -> NamesT m (Term, Term)
    combineSys' NamesT m Term
    l NamesT m Term
    ty [(NamesT m Term, NamesT m Term)]
    xs = do
      tPOr <- Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> Term) -> NamesT m (Maybe Term) -> NamesT m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> PrimitiveId -> NamesT m (Maybe Term)
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    a -> m (Maybe Term)
    getTerm' PrimitiveId
    builtinPOr
      tMax <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIMax
      iz <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIZero
      tEmpty <- fromMaybe __IMPOSSIBLE__ <$> getTerm' builtinIsOneEmpty

      let
        pOr NamesT m Term
    l NamesT m Term
    ty NamesT m Term
    phi NamesT m Term
    psi NamesT m Term
    u0 NamesT m Term
    u1 = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tPOr
          NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT m Term
    l NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    phi NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    psi NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam String
    "o" (\ NamesT m Term
    _ -> NamesT m Term
    ty)
          NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    u0 NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    u1

        -- In one pass, compute the disjunction of all the cofibrations and
        -- compute the primPOr expression.
        combine :: [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)
        combine [] = (Term
    iz,) (Term -> (Term, Term)) -> NamesT m Term -> NamesT m (Term, Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tEmpty NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT m Term
    l NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam String
    "o" (\ NamesT m Term
    _ -> NamesT m Term
    ty))
        combine [(NamesT m Term
    psi, NamesT m Term
    u)] = (,) (Term -> Term -> (Term, Term))
    -> NamesT m Term -> NamesT m (Term -> (Term, Term))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT m Term
    psi NamesT m (Term -> (Term, Term))
    -> NamesT m Term -> NamesT m (Term, Term)
    forall a b. NamesT m (a -> b) -> NamesT m a -> NamesT m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> NamesT m Term
    u
        combine ((NamesT m Term
    psi, NamesT m Term
    u):[(NamesT m Term, NamesT m Term)]
    xs) = do
          (phi, c) <- [(NamesT m Term, NamesT m Term)] -> NamesT m (Term, Term)
    combine [(NamesT m Term, NamesT m Term)]
    xs
          (,) <$> imax psi (pure phi) <*> pOr l ty psi (pure phi) u (pure c)
      combine xs

    -- | Helper function for constructing the type of fibres of a function
    -- over a given point.
    fiber
      :: (HasBuiltins m, HasConstInfo m)
      => NamesT m Term -- @la : Level@
      -> NamesT m Term -- @lb : Level@
      -> NamesT m Term -- @A : Type la@
      -> NamesT m Term -- @B : Type lb@
      -> NamesT m Term -- @f : A → B@
      -> NamesT m Term -- @x : B@
      -> NamesT m Term -- @Σ[ x ∈ A ] (f a ≡ x)@
    fiber :: forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m) =>
    NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    fiber NamesT m Term
    la NamesT m Term
    lb NamesT m Term
    bA NamesT m Term
    bB NamesT m Term
    f NamesT m Term
    b = do
      tPath <- String -> BuiltinId -> NamesT m Term
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    String -> a -> m Term
    getTerm String
    "fiber" BuiltinId
    builtinPath
      kit <- fromMaybe __IMPOSSIBLE__ <$> getSigmaKit
      pure (Def (sigmaName kit) [])
        <#> la <#> lb
        <@> bA
        <@> lam "a" (\ NamesT m Term
    a -> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tPath NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT m Term
    lb NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT m Term
    bB NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT m Term
    f NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    a) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    b)

    -- | Helper function for constructing the filler of a given composition
    -- problem.
    hfill
      :: (HasBuiltins m, HasConstInfo m)
      => NamesT m Term -- @la : Level@
      -> NamesT m Term -- @A : Type la@
      -> NamesT m Term -- @φ : I@. Cofibration
      -> NamesT m Term -- @u : Partial φ A@.
      -> NamesT m Term -- @u0 : A@. Must agree with @u@ on @φ@
      -> NamesT m Term -- @i : I@. Position along the cube.
      -> NamesT m Term
    hfill :: forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m) =>
    NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    hfill NamesT m Term
    la NamesT m Term
    bA NamesT m Term
    phi NamesT m Term
    u NamesT m Term
    u0 NamesT m Term
    i = do
      tHComp <- String -> PrimitiveId -> NamesT m Term
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    String -> a -> m Term
    getTerm String
    "hfill" PrimitiveId
    builtinHComp
      pure tHComp <#> la <#> bA <#> (imax phi (ineg i))
        <@> lam "j" (\ NamesT m Term
    j -> NamesT m Term
    -> NamesT m Term
    -> [(NamesT m Term, NamesT m Term)]
    -> NamesT m Term
    forall (m :: * -> *).
    HasBuiltins m =>
    NamesT m Term
    -> NamesT m Term
    -> [(NamesT m Term, NamesT m Term)]
    -> NamesT m Term
    combineSys NamesT m Term
    la NamesT m Term
    bA
            [ (NamesT m Term
    phi,    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam String
    "o" (\NamesT m Term
    o -> NamesT m Term
    u NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
    imin NamesT m Term
    i NamesT m Term
    j) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <..> NamesT m Term
    o))
            , (NamesT m Term -> NamesT m Term
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg NamesT m Term
    i, String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam String
    "o" (\NamesT m Term
    _ -> NamesT m Term
    u0))
            ])
        <@> u0

    {-# SPECIALIZE decomposeInterval :: Term -> TCM [(IntMap Bool, [Term])] #-}
    -- | Decompose an interval expression @i : I@ as in
    -- 'decomposeInterval'', but discard any inconsistent mappings.
    decomposeInterval :: HasBuiltins m => Term -> m [(IntMap Bool, [Term])]
    decomposeInterval :: forall (m :: * -> *).
    HasBuiltins m =>
    Term -> m [(IntMap Bool, [Term])]
    decomposeInterval Term
    t = do
      Term -> m [(IntMap BoolSet, [Term])]
    forall (m :: * -> *).
    HasBuiltins m =>
    Term -> m [(IntMap BoolSet, [Term])]
    decomposeInterval' Term
    t m [(IntMap BoolSet, [Term])]
    -> ([(IntMap BoolSet, [Term])] -> [(IntMap Bool, [Term])])
    -> m [(IntMap Bool, [Term])]
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \[(IntMap BoolSet, [Term])]
    xs ->
        [ (IntMap Bool
    bm, [Term]
    ts) | (IntMap BoolSet
    bsm, [Term]
    ts) <- [(IntMap BoolSet, [Term])]
    xs, IntMap Bool
    bm <- Maybe (IntMap Bool) -> [IntMap Bool]
    forall a. Maybe a -> [a]
    maybeToList (Maybe (IntMap Bool) -> [IntMap Bool])
    -> Maybe (IntMap Bool) -> [IntMap Bool]
    forall a b. (a -> b) -> a -> b
    $ (BoolSet -> Maybe Bool) -> IntMap BoolSet -> Maybe (IntMap Bool)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> IntMap a -> f (IntMap b)
    traverse BoolSet -> Maybe Bool
    BoolSet.toSingleton IntMap BoolSet
    bsm ]

    {-# SPECIALIZE decomposeInterval' :: Term -> TCM [(IntMap BoolSet, [Term])] #-}
    -- | Decompose an interval expression @φ : I@ into a set of possible
    -- assignments for the variables mentioned in @φ@, together any leftover
    -- neutral terms that could not be put into 'IntervalView' form.
    decomposeInterval' :: HasBuiltins m => Term -> m [(IntMap BoolSet, [Term])]
    decomposeInterval' :: forall (m :: * -> *).
    HasBuiltins m =>
    Term -> m [(IntMap BoolSet, [Term])]
    decomposeInterval' Term
    t = do
      view   <- m (Term -> IntervalView)
    forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
    intervalView'
      unview <- intervalUnview'
      let
        f :: IntervalView -> [[Either (Int,Bool) Term]]
        -- TODO handle primIMinDep
        -- TODO? handle forall
        f IntervalView
    IZero = [[Either (Arity, Bool) Term]]
    forall a. [a]
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero     -- No assignments are possible
        f IntervalView
    IOne  = [Either (Arity, Bool) Term] -> [[Either (Arity, Bool) Term]]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] -- No assignments are necessary
        -- Take the cartesian product
        f (IMin Arg Term
    x Arg Term
    y) = do
          xs <- (IntervalView -> [[Either (Arity, Bool) Term]]
    f (IntervalView -> [[Either (Arity, Bool) Term]])
    -> (Arg Term -> IntervalView)
    -> Arg Term
    -> [[Either (Arity, Bool) Term]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> IntervalView
    view (Term -> IntervalView)
    -> (Arg Term -> Term) -> Arg Term -> IntervalView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) Arg Term
    x
          ys <- (f . view . unArg) y
          return (xs ++ ys)
        -- Take the union
        f (IMax Arg Term
    x Arg Term
    y) = [[[Either (Arity, Bool) Term]]] -> [[Either (Arity, Bool) Term]]
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, MonadPlus m) =>
    t (m a) -> m a
    msum ([[[Either (Arity, Bool) Term]]] -> [[Either (Arity, Bool) Term]])
    -> [[[Either (Arity, Bool) Term]]] -> [[Either (Arity, Bool) Term]]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> [[Either (Arity, Bool) Term]])
    -> [Arg Term] -> [[[Either (Arity, Bool) Term]]]
    forall a b. (a -> b) -> [a] -> [b]
    map (IntervalView -> [[Either (Arity, Bool) Term]]
    f (IntervalView -> [[Either (Arity, Bool) Term]])
    -> (Arg Term -> IntervalView)
    -> Arg Term
    -> [[Either (Arity, Bool) Term]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> IntervalView
    view (Term -> IntervalView)
    -> (Arg Term -> Term) -> Arg Term -> IntervalView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) [Arg Term
    x,Arg Term
    y]
        -- Invert the possible assignments and negate the neutrals
        f (INeg Arg Term
    x) =
          (Either (Arity, Bool) Term -> Either (Arity, Bool) Term)
    -> [Either (Arity, Bool) Term] -> [Either (Arity, Bool) Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (((Arity, Bool) -> Either (Arity, Bool) Term)
    -> (Term -> Either (Arity, Bool) Term)
    -> Either (Arity, Bool) Term
    -> Either (Arity, Bool) Term
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (\ (Arity
    x,Bool
    y) -> (Arity, Bool) -> Either (Arity, Bool) Term
    forall a b. a -> Either a b
    Left (Arity
    x,Bool -> Bool
    not Bool
    y)) (Term -> Either (Arity, Bool) Term
    forall a b. b -> Either a b
    Right (Term -> Either (Arity, Bool) Term)
    -> (Term -> Term) -> Term -> Either (Arity, Bool) Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . IntervalView -> Term
    unview (IntervalView -> Term) -> (Term -> IntervalView) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> IntervalView
    INeg (Arg Term -> IntervalView)
    -> (Term -> Arg Term) -> Term -> IntervalView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Arg Term
    forall e. e -> Arg e
    argN))
            ([Either (Arity, Bool) Term] -> [Either (Arity, Bool) Term])
    -> [[Either (Arity, Bool) Term]] -> [[Either (Arity, Bool) Term]]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (IntervalView -> [[Either (Arity, Bool) Term]]
    f (IntervalView -> [[Either (Arity, Bool) Term]])
    -> (Arg Term -> IntervalView)
    -> Arg Term
    -> [[Either (Arity, Bool) Term]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> IntervalView
    view (Term -> IntervalView)
    -> (Arg Term -> Term) -> Arg Term -> IntervalView
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) Arg Term
    x
        f (OTerm (Var Arity
    i [])) = [Either (Arity, Bool) Term] -> [[Either (Arity, Bool) Term]]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [(Arity, Bool) -> Either (Arity, Bool) Term
    forall a b. a -> Either a b
    Left (Arity
    i,Bool
    True)]
        f (OTerm Term
    t)          = [Either (Arity, Bool) Term] -> [[Either (Arity, Bool) Term]]
    forall a. a -> [a]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Term -> Either (Arity, Bool) Term
    forall a b. b -> Either a b
    Right Term
    t]

      return [ (bsm, ts)
             | xs <- f (view t)
             , let (bs,ts) = partitionEithers xs
             , let bsm     = (BoolSet -> BoolSet -> BoolSet)
    -> [(Arity, BoolSet)] -> IntMap BoolSet
    forall a. (a -> a -> a) -> [(Arity, a)] -> IntMap a
    IntMap.fromListWith BoolSet -> BoolSet -> BoolSet
    BoolSet.union ([(Arity, BoolSet)] -> IntMap BoolSet)
    -> [(Arity, BoolSet)] -> IntMap BoolSet
    forall a b. (a -> b) -> a -> b
    $ ((Arity, Bool) -> (Arity, BoolSet))
    -> [(Arity, Bool)] -> [(Arity, BoolSet)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Bool -> BoolSet) -> (Arity, Bool) -> (Arity, BoolSet)
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second Bool -> BoolSet
    BoolSet.singleton) [(Arity, Bool)]
    bs
             ]

    reduce2Lam :: Term -> ReduceM (Blocked Term)
    reduce2Lam :: Term -> ReduceM (Blocked Term)
    reduce2Lam Term
    t = do
      t <- Term -> ReduceM Term
    forall t. Reduce t => t -> ReduceM t
    reduce' Term
    t
      case lam2Abs relevant t of
        Abs Term
    t -> Abs Term
    -> (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term)
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Abs a -> (a -> m b) -> m b
    underAbstraction_ Abs Term
    t ((Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term))
    -> (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term)
    forall a b. (a -> b) -> a -> b
    $ \ Term
    t -> do
          t <- Term -> ReduceM Term
    forall t. Reduce t => t -> ReduceM t
    reduce' Term
    t
          case lam2Abs irrelevant t of
            Abs Term
    t -> Abs Term
    -> (Term -> ReduceM (Blocked Term)) -> ReduceM (Blocked Term)
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Abs a -> (a -> m b) -> m b
    underAbstraction_ Abs Term
    t Term -> ReduceM (Blocked Term)
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB'
      where
        lam2Abs :: Relevance -> Term -> Abs Term
    lam2Abs Relevance
    rel (Lam ArgInfo
    _ Abs Term
    t) = Abs Term -> Term
    forall a. Subst a => Abs a -> a
    absBody Abs Term
    t Term -> Abs Term -> Abs Term
    forall a b. a -> Abs b -> Abs a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Abs Term
    t
        lam2Abs Relevance
    rel Term
    t         = String -> Term -> Abs Term
    forall a. String -> a -> Abs a
    Abs String
    "y" (Arity -> Term -> Term
    forall a. Subst a => Arity -> a -> a
    raise Arity
    1 Term
    t Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Relevance -> Arg Term -> Arg Term
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    rel (Arg Term -> Arg Term) -> Arg Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Arg Term
    forall e. e -> Arg e
    argN (Term -> Arg Term) -> Term -> Arg Term
    forall a b. (a -> b) -> a -> b
    $ Arity -> Term
    var Arity
    0])

    -- | Are we looking at an application of the 'Sub' type? If so, return:
    -- * The type we're an extension of
    -- * The extent
    -- * The partial element.
    isCubicalSubtype :: PureTCM m => Type -> m (Maybe (Term, Term, Term, Term))
    isCubicalSubtype :: forall (m :: * -> *).
    PureTCM m =>
    Type -> m (Maybe (Term, Term, Term, Term))
    isCubicalSubtype Type
    t = do
      t <- Type -> m Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    t
      msub <- getBuiltinName' builtinSub
      case unEl t of
        Def QName
    q Elims
    es | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    msub, Just (Arg Term
    level:Arg Term
    typ:Arg Term
    phi:Arg Term
    ext:[Arg Term]
    _) <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es -> do
          Maybe (Term, Term, Term, Term)
    -> m (Maybe (Term, Term, Term, Term))
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ((Term, Term, Term, Term) -> Maybe (Term, Term, Term, Term)
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    level, Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    typ, Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    phi, Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    ext))
        Term
    _ -> Maybe (Term, Term, Term, Term)
    -> m (Maybe (Term, Term, Term, Term))
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe (Term, Term, Term, Term)
    forall a. Maybe a
    Nothing