{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

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

  , primGlue'
  , prim_glue'
  , prim_unglue'
  )
  where

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

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

import Agda.Syntax.Common
  ( Hiding(..), Cubical(..), Arg(..)
  , ConOrigin(..), ProjOrigin(..)
  , Relevance(..)
  , setRelevance
  , setHiding
  )
import Agda.Syntax.Internal

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

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

import Agda.Utils.Impossible
  ( __IMPOSSIBLE__ )

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

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

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

  forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ do
    [NamesT m Term
psi, NamesT m Term
u, NamesT m Term
u0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
psi, Arg Term
u, Arg Term
u0]
    [NamesT m Term
la, NamesT m Term
lb, NamesT m Term
bA, NamesT m Term
phi, NamesT m Term
bT, NamesT m Term
e] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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) [Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e]

    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
headStop TermPosition
tpos NamesT m Term
phi) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    let
      tf :: NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o   = forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
hfill NamesT m Term
lb (NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) NamesT m Term
psi NamesT m Term
u NamesT m Term
u0 NamesT m Term
i
      unglue :: NamesT m Term -> NamesT m Term
unglue NamesT m Term
g = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tunglue forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
e forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
g

      a1 :: NamesT m Term
a1 = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tHComp forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m 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
"i" (\NamesT m Term
i -> forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys NamesT m Term
la NamesT m Term
bA
            [ (NamesT m Term
psi, forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" (\NamesT m Term
o -> NamesT m Term -> NamesT m Term
unglue (NamesT m Term
u forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o)))
            , (NamesT m Term
phi, forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" (\NamesT m Term
o -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tEFun forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> (NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term
e forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o))
            ])
        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term -> NamesT m Term
unglue NamesT m Term
u0

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

    case TermPosition
tpos of
      TermPosition
Head       -> NamesT m Term -> NamesT m Term
t1 (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tItIsOne)
      TermPosition
Eliminated -> NamesT m Term
a1

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

    NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
gcomp <- forall (m :: * -> *).
HasBuiltins m =>
String
-> NamesT
     m
     (NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term
      -> NamesT m Term)
mkGComp String
localUse

    -- transpFill: transp (λ j → bA (i ∧ j)) (φ ∨ ~ i) u0
    -- connects u0 and transp bA i0 u0
    let transpFill :: NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
transpFill NamesT m Term
la NamesT m Term
bA NamesT m Term
phi NamesT m Term
u0 NamesT m Term
i =
          forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
tTrans 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
"j" (\ NamesT m Term
j -> NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j)
                      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
"j" (\ NamesT m Term
j -> NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imin NamesT m Term
i NamesT m Term
j)
                      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
phi (forall (m :: * -> *). HasBuiltins m => m Term -> m Term
ineg NamesT m Term
i))
                      forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
u0
    [NamesT m Term
psi,NamesT m Term
u0] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
psi,Arg Term
u0]

    -- glue1 t a = glue la[i1/i] lb[i1/i] bA[i1/i] phi[i1/i] bT[i1/i] e[i1/i] t a
    NamesT m Term -> NamesT m Term -> NamesT m Term
glue1 <- do
      NamesT m Term
g <- forall (m :: * -> *) a.
(MonadFail m, Subst a) =>
a -> NamesT m (NamesT m a)
open forall a b. (a -> b) -> a -> b
$ (Term
tglue forall t. Apply t => t -> [Arg Term] -> t
`apply`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map ((forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 Term
io)) forall a b. (a -> b) -> a -> b
$ [Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e]
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ NamesT m Term
t NamesT m Term
a -> NamesT m Term
g forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
t forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
a

    [NamesT m Term
la, NamesT m Term
lb, NamesT m Term
bA, NamesT m Term
phi, NamesT m Term
bT, NamesT m Term
e] <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Arg Term
a -> 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 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))) [Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e]

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

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

    Term -> IntervalView
view <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'

    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *). PureTCM m => TermPosition -> m Term -> m Bool
