{-# OPTIONS_GHC -Wunused-imports #-}

-- | Implementation of the primitives relating to Cubical identity types.

module Agda.TypeChecking.Primitive.Cubical.Id
  ( -- * General elimination form
    primIdElim'
  -- * Introduction form
  , primConId'
  -- * Projection maps (primarily used internally)
  , primIdFace'
  , primIdPath'
  -- * Kan operations
  , doIdKanOp
  )
  where

import qualified Data.IntMap as IntMap
import Data.Traversable
import Data.Maybe

import Agda.Syntax.Common
  ( Cubical(..), Arg(..), defaultArgInfo, defaultArg )
import Agda.Syntax.Internal

import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Debug (__IMPOSSIBLE_VERBOSE__)

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

import Agda.Utils.Impossible (__IMPOSSIBLE__)

-- | Primitive elimination rule for the cubical identity types. Unlike
-- J, @idElim@ makes explicit the structure of Swan's identity types as
-- being pairs of a cofibration and a path. Moreover, it records that
-- the path is definitionally @refl@ under that cofibration.
primIdElim' :: TCM PrimitiveImpl
primIdElim' :: TCM PrimitiveImpl
primIdElim' = do
  -- The implementation here looks terrible but most of it is actually
  -- the type.
  Cubical -> String -> TCM ()
requireCubical Cubical
CErased String
""
  Type
t <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"c" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
c ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"x" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
x ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"C" (forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"y" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
y ->
              forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
c)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bC ->
    -- To construct (C : (y : A) → Id A x y → Type c), it suffices to:

    -- For all cofibrations φ,
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"φ" forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType (\ NamesT (TCMT IO) Term
phi ->
      -- For all y : A [ φ → (λ _ → x) ]
      forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"y" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"o" (forall a b. a -> b -> a
const NamesT (TCMT IO) Term
x)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
y ->
      let pathxy :: NamesT (TCMT IO) Term
pathxy = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
outSy
          outSy :: NamesT (TCMT IO) Term
outSy  = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"o" (forall a b. a -> b -> a
const NamesT (TCMT IO) Term
x) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y
          reflx :: NamesT (TCMT IO) Term
reflx  = forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
x -- TODO Andrea, should block on o
      -- For all w : (Path A x (outS y)) [ φ (λ _ → refl {x = outS y} ]
      in forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"w" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
pathxy forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
reflx) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
w ->
      let outSw :: NamesT (TCMT IO) Term
outSw = (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
pathxy forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
reflx forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
w)
      in forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
c forall a b. (a -> b) -> a -> b
$ NamesT (TCMT IO) Term
bC forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
outSy forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primConId forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
outSy forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
outSw))
      -- Construct an inhabitant of (C (outS y) (conid φ (outS w)))
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"y" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) (\ NamesT (TCMT IO) Term
y ->
      forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"p" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
p ->
      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
c forall a b. (a -> b) -> a -> b
$ NamesT (TCMT IO) Term
bC forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
p)

  -- Implementation starts here:
  Term
conid <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primConId
  Term
sin <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubIn
  Term
path <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
8 forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
a,Arg Term
c,Arg Term
bA,Arg Term
x,Arg Term
bC,Arg Term
f,Arg Term
y,Arg Term
p] -> do
      Blocked (Arg Term)
sp <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
p
      Term -> Term -> Maybe (Arg Term, Arg Term)
cview <- forall (m :: * -> *).
HasBuiltins m =>
m (Term -> Term -> Maybe (Arg Term, Arg Term))
conidView'
      case Term -> Term -> Maybe (Arg Term, Arg Term)
cview (forall e. Arg e -> e
unArg Arg Term
x) forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sp of
        -- Record that the right endpoint and the path definitionally
        -- agree with x φ holds. This is guaranteed internally by the
        -- typing rule for @conId@ but can't be recovered from
        -- @primIdPath@ and @primIdFace@ (see #2598)
        Just (Arg Term
phi, Arg Term
w) -> do
          let y' :: Term
y' = Term
sin forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
a, Arg Term
bA, Arg Term
phi, forall e. e -> Arg e
argN (forall e. Arg e -> e
unArg Arg Term
y)]
          let w' :: Term
w' = Term
sin forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
a, forall e. e -> Arg e
argN (Term
path forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
a, Arg Term
bA, Arg Term
x, Arg Term
y]), Arg Term
phi, forall e. e -> Arg e
argN (forall e. Arg e -> e
unArg Arg Term
w)]
          forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
f forall t. Apply t => t -> [Arg Term] -> t
`apply` [Arg Term
phi, forall e. e -> Arg e
defaultArg Term
y', forall e. e -> Arg e
defaultArg Term
w']
        Maybe (Arg Term, Arg Term)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
a,Arg Term
c,Arg Term
bA,Arg Term
x,Arg Term
bC,Arg Term
f,Arg Term
y] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sp]
    [Arg Term]
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
"implementation of primIdElim called with wrong arity"

