open import Prim.Extension
open import Prim.Interval
open import Prim.Type

module Prim.Kan where

Primitive: Kan operationsπŸ”—

Using the machinery from the other Prim modules, we can define the Kan operations: transport and composition.

private module X where primitive
  primTransp : βˆ€ {β„“} (A : (i : I) β†’ Type (β„“ i)) (Ο† : I) (a : A i0) β†’ A i1
  primHComp  : βˆ€ {β„“} {A : Type β„“} {Ο† : I} (u : βˆ€ i β†’ Partial Ο† A) (a : A) β†’ A
  primComp : βˆ€ {β„“} (A : (i : I) β†’ Type (β„“ i)) {Ο† : I} (u : βˆ€ i β†’ Partial Ο† (A i)) (a : A i0) β†’ A i1

open X public renaming (primTransp to transp)

hcomp
  : βˆ€ {β„“} {A : Type β„“} (Ο† : I)
  β†’ (u : (i : I) β†’ Partial (Ο† ∨ ~ i) A)
  β†’ A
hcomp {A = A} Ο† u = X.primHComp sys (u i0 1=1) module hcomp-sys where
  sys : βˆ€ j β†’ Partial Ο† A
  sys j (Ο† = i1) = u j 1=1

βˆ‚ : I β†’ I
βˆ‚ i = i ∨ ~ i

comp
  : βˆ€ {β„“ : I β†’ Level} (A : (i : I) β†’ Type (β„“ i)) (Ο† : I)
  β†’ (u : (i : I) β†’ Partial (Ο† ∨ ~ i) (A i))
  β†’ A i1
comp A Ο† u = X.primHComp sys (transp (Ξ» i β†’ A i) i0 (u i0 1=1)) module comp-sys where
  sys : βˆ€ j β†’ Partial Ο† (A i1)
  sys i (Ο† = i1) = transp (Ξ» j β†’ A (i ∨ j)) i (u i 1=1)

We also define the type of dependent paths, and of non-dependent paths.

postulate
  PathP : βˆ€ {β„“} (A : I β†’ Type β„“) β†’ A i0 β†’ A i1 β†’ Type β„“

{-# BUILTIN PATHP PathP #-}

infix 7 _≑_

_≑_ : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ A β†’ Type β„“
_≑_ {A = A} = PathP (Ξ» i β†’ A)

{-# BUILTIN PATH _≑_ #-}

{-# BUILTIN REWRITE _≑_ #-}

caseⁱ_of_ : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} (x : A) β†’ ((y : A) β†’ x ≑ y β†’ B) β†’ B
caseⁱ x of f = f x (Ξ» i β†’ x)

caseⁱ_return_of_ : βˆ€ {β„“ β„“'} {A : Type β„“} (x : A) (P : A β†’ Type β„“') β†’ ((y : A) β†’ x ≑ y β†’ P y) β†’ P x
caseⁱ x return P of f = f x (Ξ» i β†’ x)

{-# INLINE caseⁱ_of_ #-}
{-# INLINE caseⁱ_return_of_ #-}

{-# DISPLAY X.primHComp {β„“} {A} {Ο†} (hcomp-sys.sys _ u) _ = hcomp {β„“} {A} Ο† u #-}
{-# DISPLAY X.primHComp {_} {_} {Ο†} (comp-sys.sys A _ u) _ = comp A Ο† u #-}