{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Primitive.Cubical.Glue
  ( mkGComp
  , doGlueKanOp

  , primGlue'
  , prim_glue'
  , prim_unglue'
  )
  where

import Control.Monad.Except

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

import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Pure
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Substitute (absBody, apply, sort, subst, applyE)
import Agda.TypeChecking.Reduce (reduceB', reduce')
import Agda.TypeChecking.Names (NamesT, runNamesT, runNames, cl, lam, open, ilam)

import Agda.Interaction.Options.Base (optCubical)

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

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

import Agda.Syntax.Internal
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.TypeChecking.Monad.Debug (__IMPOSSIBLE_VERBOSE__)

import Agda.TypeChecking.Primitive.Cubical.Base

-- | 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 :: 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 :: String -> NamesT m Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
s
  Term
tPOr <- String -> NamesT m Term
getTermLocal String
"primPOr"
  Term
tIMax <- String -> NamesT m Term
getTermLocal String
builtinIMax
  Term
tIMin <- String -> NamesT m Term
getTermLocal String
builtinIMin
  Term
tINeg <- String -> NamesT m Term
getTermLocal String
builtinINeg
  Term
tHComp <- String -> NamesT m Term
getTermLocal String
builtinHComp
  Term
tTrans <- String -> NamesT m Term
getTermLocal String
builtinTrans
  Term
io      <- String -> NamesT m Term
getTermLocal String
builtinIOne
  Term
iz      <- String -> NamesT m Term
getTermLocal String
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
  :: 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 :: String -> m Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm forall a b. (a -> b) -> a -> b
$ String
builtinHComp forall a. [a] -> [a] -> [a]
++ String
" for " forall a. [a] -> [a] -> [a]
++ String
builtinGlue
  Term
tHComp   <- String -> m Term
getTermLocal String
builtinHComp
  Term
tEFun    <- String -> m Term
getTermLocal String
builtinEquivFun
  Term
tglue    <- String -> m Term
getTermLocal String
builtin_glue
  Term
tunglue  <- String -> m Term
getTermLocal String
builtin_unglue
  Term
io       <- String -> m Term
getTermLocal String
builtinIOne
  Term
tItIsOne <- String -> m Term
getTermLocal String
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 = String
builtinTrans forall a. [a] -> [a] -> [a]
++ String
" for " forall a. [a] -> [a] -> [a]
++ String
builtinGlue
    getTermLocal :: String -> m Term
getTermLocal = forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
localUse
  Term
tHComp <- String -> m Term
getTermLocal String
builtinHComp
  Term
tTrans <- String -> m Term
getTermLocal String
builtinTrans
  Term
tForall <- String -> m Term
getTermLocal String
builtinFaceForall
  Term
tEFun   <- String -> m Term
getTermLocal String
builtinEquivFun
  Term
tEProof <- String -> m Term
getTermLocal String
builtinEquivProof
  Term
toutS   <- String -> m Term
getTermLocal String
builtinSubOut
  Term
tglue   <- String -> m Term
getTermLocal String
builtin_glue
  Term
tunglue <- String -> m Term
getTermLocal String
builtin_unglue
  Term
io      <- String -> m Term
getTermLocal String
builtinIOne
  Term
iz      <- String -> m Term
getTermLocal String
builtinIZero
  Term
tLMax   <- String -> m Term
getTermLocal String
builtinLevelMax
  Term
tTransp <- String -> m Term
getTermLocal String
builtinTranspProof
  Term
tItIsOne <- String -> m Term
getTermLocal String
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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 => String -> m (Maybe QName)
getPrimitiveName' String
builtinGlue
  Maybe QName
mglue <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
builtin_glue
  Maybe QName
mtransp <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
builtinTrans
  Maybe QName
mhcomp <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
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 :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
builtin_unglue String
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__