-- | Introduction form for the cubical identity types.
primConId' :: TCM PrimitiveImpl
primConId' :: TCM PrimitiveImpl
primConId' = do
  Cubical -> String -> TCM ()
requireCubical Cubical
CErased String
""
  Type
t <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"x" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
x ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"y" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
y ->
    forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType -- Cofibration
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y)
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y)

  -- Implementation note: conId, as the name implies, is a constructor.
  -- It's not represented as a constructor because users can't match on
  -- it (but we, internally, can: see createMissingConIdClause).

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
6 forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
l,Arg Term
bA,Arg Term
x,Arg Term
y,Arg Term
phi,Arg Term
p] -> do
      Blocked (Arg Term)
sphi <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
      Term -> IntervalView
view <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
      case Term -> IntervalView
view forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sphi of
        -- But even though it's a constructor, it does reduce, in some
        -- cases: If the cofibration is definitely true, then we return
        -- reflId.  TODO: Handle this in the conversion checker instead?
        IntervalView
IOne -> do
          Term
reflId <- forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
String -> a -> m Term
getTerm (forall a. IsBuiltin a => a -> String
getBuiltinId PrimitiveId
builtinConId) BuiltinId
builtinReflId
          forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ Term
reflId
        IntervalView
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
l,Arg Term
bA,Arg Term
x,Arg Term
y] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi, forall a. a -> MaybeReduced a
notReduced Arg Term
p]
    [Arg Term]
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
"implementation of primConId called with wrong arity"

-- | Extract the underlying cofibration from an inhabitant of the
-- cubical identity types.
--
-- TODO (Amy, 2022-08-17): Projecting a cofibration from a Kan type
-- violates the cubical phase distinction.
primIdFace' :: TCM PrimitiveImpl
primIdFace' :: TCM PrimitiveImpl
primIdFace' = do
  Cubical -> String -> TCM ()
requireCubical Cubical
CErased String
""
  Type
t <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"x" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
x ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"y" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
y ->
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y)
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Type
primIntervalType

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
5 forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
l,Arg Term
bA,Arg Term
x,Arg Term
y,Arg Term
t] -> do
      Blocked (Arg Term)
st <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
t
      Maybe QName
mConId <- forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' PrimitiveId
builtinConId
      Term -> Term -> Maybe (Arg Term, Arg Term)
cview <- forall (m :: * -> *).
HasBuiltins m =>
m (Term -> Term -> Maybe (Arg Term, Arg Term))
conidView'
      case Term -> Term -> Maybe (Arg Term, Arg Term)
cview (forall e. Arg e -> e
unArg Arg Term
x) forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg (forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
st) of
        Just (Arg Term
phi, Arg Term
_) -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (forall e. Arg e -> e
unArg Arg Term
phi)
        Maybe (Arg Term, Arg Term)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
l,Arg Term
bA,Arg Term
x,Arg Term
y] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
st]
    [Arg Term]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Extract the underlying path from an inhabitant of the
-- cubical identity types.
primIdPath' :: TCM PrimitiveImpl
primIdPath' :: TCM PrimitiveImpl
primIdPath' = do
  Cubical -> String -> TCM ()
requireCubical Cubical
CErased String
""
  Type
t <- forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"x" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
x ->
    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"y" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
y ->
    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y)
    forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
y)

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PrimFun -> PrimitiveImpl
PrimImpl Type
t forall a b. (a -> b) -> a -> b
$ QName
-> Arity
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Arity
5 forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
l,Arg Term
bA,Arg Term
x,Arg Term
y,Arg Term
t] -> do
      Blocked (Arg Term)
st <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
t
      Maybe QName
mConId <- forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' PrimitiveId
builtinConId
      Term -> Term -> Maybe (Arg Term, Arg Term)
cview <- forall (m :: * -> *).
HasBuiltins m =>
m (Term -> Term -> Maybe (Arg Term, Arg Term))
conidView'
      case Term -> Term -> Maybe (Arg Term, Arg Term)
cview (forall e. Arg e -> e
unArg Arg Term
x) forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg (forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
st) of
        Just (Arg Term
_, Arg Term
w) -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn (forall e. Arg e -> e
unArg Arg Term
w)
        Maybe (Arg Term, Arg Term)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall no yes. no -> Reduced no yes
NoReduction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
l,Arg Term
bA,Arg Term
x,Arg Term
y] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
st]
    [Arg Term]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Check that a term matches a given predicate on every consistent
-- substitution of interval variables which makes the given cofibration
-- hold.
onEveryFace
  :: Term -- ^ The cofibration @φ@
  -> Term -- ^ The term to test
  -> (Term -> Bool)
  -- ^ The predicate to test with.
  -> ReduceM Bool
