Kan (cooltt.Core.TermBuilder.Kan)

type coe = r:t m -> r':t m -> bdy:t m -> t m

type hcom = r:t m -> r':t m -> phi:t m -> bdy:t m -> t m

val coe_pi : base_line:t m -> fam_line:t m -> coe

val hcom_pi : fam:t m -> hcom

val coe_sg : base_line:t m -> fam_line:t m -> coe

val hcom_sg : base:t m -> fam:t m -> hcom

val hcom_ext : n:int -> cof:t m -> fam:t m -> bdry:t m -> hcom

val coe_ext : n:int -> cof:t m -> fam_line:t m -> bdry_line:t m -> coe

module V : sig ... end

module FHCom : sig ... end