headStop TermPosition
tpos (NamesT m Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)) (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    let
      tf :: NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o = NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
transpFill NamesT m Term
lb (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 m Term
i -> NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) NamesT m Term
psi NamesT m Term
u0 NamesT m Term
i
      t1 :: NamesT m Term -> NamesT m Term
t1 NamesT m Term
o = NamesT m Term -> NamesT m Term -> NamesT m Term
tf (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
o

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

      -- a1 with gcomp
      -- a1 = gcomp (ψ ∨ (∀ i. φ)) (λ { i (ψ = i1) → unglue_u0 i ; i ((∀ i. φ) = i1) → equivFun ... })
      --        (unglue_u0 i0)
      a1 :: NamesT m Term
a1 = NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
gcomp NamesT m Term
la NamesT m Term
bA (forall (m :: * -> *). HasBuiltins m => m Term -> m Term -> m Term
imax NamesT m Term
psi NamesT m Term
forallphi)
        (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 m Term
i -> forall (m :: * -> *).
HasBuiltins m =>
NamesT m Term
-> NamesT m Term
-> [(NamesT m Term, NamesT m Term)]
-> NamesT m Term
combineSys (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i) (NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT m Term
i)
          [ (NamesT m Term
psi,       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 m Term
_ -> NamesT m Term -> NamesT m Term
unglue_u0 NamesT m Term
i)
          , (NamesT m Term
forallphi, 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 m Term
o -> NamesT m Term -> NamesT m Term -> NamesT m Term
w NamesT m Term
i NamesT m Term
o forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT m Term -> NamesT m Term -> NamesT m Term
tf NamesT m Term
i NamesT m Term
o))
          ])
        (NamesT m Term -> NamesT m Term
unglue_u0 (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
iz))

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

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

      -- Type of fibres of the partial equivalence over a1.
      fiberT :: NamesT m Term -> NamesT m Term
fiberT NamesT m Term
o = forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
-> NamesT m Term
fiber (NamesT m Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) (NamesT m Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
        (NamesT m Term
bT forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<..> NamesT m Term
o) (NamesT m Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io)
        (NamesT m Term -> NamesT m Term -> NamesT m Term
w (forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
io) NamesT m Term
o)
        NamesT m Term
a1

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

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

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

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

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

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

  -- Takes a partial element of @t : T@ and an element of the base type @A@
  -- which extends @e t@, and makes it into a Glue.
  Term -> IntervalView
view <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  Term
one <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne
  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
-> Int
-> ([Arg Term] -> ReduceM (Reduced MaybeReducedArgs Term))
-> PrimFun
primFun forall a. HasCallStack => a
__IMPOSSIBLE__ Int
8 forall a b. (a -> b) -> a -> b
$ \case
    [Arg Term
la, Arg Term
lb, Arg Term
bA, Arg Term
phi, Arg Term
bT, Arg Term
e, Arg Term
t, Arg Term
a] -> do
      Blocked (Arg Term)
sphi <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
phi
      -- When @φ = 1@ then @t : T@ is totally defined.
      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 forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sphi of
        IntervalView
IOne -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
t forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall e. e -> Arg e
argN Term
one]
        -- Otherwise we'll just wait to get unglued.
        IntervalView
_    -> forall (m :: * -> *) a. Monad m => a -> m a
return (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
la,Arg Term
lb,Arg Term
bA] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
e,Arg Term
t,Arg Term
a])
    [Arg Term]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

        -- Otherwise we're dealing with a proper glued thing.
        -- Definitely a sticky situation!
        IntervalView
_    -> do
          Blocked (Arg Term)
sb <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
b
          let fallback :: Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback Blocked (Arg Term)
sbA = forall (m :: * -> *) a. Monad m => a -> m a
return (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
la,Arg Term
lb] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced [Blocked (Arg Term)
sbA, Blocked (Arg Term)
sphi] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
e] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sb])
          case forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking forall a b. (a -> b) -> a -> b
$ Blocked (Arg Term)
sb of
            -- Case 1: unglue (glue a) = a. This agrees with the @φ =
            -- i1@ reduction because under @φ@, the argument to
            -- @glue@ must be in the image of the equivalence.
            Def QName
q Elims
es
              | Just [Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
_, Arg Term
a] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
              , forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mglue -> forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a

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

            -- Case 3: unglue (hcomp u u0).
            -- Defer to the implementation of @doGlueKanOp DoHComp ... Eliminated@: It knows how to unglue itself.
            Def QName
q [Apply Arg Term
l,Apply Arg Term
bA,Apply Arg Term
r,Apply Arg Term
u,Apply Arg Term
u0] | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mhcomp -> do
              Blocked (Arg Term)
sbA <- forall t. Reduce t => t -> ReduceM (Blocked t)
reduceB' Arg Term
bA
              case forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ forall t a. Blocked' t a -> a
ignoreBlocking Blocked (Arg Term)
sbA of
                -- Idem: use the Glue data from the type we're doing
                -- hcomp in.
                Def QName
g Elims
es | Just [Arg Term
la', Arg Term
lb', Arg Term
bA', Arg Term
phi', Arg Term
bT', Arg Term
e'] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, forall a. a -> Maybe a
Just QName
g forall a. Eq a => a -> a -> Bool
== Maybe QName
mGlue -> do
                  forall a a'. a -> ReduceM (Reduced a' a)
redReturn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
                    forall (m :: * -> *).
PureTCM m =>
KanOperation
-> FamilyOrNot
     (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)
-> TermPosition
-> m (Maybe Term)
doGlueKanOp (Blocked (Arg Term) -> Arg Term -> Arg Term -> KanOperation
HCompOp (forall a t. a -> Blocked' t a
notBlocked Arg Term
r) Arg Term
u Arg Term
u0) (forall a. a -> FamilyOrNot a
IsNot (Arg Term
la',Arg Term
lb',Arg Term
bA',Arg Term
phi',Arg Term
bT',Arg Term
e')) TermPosition
Eliminated
                Term
_ -> Blocked (Arg Term) -> ReduceM (Reduced MaybeReducedArgs Term)
fallback Blocked (Arg Term)
sbA

            Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (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
la,Arg Term
lb,Arg Term
bA] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sphi] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> MaybeReduced a
notReduced [Arg Term
bT,Arg Term
e] forall a. [a] -> [a] -> [a]
++ [Blocked (Arg Term) -> MaybeReduced (Arg Term)
reduced Blocked (Arg Term)
sb])
    [Arg Term]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__