onEveryFace :: Term -> Term -> (Term -> Bool) -> ReduceM Bool
onEveryFace Term
phi Term
u Term -> Bool
p = do
  IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
  let boolToI :: Bool -> Term
boolToI Bool
b = if Bool
b then IntervalView -> Term
unview IntervalView
IOne else IntervalView -> Term
unview IntervalView
IZero
  [(IntMap Bool, [Term])]
as <- forall (m :: * -> *).
HasBuiltins m =>
Term -> m [(IntMap Bool, [Term])]
decomposeInterval Term
phi
  [Bool]
bools <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(IntMap Bool, [Term])]
as forall a b. (a -> b) -> a -> b
$ \ (IntMap Bool
bs,[Term]
ts) -> do
    let u' :: Term
u' = forall a. EndoSubst a => [(Arity, a)] -> Substitution' a
listS (forall a. IntMap a -> [(Arity, a)]
IntMap.toAscList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map Bool -> Term
boolToI IntMap Bool
bs) forall a. Subst a => Substitution' (SubstArg a) -> a -> a
`applySubst` Term
u
    Blocked Term
t <- Term -> ReduceM (Blocked Term)
reduce2Lam Term
u'
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Term -> Bool
p forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
t
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
bools)

doIdKanOp
  :: KanOperation           -- ^ Are we composing or transporting?
  -> FamilyOrNot (Arg Term) -- ^ Level argument
  -> FamilyOrNot (Arg Term, Arg Term, Arg Term)
    -- ^ Domain, left and right endpoints of the identity type
  -> ReduceM (Maybe (Reduced t Term))
doIdKanOp :: forall t.
KanOperation
-> FamilyOrNot (Arg Term)
-> FamilyOrNot (Arg Term, Arg Term, Arg Term)
-> ReduceM (Maybe (Reduced t Term))
doIdKanOp KanOperation
kanOp FamilyOrNot (Arg Term)
l FamilyOrNot (Arg Term, Arg Term, Arg Term)
bA_x_y = do
  let getTermLocal :: IsBuiltin a => a -> ReduceM Term
      getTermLocal :: forall a. IsBuiltin a => a -> ReduceM Term
getTermLocal = forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
String -> a -> m Term
getTerm forall a b. (a -> b) -> a -> b
$ KanOperation -> String
kanOpName KanOperation
kanOp forall a. [a] -> [a] -> [a]
++ String
" for " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> String
getBuiltinId BuiltinId
builtinId

  IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
  Maybe QName
mConId <- forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' PrimitiveId
builtinConId
  Term -> Term -> Maybe (Arg Term, Arg Term)
cview <- forall (m :: * -> *).
HasBuiltins m =>
m (Term -> Term -> Maybe (Arg Term, Arg Term))
conidView'
  let isConId :: Term -> Bool
isConId Term
t = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ Term -> Term -> Maybe (Arg Term, Arg Term)
cview HasCallStack => Term
__DUMMY_TERM__ Term
t

  Blocked (Arg Term)
sa0 <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' (KanOperation -> Arg Term
kanOpBase KanOperation
kanOp)
  -- TODO: wasteful to compute b even when cheaper checks might fail
  --
  -- Should we go forward with the Kan operation? This is the case when
  -- doing transport always, and when every face fo the partial element
  -- has reduced to @conid@ otherwise. Note that @conidView@ treats
  -- @reflId@ as though it were @conid i1 refl@.
  Bool
