Module `Catt.Functorialisation`Source

Source

val coh_depth1 : 
  (Kernel.Coh.t ->
    Common.Var.t list ->
    Unchecked_types.Unchecked_types(Kernel.Coh).tm
    * Unchecked_types.Unchecked_types(Kernel.Coh).ctx)
    ref

Source

val preimage : 
  Unchecked_types.Unchecked_types(Kernel.Coh).ctx ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps ->
  Common.Var.t list ->
  Common.Var.t list

Source

val tgt_subst : 
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub

Source

val coh : 
  Kernel.Coh.t ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm
  * Unchecked_types.Unchecked_types(Kernel.Coh).ctx

Source

val coh_successively : 
  Kernel.Coh.t ->
  (Common.Var.t * int) list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm
  * Unchecked_types.Unchecked_types(Kernel.Coh).ctx

Sourceval coh_depth0 : Kernel.Coh.t -> Common.Var.t list -> Kernel.Coh.t

Sourceval coh_all : Kernel.Coh.t -> Kernel.Coh.t

Source

val tm_one_step_tm : 
  Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm

Source

val ty : 
  Unchecked_types.Unchecked_types(Kernel.Coh).ty ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
  Unchecked_types.Unchecked_types(Kernel.Coh).ty

Source

val ctx : 
  Unchecked_types.Unchecked_types(Kernel.Coh).ctx ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).ctx

Source

val sub_ps : 
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps

Source

val tm : 
  Unchecked_types.Unchecked_types(Kernel.Coh).ctx ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
  (Common.Var.t * int) list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm
  * Unchecked_types.Unchecked_types(Kernel.Coh).ctx

Source

val ps : 
  Common.ps ->
  Common.Var.t list ->
  Common.ps * (Common.Var.t * int) list

Source

val sub : 
  Unchecked_types.Unchecked_types(Kernel.Coh).sub ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub

Source

val sub_w_tgt : 
  Common.ps ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps ->
  Common.Var.t list ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps
  * Common.ps
  * (Common.Var.t * int) list
  * Common.Var.t list

Source

val whisk_sub_ps : 
  int ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
  Unchecked_types.Unchecked_types(Kernel.Coh).ty ->
  Unchecked_types.Unchecked_types(Kernel.Coh).tm ->
  Unchecked_types.Unchecked_types(Kernel.Coh).ty ->
  Unchecked_types.Unchecked_types(Kernel.Coh).sub_ps

package catt

Module Catt.FunctorialisationSource

Module `Catt.Functorialisation`Source