-- | 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 Control.Monad.Except

import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Monad

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

import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Substitute (apply, sort, listS, applySubst)
import Agda.TypeChecking.Reduce (reduceB', reduce')
import Agda.TypeChecking.Names
  (runNamesT, runNames, cl, lam, ilam, open)

import Agda.Interaction.Options.Base (optCubical)

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

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

import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Debug (__IMPOSSIBLE_VERBOSE__)

import Agda.TypeChecking.Primitive.Cubical.Base

-- | 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 :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
builtinConId String
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 :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' String
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 :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' String
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 :: String -> ReduceM Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => String -> String -> 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]
++ String
builtinId

  IntervalView -> Term
unview <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
  Maybe QName
mConId <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' String
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    <- String -> ReduceM Term
getTermLocal String
builtinHComp
      Term
tTrans    <- String -> ReduceM Term
getTermLocal String
builtinTrans
      Term
tIMin     <- String -> ReduceM Term
getTermLocal String
"primDepIMin"
      Term
idFace    <- String -> ReduceM Term
getTermLocal String
"primIdFace"
      Term
idPath    <- String -> ReduceM Term
getTermLocal String
"primIdPath"
      Term
tPathType <- String -> ReduceM Term
getTermLocal String
builtinPath
      Term
tConId    <- String -> ReduceM Term
getTermLocal String
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