b <- case KanOperation
kanOp of
    TranspOp{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    HCompOp Blocked (Arg Term)
_ Arg Term
u Arg Term
_ ->
      Term -> Term -> (Term -> Bool) -> ReduceM Bool
onEveryFace (forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking forall b c a. (b -> c) -> (a -> b) -> a -> c
. KanOperation -> Blocked (Arg Term)
kanOpCofib forall a b. (a -> b) -> a -> b
$ KanOperation
kanOp) (forall e. Arg e -> e
unArg Arg Term
u) Term -> Bool
isConId

  case Maybe QName
mConId of
    Just QName
conid | Term -> Bool
isConId (forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sa0), Bool
b -> (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall a b. (a -> b) -> a -> b
$ do
      Term
tHComp    <- forall a. IsBuiltin a => a -> ReduceM Term
getTermLocal PrimitiveId
builtinHComp
      Term
tTrans    <- forall a. IsBuiltin a => a -> ReduceM Term
getTermLocal PrimitiveId
builtinTrans
      Term
tIMin     <- forall a. IsBuiltin a => a -> ReduceM Term
getTermLocal PrimitiveId
builtinDepIMin
      Term
idFace    <- forall a. IsBuiltin a => a -> ReduceM Term
getTermLocal PrimitiveId
builtinIdFace
      Term
idPath    <- forall a. IsBuiltin a => a -> ReduceM Term
getTermLocal PrimitiveId
builtinIdPath
      Term
tPathType <- forall a. IsBuiltin a => a -> ReduceM Term
getTermLocal BuiltinId
builtinPath
      Term
tConId    <- forall a. IsBuiltin a => a -> ReduceM Term
getTermLocal PrimitiveId
builtinConId

      forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
        let
          io :: NamesT ReduceM Term
io = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ IntervalView -> Term
unview IntervalView
IOne
          iz :: NamesT ReduceM Term
iz = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ IntervalView -> Term
unview IntervalView
IZero
          conId :: NamesT ReduceM Term
conId = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tConId

          eval :: KanOperation
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
eval TranspOp{} NamesT ReduceM Term
l NamesT ReduceM Term
bA NamesT ReduceM Term
phi NamesT ReduceM Term
_ NamesT ReduceM Term
u0 =
            forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
u0
          eval HCompOp{} NamesT ReduceM Term
l NamesT ReduceM Term
bA NamesT ReduceM Term
phi NamesT ReduceM Term
u NamesT ReduceM Term
u0 =
            forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT ReduceM Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
u0

        -- Compute a line of levels. So we can invoke 'eval' uniformly.
        NamesT ReduceM Term
l <- case FamilyOrNot (Arg Term)
l of
          IsFam Arg Term
l -> forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ Arg Term
l
          IsNot Arg Term
l -> forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
NoAbs String
"_" forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
l)

        NamesT ReduceM Term
p0 <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ KanOperation -> Arg Term
kanOpBase KanOperation
kanOp

        -- p is the partial element we are extending against. This is
        -- used to compute the resulting cofibration, so we fake a
        -- partial element when doing transport.
        NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
p <- case KanOperation
kanOp of
          HCompOp Blocked (Arg Term)
_ Arg Term
u Arg Term
_ -> do
            NamesT ReduceM Term
u <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ Arg Term
u
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term
i NamesT ReduceM Term
o -> NamesT ReduceM Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT ReduceM Term
o
          TranspOp{} -> do
            forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term
i NamesT ReduceM Term
o -> NamesT ReduceM Term
p0

        NamesT ReduceM Term
phi <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Blocked' t a -> a
ignoreBlocking forall a b. (a -> b) -> a -> b
$ KanOperation -> Blocked (Arg Term)
kanOpCofib KanOperation
kanOp

        -- Similarly to the fake line of levels above, fake lines of
        -- everything even when we're doing composition, for uniformity
        -- of eval.
        [NamesT ReduceM Term
bA, NamesT ReduceM Term
x, NamesT ReduceM Term
y] <- case FamilyOrNot (Arg Term, Arg Term, Arg Term)
bA_x_y of
          IsFam (Arg Term
bA, Arg Term
x, Arg Term
y) -> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Arg Term
bA, Arg Term
x, Arg Term
y] forall a b. (a -> b) -> a -> b
$ \Arg Term
a ->
            forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ forall a. Names -> NamesT Fail a -> a
runNames [] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" (forall a b. a -> b -> a
const (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a))
          IsNot (Arg Term
bA, Arg Term
x, Arg Term
y) -> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Arg Term
bA, Arg Term
x, Arg Term
y] forall a b. (a -> b) -> a -> b
$ \Arg Term
a ->
            forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
NoAbs String
"_" forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a)

        -- The resulting path is constant when when
        --    @Σ φ λ o → -- primIdFace p i1 o@
        -- holds. That's why cofibrations have to be closed under Σ,
        -- c.f. primDepIMin.
        Term
cof <- forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tIMin
          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
phi
          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" (\NamesT ReduceM Term
o ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
idFace forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
y forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
p NamesT ReduceM Term
io NamesT ReduceM Term
o))

        -- Do the Kan operation for our faces in the Path type.
        Term
path <- KanOperation
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
-> NamesT ReduceM Term
eval KanOperation
kanOp NamesT ReduceM Term
l
          (forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term
i -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tPathType forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT ReduceM Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT ReduceM Term
y forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i))
          NamesT ReduceM Term
phi
          (forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term
i -> forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" forall a b. (a -> b) -> a -> b
$ \NamesT ReduceM Term
o ->
            forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
idPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
y forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
i) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT ReduceM Term -> NamesT ReduceM Term -> NamesT ReduceM Term
p NamesT ReduceM Term
i NamesT ReduceM Term
o))
          (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
idPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
iz) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
iz) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
iz) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
y forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
iz) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
p0)

        NamesT ReduceM Term
conId forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT ReduceM Term
y forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT ReduceM Term
io)
          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
cof
          forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
path
    Maybe QName
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing