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 _β‘_ #-}