    {-# OPTIONS_GHC -Wunused-imports #-}

    {-# LANGUAGE NondecreasingIndentation #-}

    module Agda.TypeChecking.Primitive.Cubical.Glue
      ( mkGComp
      , doGlueKanOp

      , primGlue'
      , prim_glue'
      , prim_unglue'
      )
      where

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

    import Agda.TypeChecking.Names
      ( NamesT, runNamesT, runNames, cl, lam, open, ilam )
    import Agda.TypeChecking.Primitive.Cubical.Base
    import Agda.TypeChecking.Reduce
      ( reduceB' )
    import Agda.TypeChecking.Substitute
      ( absBody, apply, sort, applyE )

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

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

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

    import Agda.Utils.Impossible
      ( __IMPOSSIBLE__ )

    -- | Define a "ghcomp" version of gcomp. Normal comp looks like:
    --
    -- comp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u ] (forward A 0 u0)
    --
    -- So for "gcomp" we compute:
    --
    -- gcomp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u, ~ phi -> forward A 0 u0 ] (forward A 0 u0)
    --
    -- The point of this is that gcomp does not produce any empty
    -- systems (if phi = 0 it will reduce to "forward A 0 u".
    mkGComp :: forall m. HasBuiltins m
            => String
            -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)
    mkGComp :: forall (m :: * -> *).
    HasBuiltins m =>
    String
    -> NamesT
         m
         (NamesT m Term
          -> NamesT m Term
          -> NamesT m Term
          -> NamesT m Term
          -> NamesT m Term
          -> NamesT m Term)
    mkGComp String
    s = do
      let getTermLocal :: IsBuiltin a => a -> NamesT m Term
          getTermLocal :: forall a. IsBuiltin a => a -> NamesT m Term
    getTermLocal = String -> a -> NamesT m Term
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    String -> a -> m Term
    getTerm String
    s
      tPOr <- PrimitiveId -> NamesT m Term
    forall a. IsBuiltin a => a -> NamesT m Term
    getTermLocal PrimitiveId
    builtinPOr
      tIMax <- getTermLocal builtinIMax
      tIMin <- getTermLocal builtinIMin
      tINeg <- getTermLocal builtinINeg
      tHComp <- getTermLocal builtinHComp
      tTrans <- getTermLocal builtinTrans
      io      <- getTermLocal builtinIOne
      iz      <- getTermLocal builtinIZero
      let forward NamesT m Term
    la NamesT m Term
    bA NamesT m Term
    r NamesT m Term
    u = 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
    <#> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "i" (\ NamesT m Term
    i -> 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 :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
    `imax` NamesT m Term
    r))
                                          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
    lam String
    "i" (\ 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 -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
    `imax` NamesT m Term
    r))
                                          NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    r
                                          NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    u
      return $ \ NamesT m Term
    la NamesT m Term
    bA NamesT m Term
    phi NamesT m Term
    u NamesT m Term
    u0 ->
        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
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg NamesT m Term
    phi)
                    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
    lam String
    "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 -> 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
    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 -> 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 -> NamesT m Term -> NamesT m Term -> NamesT m Term
    forward NamesT m Term
    la NamesT m Term
    bA NamesT m Term
    i (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 -> NamesT m Term
    forall (m :: * -> *). HasBuiltins m => m Term -> m Term
    ineg 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 -> 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 -> NamesT m Term -> NamesT m Term -> NamesT m Term
    forward NamesT m Term
    la NamesT m Term
    bA (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    iz) 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
    -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term
    forward NamesT m Term
    la NamesT m Term
    bA (Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    iz) NamesT m Term
    u0

    -- | Perform the Kan operations for a @Glue φ A (T , e)@ type.
    doGlueKanOp
      :: forall m. PureTCM m
      => KanOperation -- ^ Are we composing or transporting?
      -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
      -- ^ The data of the Glue operation: The levels of @A@ and @T@, @A@
      -- itself, the extent of @T@, @T@ itself, and the family of
      -- equivalences.
      -> TermPosition
      -- ^ Are we computing a plain hcomp/transp or are we computing under
      -- @unglue@?
      -> m (Maybe Term)

    doGlueKanOp :: forall (m :: * -> *).
    PureTCM m =>
    KanOperation
    -> FamilyOrNot
         (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
    -> TermPosition
    -> m (Maybe Term)
    doGlueKanOp (HCompOp Blocked (Arg Term)
    psi Arg Term
    u Arg Term
    u0) (IsNot (Arg Term
    la, Arg Term
    lb, Arg Term
    bA, Arg Term
    phi, Arg Term
    bT, Arg Term
    e)) TermPosition
    tpos = do
    -- hcomp {psi} u u0 : Glue {la} {lb} bA {φ} (bT, e)
    -- ... |- la, lb : Level
    -- ... |- bA : Type la
    -- ... |- bT : Partial φ (Type lB)
    -- ... |- e : PartialP φ λ o → bT o ≃ bA
      let getTermLocal :: IsBuiltin a => a -> m Term
          getTermLocal :: forall a. IsBuiltin a => a -> m Term
    getTermLocal = String -> a -> m Term
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    String -> a -> m Term
    getTerm (String -> a -> m Term) -> String -> a -> m Term
    forall a b. (a -> b) -> a -> b
    $ PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    builtinHComp String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    builtinGlue
      tHComp   <- PrimitiveId -> m Term
    forall a. IsBuiltin a => a -> m Term
    getTermLocal PrimitiveId
    builtinHComp
      tEFun    <- getTermLocal builtinEquivFun
      tunglue  <- getTermLocal builtin_unglue
      io       <- getTermLocal builtinIOne
      tItIsOne <- getTermLocal builtinItIsOne
      view     <- intervalView'

      runNamesT [] $ do
        psi <- open . unArg $ ignoreBlocking psi
        u   <- open . unArg $ u
        u0  <- open . unArg $ u0
        la  <- open . unArg $ la
        lb  <- open . unArg $ lb
        bA  <- open . unArg $ bA
        phi <- open . unArg $ phi
        bT  <- open . unArg $ bT
        e   <- open . unArg $ e

        ifM (headStop tpos phi) (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
    -> 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
    lb (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
    o) NamesT m Term
    psi NamesT m Term
    u NamesT m Term
    u0 NamesT m Term
    i
          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
    lb 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
    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
    e 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
    <@> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "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, 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 -> 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, 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 -> Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tEFun 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
    la 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
    o) 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
    e 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
    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)

        case tpos of
          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)
          TermPosition
    Eliminated -> NamesT m Term
    a1

    -- ...    |- psi, u0
    -- ..., i |- la, lb, bA, phi, bT, e
    doGlueKanOp (TranspOp Blocked (Arg Term)
    psi Arg Term
    u0) (IsFam (Arg Term
    la, Arg Term
    lb, Arg Term
    bA, Arg Term
    phi, Arg Term
    bT, Arg Term
    e)) TermPosition
    tpos = do
    -- transp (λ i → Glue {la} {lb} bA {φ} (bT , e)) ψ u0
      let
        localUse :: String
    localUse = PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    builtinTrans String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    builtinGlue
        getTermLocal :: IsBuiltin a => a -> m Term
        getTermLocal :: forall a. IsBuiltin a => a -> m Term
    getTermLocal = String -> a -> m Term
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    String -> a -> m Term
    getTerm String
    localUse
      tHComp <- PrimitiveId -> m Term
    forall a. IsBuiltin a => a -> m Term
    getTermLocal PrimitiveId
    builtinHComp
      tTrans <- getTermLocal builtinTrans
      tForall <- getTermLocal builtinFaceForall
      tEFun   <- getTermLocal builtinEquivFun
      tEProof <- getTermLocal builtinEquivProof
      toutS   <- getTermLocal builtinSubOut
      tunglue <- getTermLocal builtin_unglue
      io      <- getTermLocal builtinIOne
      iz      <- getTermLocal builtinIZero
      tLMax   <- getTermLocal builtinLevelMax
      tTransp <- getTermLocal builtinTranspProof
      tItIsOne <- getTermLocal builtinItIsOne
      kit <- fromMaybe __IMPOSSIBLE__ <$> getSigmaKit
      runNamesT [] $ do

        gcomp <- mkGComp localUse

        -- transpFill: transp (λ j → bA (i ∧ j)) (φ ∨ ~ i) u0
        -- connects u0 and transp bA i0 u0
        let 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
    <#> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "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
    <@> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "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
    . String
    -> (NamesT Identity Term -> NamesT Identity Term)
    -> NamesT Identity Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "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
        lb  <- lami lb
        bA  <- lami bA
        phi <- lami phi
        bT  <- lami bT
        e   <- lami e

        -- Andreas, 2022-03-24, fixing #5838
        -- Following the updated note
        --
        --   Simon Huber, A Cubical Type Theory for Higher Inductive Types
        --   https://simhu.github.io/misc/hcomp.pdf (February 2022)
        --
        -- See: https://github.com/agda/agda/issues/5755#issuecomment-1043797776

        -- unglue_u0 i = unglue la[i/i] lb[i/i] bA[i/i] phi[i/i] bT[i/i] e[i/e] u0
        let unglue_u0 NamesT m Term
    i = (NamesT m Term -> NamesT m Term -> NamesT m Term)
    -> NamesT m Term -> [NamesT m Term] -> NamesT m Term
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl 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
    tunglue) ((NamesT m Term -> NamesT m Term)
    -> [NamesT m Term] -> [NamesT m Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (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
    la, NamesT m Term
    lb, NamesT m Term
    bA, NamesT m Term
    phi, NamesT m Term
    bT, NamesT m Term
    e]) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    u0

        view <- intervalView'

        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
    lb (String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "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
    <..> 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 = gcomp (ψ ∨ (∀ i. φ)) (λ { i (ψ = i1) → unglue_u0 i ; i ((∀ i. φ) = i1) → equivFun ... })
          --        (unglue_u0 i0)
          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)
            (String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "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,       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) -> 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, 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) -> 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 -> NamesT m Term
    w 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 -> 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))

          max NamesT m Term
    l NamesT m Term
    l' = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tLMax 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
    l'
          sigCon NamesT m Term
    x NamesT m Term
    y = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ConHead -> ConInfo -> Elims -> Term
    Con (SigmaKit -> ConHead
    sigmaCon SigmaKit
    kit) ConInfo
    ConOSystem []) NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    x NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> NamesT m Term
    y

          -- The underlying function of our partial equivalence at the given
          -- endpoint of the interval, together with proof (o : IsOne φ).
          w NamesT m Term
    i NamesT m Term
    o = Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    tEFun 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
    i)
                             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
    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
    o)
                             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)
                             NamesT m Term -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> (NamesT m Term
    e 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)

          -- Type of fibres of the partial equivalence over a1.
          fiberT 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
    fiber (NamesT m Term
    lb 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
    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
    <..> NamesT m Term
    o) (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
    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
    a1

          -- We don't have to do anything special for "~ forall. phi"
          -- here (to implement "ghcomp") as it is taken care off by
          -- tEProof in t1'alpha below
          pe NamesT m Term
    o = -- o : IsOne φ
            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 -> NamesT m Term -> NamesT m Term
    max (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
    lb 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
    fiberT NamesT m Term
    o)
              [ (NamesT m Term
    psi       , 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) -> 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
    sigCon NamesT m Term
    u0     (String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "_" ((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
    a1))
              , (NamesT m Term
    forallphi , 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) -> 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 -> NamesT m Term
    sigCon (NamesT m Term -> NamesT m Term
    t1 NamesT m Term
    o) (String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "_" ((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
    a1))
              ]
          -- pe is a partial fibre of the equivalence with extent (ψ ∨ ∀ i. φ)
          -- over a1

          -- "ghcomp" is implemented in the proof of tEProof
          -- (see src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda)
          t1'alpha NamesT m Term
    o = -- o : IsOne φ
             -- Because @e i1 1=1@ is an equivalence, we can extend the
             -- partial fibre @pe@ to an actual fibre of (e i1 1=1) over a1.
             Term -> NamesT m Term
    forall a. a -> NamesT m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    toutS 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
    max (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
    lb 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
    fiberT 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
    pe 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
    tEProof
                    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
    <@> 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
    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
    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 -> 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
    e 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 -> NamesT m Term -> NamesT m Term
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
    <@> 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 -> 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
    pe NamesT m Term
    o)

          -- 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
    <@> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    forall (m :: * -> *).
    Monad m =>
    String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
    lam String
    "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, 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) -> 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,             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) -> 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
    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)
          TermPosition
    Eliminated -> NamesT m Term
    a1'
    doGlueKanOp KanOperation
    _ FamilyOrNot
      (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
    _ TermPosition
    _ = m (Maybe Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- The implementation of 'primGlue'. Handles reduction where the partial
    -- element is defined.
    primGlue' :: TCM PrimitiveImpl
    primGlue' :: TCM PrimitiveImpl
    primGlue' = do
      Cubical -> TCM ()
    requireCubical Cubical
    CFull
      -- primGlue
      --   : {la lb : Level} (A : Type la) {φ : I}
      --   → (T : Partial φ (Type lb)
      --   → (e : PartialP φ λ o → A ≃ T o)
      --   → Type lb
      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
    $
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "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 ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "lb" (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 -> 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
    lb ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' String
    "A" (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
    a ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "φ" 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
    φ ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    nPi' String
    "T" (String
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    String
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' String
    "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 -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' (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
    lb) (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
    lb)) ((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 ->
           String
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    String
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' String
    "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' (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
    primLevelMax 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
    <@> NamesT (TCMT IO) Term
    lb) (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
    primEquiv 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
    lb 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
    <@> (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
    o) 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) Type
    -> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
    --> (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
    lb))
      view <- intervalView'
      one <- primItIsOne
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 6 $ \[Arg Term]
    ts ->
        case [Arg Term]
    ts of
         [Arg Term
    la,Arg Term
    lb,Arg Term
    a,Arg Term
    phi,Arg Term
    t,Arg Term
    e] -> do
           sphi <- Arg Term -> ReduceM (Blocked (Arg Term))
    forall t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    phi
           -- If @φ = i1@ then we reduce to @T 1=1@, since @Glue@ is also a Kan operation.
           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]
             -- Otherwise we're a regular ol' type.
             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,Arg Term
    lb,Arg Term
    a] 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
    t,Arg Term
    e])
         [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | The implementation of 'prim_glue', the introduction form for @Glue@
    -- types.
    prim_glue' :: TCM PrimitiveImpl
    prim_glue' :: TCM PrimitiveImpl
    prim_glue' = do
      Cubical -> TCM ()
    requireCubical Cubical
    CFull
      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
    $
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "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 ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "lb" (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 -> 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
    lb ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "A" (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
    a ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "φ" 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
    φ ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "T" (String
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    String
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' String
    "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 ->  NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' (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
    lb) (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
    lb)) ((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 ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "e" (String
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    String
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' String
    "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 -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' (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
    primLevelMax 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
    <@> NamesT (TCMT IO) Term
    lb) (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
    primEquiv 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
    lb 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
    <@> (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
    o) 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) 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
    e ->
           String
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    String
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' String
    "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
    lb (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
    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
    a 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
    lb (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
    primGlue 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
    <#> NamesT (TCMT IO) Term
    lb 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) 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
    e)))

      -- Takes a partial element of @t : T@ and an element of the base type @A@
      -- which extends @e t@, and makes it into a Glue.
      view <- intervalView'
      one <- primItIsOne
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 8 $ \case
        [Arg Term
    la, Arg Term
    lb, Arg Term
    bA, Arg Term
    phi, Arg Term
    bT, Arg Term
    e, 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
          -- When @φ = 1@ then @t : T@ is totally defined.
          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]
            -- Otherwise we'll just wait to get unglued.
            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,Arg Term
    lb,Arg Term
    bA] 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
    e,Arg Term
    t,Arg Term
    a])
        [Arg Term]
    _ -> ReduceM (Reduced MaybeReducedArgs Term)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | The implementation of 'prim_unglue', the elimination form for
    -- @Glue@ types.
    prim_unglue' :: TCM PrimitiveImpl
    prim_unglue' :: TCM PrimitiveImpl
    prim_unglue' = do
      Cubical -> TCM ()
    requireCubical Cubical
    CFull
      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
    $
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "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 ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "lb" (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 -> 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
    lb ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "A" (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
    a ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "φ" 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
    φ ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "T" (String
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    String
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' String
    "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 ->  NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' (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
    lb) (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
    lb)) ((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 ->
           String
    -> NamesT (TCMT IO) Type
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, MonadDebug m) =>
    String
    -> NamesT m Type
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    hPi' String
    "e" (String
    -> NamesT (TCMT IO) Term
    -> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
    -> NamesT (TCMT IO) Type
    forall (m :: * -> *).
    (MonadAddContext m, HasBuiltins m, MonadDebug m) =>
    String
    -> NamesT m Term
    -> (NamesT m Term -> NamesT m Type)
    -> NamesT m Type
    pPi' String
    "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 -> NamesT (TCMT IO) Term
    -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
    el' (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
    primLevelMax 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
    <@> NamesT (TCMT IO) Term
    lb) (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
    primEquiv 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
    lb 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
    <@> (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
    o) 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) 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
    e ->
           (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
    lb (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
    primGlue 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
    <#> NamesT (TCMT IO) Term
    lb 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) 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
    e)) 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
    a)

      -- Takes an element @b : Glue φ A (T, e)@ to an element of @A@ which,
      -- under @φ@, agrees with @e b@. Recall that @φ ⊢ e : A → T@ and @φ ⊢
      -- Glue φ A (T, e) = T@ so this is well-typed.
      view <- intervalView'
      one <- primItIsOne
      mGlue <- getPrimitiveName' builtinGlue
      mglue <- getPrimitiveName' builtin_glue
      mtransp <- getPrimitiveName' builtinTrans
      mhcomp <- getPrimitiveName' builtinHComp
      return $ PrimImpl t $ primFun __IMPOSSIBLE__ 7 $ \case
        [Arg Term
    la, Arg Term
    lb, Arg Term
    bA, Arg Term
    phi, Arg Term
    bT, Arg Term
    e, 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
            -- When @φ = i1@ we have @Glue i1 A (T , e) = T@ so @b : T@,
            -- and we must produce @unglue b : A [ i1 → e b ]@. But that's
            -- just @e b@!
            IntervalView
    IOne -> do
              let argOne :: Arg Term
    argOne = Relevance -> Arg Term -> Arg Term
    forall a. LensRelevance a => Relevance -> a -> a
    setRelevance Relevance
    irrelevant (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
    one
              tEFun <- String -> BuiltinId -> ReduceM Term
    forall (m :: * -> *) a.
    (HasBuiltins m, IsBuiltin a) =>
    String -> a -> m Term
    getTerm (PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    builtin_unglue) BuiltinId
    builtinEquivFun
              redReturn $ tEFun `apply` [lb,la,argH $ unArg bT `apply` [argOne],bA, argN $ unArg e `apply` [argOne],b]

            -- Otherwise we're dealing with a proper glued thing.
            -- Definitely a sticky situation!
            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,Arg Term
    lb] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ (Blocked (Arg Term) -> MaybeReduced (Arg Term))
    -> [Blocked (Arg Term)] -> MaybeReducedArgs
    forall a b. (a -> b) -> [a] -> [b]
    map Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced [Blocked (Arg Term)
    sbA, 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
    e] MaybeReducedArgs -> MaybeReducedArgs -> MaybeReducedArgs
    forall a. [a] -> [a] -> [a]
    ++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
    reduced Blocked (Arg Term)
    sb])
              case unArg $ ignoreBlocking $ sb of
                -- Case 1: unglue (glue a) = a. This agrees with the @φ =
                -- i1@ reduction because under @φ@, the argument to
                -- @glue@ must be in the image of the equivalence.
                Def QName
    q Elims
    es
                  | Just [Arg Term
    _, Arg Term
    _, 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
    mglue -> 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

                -- Case 2: unglue (transp (λ i → Glue ...) r u0).
                -- Defer to the implementation of @doGlueKanOp DoTransp ... Eliminated@: It knows how to unglue itself.
                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 t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    bA
                  -- Require that bA be a lambda abstraction...
                  case unArg $ ignoreBlocking sbA of
                    Lam ArgInfo
    _ Abs Term
    t -> do
                      -- And that its body reduces to a Glue type.
                      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
                        -- In this case, we use the Glue data extracted from
                        -- the family we're transporting over.
                        Def QName
    g Elims
    es | Just [Arg Term
    la', Arg Term
    lb', Arg Term
    bA', Arg Term
    phi', Arg Term
    bT', Arg Term
    e'] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es, QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    g Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mGlue -> 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, Arg Term, Arg Term)
    -> TermPosition
    -> ReduceM (Maybe Term)
    forall (m :: * -> *).
    PureTCM m =>
    KanOperation
    -> FamilyOrNot
         (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
    -> TermPosition
    -> m (Maybe Term)
    doGlueKanOp (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, Arg Term, Arg Term)
    -> FamilyOrNot
         (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
    forall a. a -> FamilyOrNot a
    IsFam (Arg Term
    la',Arg Term
    lb',Arg Term
    bA',Arg Term
    phi',Arg Term
    bT',Arg Term
    e')) 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

                -- Case 3: unglue (hcomp u u0).
                -- Defer to the implementation of @doGlueKanOp DoHComp ... Eliminated@: It knows how to unglue itself.
                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 t. Reduce t => t -> ReduceM (Blocked t)
    reduceB' Arg Term
    bA
                  case unArg $ ignoreBlocking sbA of
                    -- Idem: use the Glue data from the type we're doing
                    -- hcomp in.
                    Def QName
    g Elims
    es | Just [Arg Term
    la', Arg Term
    lb', Arg Term
    bA', Arg Term
    phi', Arg Term
    bT', Arg Term
    e'] <- Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es, QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    g Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == Maybe QName
    mGlue -> 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, Arg Term, Arg Term)
    -> TermPosition
    -> ReduceM (Maybe Term)
    forall (m :: * -> *).
    PureTCM m =>
    KanOperation
    -> FamilyOrNot
         (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
    -> TermPosition
    -> m (Maybe Term)
    doGlueKanOp (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, Arg Term, Arg Term)
    -> FamilyOrNot
         (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
    forall a. a -> FamilyOrNot a
    IsNot (Arg Term
    la',Arg Term
    lb',Arg Term
    bA',Arg Term
    phi',Arg Term
    bT',Arg Term
    e')) 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,Arg Term
    lb,Arg Term
    bA] 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
    e] 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__