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 4 _≑_

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

_≑_ : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ A β†’ Type β„“
_≑_ {A = A} = Path A

{-# BUILTIN PATH _≑_ #-}