    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Primitive.Cubical.HCompU
      ( doHCompUKanOp
      , prim_glueU'
      , prim_unglueU'
      )
      where

    import Control.Monad

    import Agda.Syntax.Common
      ( Cubical(..), Arg(..)
      , ProjOrigin(..)
      )
    import Agda.Syntax.Internal

    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Monad.Pure

    import Agda.TypeChecking.Names
      ( runNamesT, runNames, cl, lam, open, ilam )
    import Agda.TypeChecking.Primitive.Base
      ( (-->), nPi', pPi', hPi', el, el', el's, (<@>), (<@@>), (<#>), argN, (<..>)
      , SigmaKit(..), getSigmaKit
      )
    import Agda.TypeChecking.Primitive.Cubical.Glue
    import Agda.TypeChecking.Primitive.Cubical.Base
    import Agda.TypeChecking.Reduce
      ( reduceB', reduceB )
    import Agda.TypeChecking.Substitute
      ( absBody, apply, sort, applyE )

    import Agda.Utils.Functor
    import Agda.Utils.Maybe
    import Agda.Utils.Monad

    import Agda.Utils.Impossible (__IMPOSSIBLE__)

    -- | Perform the Kan operations for an @hcomp {A = Type} {φ} u u0@ type.
    doHCompUKanOp
      :: forall m. PureTCM m
      => KanOperation
      -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
      -> TermPosition
      -> m (Maybe Term)

    -- TODO (Amy, 2022-08-17): This is literally the same algorithm as
    -- doGlueKanOp, but specialised for using transport as the equivalence.
    -- Can we deduplicate them?
    doHCompUKanOp :: forall (m :: * -> *).
    PureTCM m =>
    KanOperation
    -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
    -> TermPosition
    -> m (Maybe Term)
    doHCompUKanOp (HCompOp Blocked (Arg Term)
    psi Arg Term
    u Arg Term
    u0) (IsNot (Arg Term
    la, Arg Term
    phi, Arg Term
    bT, Arg Term
    bA)) TermPosition
    tpos = do
      let getTermLocal :: IsBuiltin a => a -> m Term
          getTermLocal :: forall a. IsBuiltin a => a -> m Term
    getTermLocal = [Char] -> a -> m Term
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    [Char] -> a -> m Term
    getTerm ([Char] -> a -> m Term) -> [Char] -> a -> m Term
    forall a b. (a -> b) -> a -> b
    $ PrimitiveId -> [Char]
    forall a. IsBuiltin a => a -> [Char]
    getBuiltinId PrimitiveId
    builtinHComp [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ PrimitiveId -> [Char]
    forall a. IsBuiltin a => a -> [Char]
    getBuiltinId PrimitiveId
    builtinHComp [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " of Set"
      io       <- BuiltinId -> m Term
    forall a. IsBuiltin a => a -> m Term
    getTermLocal BuiltinId
    builtinIOne
      iz       <- getTermLocal builtinIZero
      tHComp   <- getTermLocal builtinHComp
      tTransp  <- getTermLocal builtinTrans
      tunglue  <- getTermLocal builtin_unglueU
      tLSuc    <- getTermLocal builtinLevelSuc
      tSubIn   <- getTermLocal builtinSubIn
      tItIsOne <- getTermLocal builtinItIsOne
      runNamesT [] $ do
        psi <- open . unArg $ ignoreBlocking psi
        u   <- open . unArg $ u
        u0  <- open . unArg $ u0
        la  <- open . unArg $ la
        phi <- open . unArg $ phi
        bT  <- open . unArg $ bT
        bA  <- open . unArg $ bA

        ifM (headStop tpos phi) (return Nothing) $ Just <$> do

        let
          transp NamesT m Term
    la NamesT m Term -> NamesT m Term
    bA NamesT m Term
    a0 = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tTransp NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "i" (NamesT m Term -> NamesT m Term -> NamesT m Term
    forall a b. a -> b -> a
    const NamesT m Term
    la) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "i" NamesT m Term -> NamesT m Term
    bA NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    iz NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    a0
          tf NamesT m Term
    i NamesT m Term
    o = NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    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
    bT NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io 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
    psi NamesT m Term
    u NamesT m Term
    u0 NamesT m Term
    i

          bAS = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tSubIn NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tLSuc NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    la) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Sort -> Term
    Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Term) -> NamesT m Term -> NamesT m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT m Term
    la) 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
    bA
          unglue NamesT m Term
    g = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tunglue NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT m Term
    la 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
    bT NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT m Term
    bAS NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    g

          a1 = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tHComp NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT m Term
    la NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT m Term
    bA 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
    imax NamesT m Term
    psi NamesT m Term
    phi)
            NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "i" (\NamesT m Term
    i -> 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
    psi, [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "o" (\NamesT m Term
    o -> NamesT m Term -> NamesT m Term
    unglue (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
    i 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
    phi, [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "o" (\ NamesT m Term
    o -> NamesT m Term
    -> (NamesT m Term -> NamesT m Term)
    -> NamesT m Term
    -> NamesT m Term
    transp NamesT m Term
    la (\NamesT m Term
    i -> NamesT m Term
    bT 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
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg NamesT m Term
    i) 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 -> NamesT m Term
    tf NamesT m Term
    i NamesT m Term
    o)))
                ])
            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
    unglue NamesT m Term
    u0

          t1 = NamesT m Term -> NamesT m Term -> NamesT m Term
    tf (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io)

        -- pure tglue <#> la <#> phi <#> bT <#> bAS <@> (ilam "o" $ \ o -> t1 o) <@> a1
        case tpos of
          TermPosition
    Eliminated -> NamesT m Term
    a1
          TermPosition
    Head       -> NamesT m Term -> NamesT m Term
    t1 (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tItIsOne)

    doHCompUKanOp (TranspOp Blocked (Arg Term)
    psi Arg Term
    u0) (IsFam (Arg Term
    la, Arg Term
    phi, Arg Term
    bT, Arg Term
    bA)) TermPosition
    tpos = do
      let
        localUse :: [Char]
    localUse = PrimitiveId -> [Char]
    forall a. IsBuiltin a => a -> [Char]
    getBuiltinId PrimitiveId
    builtinTrans [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " for " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ PrimitiveId -> [Char]
    forall a. IsBuiltin a => a -> [Char]
    getBuiltinId PrimitiveId
    builtinHComp [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " of Set"
        getTermLocal :: IsBuiltin a => a -> m Term
        getTermLocal :: forall a. IsBuiltin a => a -> m Term
    getTermLocal = [Char] -> a -> m Term
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    [Char] -> a -> m Term
    getTerm [Char]
    localUse
      tPOr <- PrimitiveId -> m Term
    forall a. IsBuiltin a => a -> m Term
    getTermLocal PrimitiveId
    builtinPOr
      tIMax <- getTermLocal builtinIMax
      tIMin <- getTermLocal builtinIMin
      tINeg <- getTermLocal builtinINeg
      tHComp <- getTermLocal builtinHComp
      tTrans <- getTermLocal builtinTrans
      tTranspProof <- getTermLocal builtinTranspProof
      tSubIn <- getTermLocal builtinSubIn
      tForall  <- getTermLocal builtinFaceForall
      io      <- getTermLocal builtinIOne
      iz      <- getTermLocal builtinIZero
      tLSuc   <- getTermLocal builtinLevelSuc
      tPath   <- getTermLocal builtinPath
      tItIsOne   <- getTermLocal builtinItIsOne
      kit <- fromMaybe __IMPOSSIBLE__ <$> getSigmaKit
      runNamesT [] $ do
        -- Helper definitions we'll use:
        gcomp <- mkGComp localUse

        let
          transp NamesT m Term
    la NamesT m Term -> NamesT m Term
    bA NamesT m Term
    a0 = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tTrans NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "i" (NamesT m Term -> NamesT m Term -> NamesT m Term
    forall a b. a -> b -> a
    const NamesT m Term
    la) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "i" NamesT m Term -> NamesT m Term
    bA NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    iz NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    a0
          transpFill NamesT m Term
    la NamesT m Term
    bA NamesT m Term
    phi NamesT m Term
    u0 NamesT m Term
    i = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tTrans
            NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "j" (\ NamesT m Term
    j -> NamesT m Term
    la 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
    <@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "j" (\ NamesT m Term
    j -> NamesT m Term
    bA 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 -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
    imax NamesT m Term
    phi (NamesT m Term -> NamesT m Term
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg NamesT m Term
    i))
            NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    u0

        psi <- open . unArg . ignoreBlocking $ psi
        u0  <- open . unArg $ u0

        let lami = Term -> NamesT m (NamesT m Term)
    forall (m :: * -> *) a.
    (Monad m, Subst a) =>
    a -> NamesT m (NamesT m a)
    open (Term -> NamesT m (NamesT m Term))
    -> (Arg Term -> Term) -> Arg Term -> NamesT m (NamesT m Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Names -> NamesT Identity Term -> Term
    forall a. Names -> NamesT Identity a -> a
    runNames [] (NamesT Identity Term -> Term)
    -> (Arg Term -> NamesT Identity Term) -> Arg Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char]
    -> (NamesT Identity Term -> NamesT Identity Term)
    -> NamesT Identity Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "i" ((NamesT Identity Term -> NamesT Identity Term)
     -> NamesT Identity Term)
    -> (Arg Term -> NamesT Identity Term -> NamesT Identity Term)
    -> Arg Term
    -> NamesT Identity Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamesT Identity Term
    -> NamesT Identity Term -> NamesT Identity Term
    forall a b. a -> b -> a
    const (NamesT Identity Term
     -> NamesT Identity Term -> NamesT Identity Term)
    -> (Arg Term -> NamesT Identity Term)
    -> Arg Term
    -> NamesT Identity Term
    -> NamesT Identity Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> NamesT Identity Term
    forall a. a -> NamesT Identity a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> NamesT Identity Term)
    -> (Arg Term -> Term) -> Arg Term -> NamesT Identity Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg
        la  <- lami la
        phi <- lami phi
        bT  <- lami bT
        bA  <- lami bA

        -- Andreas, 2022-03-25, issue #5838.
        -- Port the fix of @unglueTranspGlue@ and @doGlueKanOp DoTransp@
        -- also to @doHCompUKanOp DoTransp@, as suggested by Tom Jack and Anders Mörtberg.
        -- We define @unglue_u0 i@ that is first used with @i@ and then with @i0@.
        -- The original code used it only with @i0@.
        tunglue <- cl $ getTermLocal builtin_unglueU
        let
          bAS NamesT m Term
    i = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tSubIn
            NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tLSuc NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT m Term
    la NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i)) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Sort -> Term
    Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Term) -> NamesT m Term -> NamesT m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (NamesT m Term
    la NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i)) 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
    i)
            NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT m Term
    bA NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i)
          unglue_u0 NamesT m Term
    i = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tunglue
            NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT m Term
    la NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i) 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
    i) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT m Term
    bT NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i)
            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
    bAS NamesT m Term
    i NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    u0

        ifM (headStop tpos (phi <@> pure io)) (return Nothing) $ Just <$> do

        let
          tf NamesT m Term
    i NamesT m Term
    o = NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    transpFill NamesT m Term
    la ([Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "i" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
    -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT m Term
    i -> NamesT m Term
    bT NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io 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
    psi NamesT m Term
    u0 NamesT m Term
    i
          t1 NamesT m Term
    o   = NamesT m Term -> NamesT m Term -> NamesT m Term
    tf (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) NamesT m Term
    o

          -- compute "forall. phi"
          forallphi = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tForall NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    phi

          -- a1 with gcomp
          a1 = NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    -> NamesT m Term
    gcomp NamesT m Term
    la NamesT m Term
    bA (NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
    imax NamesT m Term
    psi NamesT m Term
    forallphi)
            ([Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "i" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
    -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ \ NamesT m Term
    i -> 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 -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i) (NamesT m Term
    bA NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i)
              [ (NamesT m Term
    psi,       [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
    -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ \NamesT m Term
    _ -> NamesT m Term -> NamesT m Term
    unglue_u0 NamesT m Term
    i)
              , (NamesT m Term
    forallphi, [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "o" (\NamesT m Term
    o -> NamesT m Term
    -> (NamesT m Term -> NamesT m Term)
    -> NamesT m Term
    -> NamesT m Term
    transp (NamesT m Term
    la NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i) (\NamesT m Term
    j -> NamesT m Term
    bT NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i 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
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg 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 -> NamesT m Term
    tf NamesT m Term
    i NamesT m Term
    o)))
              ])
              (NamesT m Term -> NamesT m Term
    unglue_u0 (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    iz))

          w NamesT m Term
    i NamesT m Term
    o = [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "x" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
    -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ NamesT m Term
    -> (NamesT m Term -> NamesT m Term)
    -> NamesT m Term
    -> NamesT m Term
    transp (NamesT m Term
    la NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i) (\NamesT m Term
    j -> NamesT m Term
    bT NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    i 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
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg 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)

          pt NamesT m Term
    o = -- o : [ φ 1 ]
            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 -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) (NamesT m Term
    bT NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io 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
    psi       , [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
    -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ \NamesT m Term
    _ -> NamesT m Term
    u0)
              , (NamesT m Term
    forallphi , [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
    -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ \NamesT m Term
    o -> NamesT m Term -> NamesT m Term
    t1 NamesT m Term
    o)
              ]

          -- "ghcomp" is implemented in the proof of tTranspProof
          -- (see src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda)
          t1'alpha NamesT m Term
    o = -- o : [ φ 1 ]
             Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tTranspProof
              NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT m Term
    la NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "i" (\NamesT m Term
    i -> NamesT m Term
    bT NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io 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
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg NamesT m Term
    i 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 -> 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
    imax NamesT m Term
    psi NamesT m Term
    forallphi
              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
    pt NamesT m Term
    o
              NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tSubIn NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT m Term
    la NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT m Term
    bA NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) 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
    imax NamesT m Term
    psi NamesT m Term
    forallphi
                    NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    a1)

          -- TODO: optimize?
          t1' NamesT m Term
    o   = NamesT m Term -> NamesT m Term
    t1'alpha NamesT m Term
    o NamesT m Term -> (Term -> Term) -> NamesT m Term
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> (Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem (SigmaKit -> QName
    sigmaFst SigmaKit
    kit)])
          alpha NamesT m Term
    o = NamesT m Term -> NamesT m Term
    t1'alpha NamesT m Term
    o NamesT m Term -> (Term -> Term) -> NamesT m Term
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> (Term -> Elims -> Term
    forall t. Apply t => t -> Elims -> t
    `applyE` [ProjOrigin -> QName -> Elim' Term
    forall a. ProjOrigin -> QName -> Elim' a
    Proj ProjOrigin
    ProjSystem (SigmaKit -> QName
    sigmaSnd SigmaKit
    kit)])
          a1' = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tHComp NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT m Term
    la NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT m Term
    bA NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io)
            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
    imax (NamesT m Term
    phi NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) NamesT m Term
    psi
            NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam [Char]
    "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 -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) (NamesT m Term
    bA NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io)
              [ (NamesT m Term
    phi NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io, [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
    -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ \NamesT m Term
    o -> NamesT m Term -> NamesT m Term
    alpha NamesT m Term
    o NamesT m Term
    -> (NamesT m Term, NamesT m Term, NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Applicative m =>
    m Term -> (m Term, m Term, m Term) -> m Term
    <@@> (NamesT m Term -> NamesT m Term -> NamesT m Term
    w (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    io) NamesT m Term
    o 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
    t1' NamesT m Term
    o, NamesT m Term
    a1, NamesT m Term
    j))
              , (NamesT m Term
    psi,             [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    ilam [Char]
    "o" ((NamesT m Term -> NamesT m Term) -> NamesT m Term)
    -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall a b. (a -> b) -> a -> b
    $ \NamesT m Term
    o -> NamesT m Term
    a1)
              ])
            NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    a1

        -- glue1 (ilam "o" t1') a1'
        case tpos of
          TermPosition
    Eliminated -> NamesT m Term
    a1'
          TermPosition
    Head       -> NamesT m Term -> NamesT m Term
    t1' (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tItIsOne)
    doHCompUKanOp KanOperation
    _ FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
    _ TermPosition
    _ = m (Maybe Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | The implementation of 'prim_glueU', the introduction form for
    -- @hcomp@ types.
    prim_glueU' :: TCM PrimitiveImpl
    prim_glueU' :: TCM PrimitiveImpl
    prim_glueU' = do
    -- TODO (Amy, 2022-08-17): Same thing about duplicated code with Glue
    -- applies here.
      Cubical -> TCM ()
    requireCubical Cubical
    CErased
      t <- Names -> NamesT (TCMT IO) Type -> TCMT IO Type
    forall (m :: * -> *) a. Names -> NamesT m a -> m a
    runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
    -> NamesT (TCMT IO) Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $
           [Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' [Char]
    "la" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevel) (\ NamesT (TCMT IO) Term
    la ->
           [Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' [Char]
    "φ" NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    φ ->
           [Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' [Char]
    "T" ([Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' [Char]
    "i" NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    _ -> [Char]
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    [Char]
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' [Char]
    "o" NamesT (TCMT IO) Term
    φ ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    o -> Sort -> Type
    sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Term
    la) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    t ->
           [Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' [Char]
    "A" (NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el's (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    la) (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSub NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (Sort -> Term
    Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    φ NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT (TCMT IO) Term
    t NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    a -> do
           let bA :: NamesT (TCMT IO) Term
    bA = (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSubOut NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Sort -> Term
    Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT (TCMT IO) Term
    φ NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT (TCMT IO) Term
    t NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    a)
           [Char]
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    [Char]
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' [Char]
    "o" NamesT (TCMT IO) Term
    φ (\ NamesT (TCMT IO) Term
    o -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' NamesT (TCMT IO) Term
    la (NamesT (TCMT IO) Term
    t NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <..> NamesT (TCMT IO) Term
    o))
             NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> (NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' NamesT (TCMT IO) Term
    la NamesT (TCMT IO) Term
    bA)
             NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' NamesT (TCMT IO) Term
    la (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primHComp NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Sort -> Term
    Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT (TCMT IO) Term
    φ NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    t NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    bA))
      view <- intervalView'
      one <- primItIsOne
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \[Arg Term]
    ts ->
        case [Arg Term]
    ts of
          [Arg Term
    la,Arg Term
    phi,Arg Term
    bT,Arg Term
    bA,Arg Term
    t,Arg Term
    a] -> do
           sphi <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    phi
           case view $ unArg $ ignoreBlocking $ sphi of
             IntervalView
    IOne -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t Term -> [Arg Term] -> Term
    forall t. Apply t => t -> [Arg Term] -> t
    `apply` [Term -> Arg Term
    forall e. e -> Arg e
    argN Term
    one]
             IntervalView
    _    -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall no yes. no -> Reduced no yes
    NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
    -> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> MaybeReduced (Arg Term))
    -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced [Arg Term
    la] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> MaybeReduced (Arg Term))
    -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced [Arg Term
    bT,Arg Term
    bA,Arg Term
    t,Arg Term
    a])
          [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | The implementation of 'prim_unglueU', the elimination form for
    -- @hcomp@ types.
    prim_unglueU' :: TCM PrimitiveImpl
    prim_unglueU' :: TCM PrimitiveImpl
    prim_unglueU' = do
    -- TODO (Amy, 2022-08-17): Same thing about duplicated code with Glue
    -- applies here.
      Cubical -> TCM ()
    requireCubical Cubical
    CErased
      t <- Names -> NamesT (TCMT IO) Type -> TCMT IO Type
    forall (m :: * -> *) a. Names -> NamesT m a -> m a
    runNamesT [] (NamesT (TCMT IO) Type -> TCMT IO Type)
    -> NamesT (TCMT IO) Type -> TCMT IO Type
    forall a b. (a -> b) -> a -> b
    $
           [Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' [Char]
    "la" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Functor m => m Term -> m Type
    el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevel) (\ NamesT (TCMT IO) Term
    la ->
           [Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' [Char]
    "φ" NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    φ ->
           [Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' [Char]
    "T" ([Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' [Char]
    "i" NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Type
    primIntervalType ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    _ -> [Char]
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    [Char]
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' [Char]
    "o" NamesT (TCMT IO) Term
    φ ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    o -> Sort -> Type
    sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Term
    la) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    t ->
           [Char]
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    [Char]
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' [Char]
    "A" (NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el's (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    la) (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSub NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (Sort -> Term
    Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    φ NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT (TCMT IO) Term
    t NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
     -> NamesT (TCMT IO) Type)
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall a b. (a -> b) -> a -> b
    $ \ NamesT (TCMT IO) Term
    a -> do
           let bA :: NamesT (TCMT IO) Term
    bA = (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSubOut NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Sort -> Term
    Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT (TCMT IO) Term
    φ NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (NamesT (TCMT IO) Term
    t NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    a)
           NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' NamesT (TCMT IO) Term
    la (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primHComp NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (TCMT IO Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *) a. Monad m => m a -> NamesT m a
    cl TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primLevelSuc NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> (Sort -> Term
    Sort (Sort -> Term) -> (Term -> Sort) -> Term -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Sort
    tmSort (Term -> Term) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NamesT (TCMT IO) Term
    la) NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <#> NamesT (TCMT IO) Term
    φ NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    t NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT (TCMT IO) Term
    bA)
             NamesT (TCMT IO) Type
    -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' NamesT (TCMT IO) Term
    la NamesT (TCMT IO) Term
    bA)

      view <- intervalView'
      one <- primItIsOne
      mglueU <- getPrimitiveName' builtin_glueU
      mtransp <- getPrimitiveName' builtinTrans
      mHCompU <- getPrimitiveName' builtinHComp
      let mhcomp = Maybe QName
    mHCompU

      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 5 $ \case
        [Arg Term
    la,Arg Term
    phi,Arg Term
    bT,Arg Term
    bA,Arg Term
    b] -> do
          sphi <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    phi
          case view $ unArg $ ignoreBlocking $ sphi of
            -- Case where the hcomp has reduced away: Transport backwards
            -- along the partial element we've glued.
            IntervalView
    IOne -> do
              tTransp <- [Char] -> PrimitiveId -> ReduceM Term
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    [Char] -> a -> m Term
    getTerm (PrimitiveId -> [Char]
    forall a. IsBuiltin a => a -> [Char]
    getBuiltinId PrimitiveId
    builtin_unglueU) PrimitiveId
    builtinTrans
              iNeg    <- getTerm (getBuiltinId builtin_unglueU) builtinINeg
              iZ      <- getTerm (getBuiltinId builtin_unglueU) builtinIZero
              redReturn <=< runNamesT [] $ do
                la <- open . unArg $ la
                bT <- open . unArg $ bT
                b  <- open . unArg $ b
                pure tTransp <#> lam "i" (\ NamesT ReduceM Term
    _ -> NamesT ReduceM Term
    la) <@> lam "i" (\ NamesT ReduceM Term
    i -> NamesT ReduceM Term
    bT NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT ReduceM Term -> NamesT ReduceM Term
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg NamesT ReduceM Term
    i NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <..> Term -> NamesT ReduceM Term
    forall a. a -> NamesT ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    one)
                  <@> pure iZ <@> b

            -- Otherwise, we're dealing with a proper glu- didn't I already
            -- make this joke? Oh, yeah, in prim_unglue, right.
            IntervalView
    _ -> do
              sb <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    b
              let fallback Blocked (Arg Term)
    sbA = Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall no yes. no -> Reduced no yes
    NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
    -> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> MaybeReduced (Arg Term))
    -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced [Arg Term
    la] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> MaybeReduced (Arg Term))
    -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced [Arg Term
    bT,Arg Term
    bA] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    sb])
              case unArg $ ignoreBlocking $ sb of
                -- Project:
                Def QName
    q Elims
    es | Just [Arg Term
    _,Arg Term
    _,Arg Term
    _,Arg Term
    _,Arg Term
    _, Arg Term
    a] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims 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
    mglueU -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a b. (a -> b) -> a -> b
    $ Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    a

                -- Transport:
                Def QName
    q [Apply Arg Term
    l, Apply Arg Term
    bA, Apply Arg Term
    r, Apply Arg Term
    u0] | 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
    mtransp -> do
                  sbA <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Arg Term
    bA
                  case unArg $ ignoreBlocking sbA of
                    Lam ArgInfo
    _ Abs Term
    t -> do
                      st <- Term -> ReduceM (Blocked Term)
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' (Abs Term -> Term
    forall a. Subst a => Abs a -> a
    absBody Abs Term
    t)
                      case ignoreBlocking st of
                        Def QName
    h Elims
    es | Just [Arg Term
    la,Arg Term
    _,Arg Term
    phi,Arg Term
    bT,Arg Term
    bA] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es, QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    h Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mHCompU -> do
                          Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (Maybe Term -> Term)
    -> Maybe Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Maybe Term) -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                            KanOperation
    -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
    -> TermPosition
    -> ReduceM (Maybe Term)
    forall (m :: * -> *).
    PureTCM m =>
    KanOperation
    -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
    -> TermPosition
    -> m (Maybe Term)
    doHCompUKanOp (Blocked (Arg Term) -> Arg Term -> KanOperation
    TranspOp (Arg Term -> Blocked (Arg Term)
    forall a t. a -> Blocked' t a
    notBlocked Arg Term
    r) Arg Term
    u0) ((Arg Term, Arg Term, Arg Term, Arg Term)
    -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
    forall a. a -> FamilyOrNot a
    IsFam (Arg Term
    la,Arg Term
    phi,Arg Term
    bT,Arg Term
    bA)) TermPosition
    Eliminated
                        Term
    _ -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
    fallback (Blocked Term
    st Blocked Term -> Blocked (Arg Term) -> Blocked (Arg Term)
    forall a b. Blocked' Term a -> Blocked' Term b -> Blocked' Term b
    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
    *> Blocked (Arg Term)
    sbA)
                    Term
    _  -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
    fallback Blocked (Arg Term)
    sbA

                -- Compose:
                Def QName
    q [Apply Arg Term
    l,Apply Arg Term
    bA,Apply Arg Term
    r,Apply Arg Term
    u,Apply Arg Term
    u0] | 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
    mhcomp -> do
                  sbA <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Arg Term
    bA
                  case unArg $ ignoreBlocking sbA of
                    Def QName
    h Elims
    es | Just [Arg Term
    la,Arg Term
    _,Arg Term
    phi,Arg Term
    bT,Arg Term
    bA] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es, QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    h Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mHCompU -> do
                      Term -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a a'. a -> ReduceM (Reduced a' a)
    redReturn (Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> (Maybe Term -> Term)
    -> Maybe Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Maybe Term -> Term
    forall a. a -> Maybe a -> a
    fromMaybe Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Term -> ReduceM (Reduced MaybeReducedArgs Term))
    -> ReduceM (Maybe Term) -> ReduceM (Reduced MaybeReducedArgs Term)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
                        KanOperation
    -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
    -> TermPosition
    -> ReduceM (Maybe Term)
    forall (m :: * -> *).
    PureTCM m =>
    KanOperation
    -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
    -> TermPosition
    -> m (Maybe Term)
    doHCompUKanOp (Blocked (Arg Term) -> Arg Term -> Arg Term -> KanOperation
    HCompOp (Arg Term -> Blocked (Arg Term)
    forall a t. a -> Blocked' t a
    notBlocked Arg Term
    r) Arg Term
    u Arg Term
    u0) ((Arg Term, Arg Term, Arg Term, Arg Term)
    -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term)
    forall a. a -> FamilyOrNot a
    IsNot (Arg Term
    la,Arg Term
    phi,Arg Term
    bT,Arg Term
    bA)) TermPosition
    Eliminated
                    Term
    _ -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
    fallback Blocked (Arg Term)
    sbA
                Term
    _ -> Reduced MaybeReducedArgs Term
    -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall no yes. no -> Reduced no yes
    NoReduction (MaybeReducedArgs -> Reduced MaybeReducedArgs Term)
    -> MaybeReducedArgs -> Reduced MaybeReducedArgs Term
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> MaybeReduced (Arg Term))
    -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced [Arg Term
    la] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    sphi] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> MaybeReduced (Arg Term))
    -> [Arg Term] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Arg Term -> MaybeReduced (Arg Term)
    forall a. a -> MaybeReduced a
    notReduced [Arg Term
    bT,Arg Term
    bA] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    sb])

        [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__