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 Ο† u = X.primHComp (Ξ» j .o β†’ u j (leftIs1 Ο† (~ j) o)) (u i0 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.primComp A (Ξ» j .o β†’ u j (leftIs1 Ο† (~ j) o)) (u i0 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_ #-}