ITree.Indexed.Function

The Category of Indexed Functions

Indexed functions have type E ~> F, i.e., forall T, E T -> F T, for some E and F. Like regular functions (Basics.Function), they form a cocartesian category.


The name of the category.
Definition IFun (E F : Type -> Type) : Type := E ~> F.

Unwrap IFun, potentially useful for type inference.
Definition apply_IFun {E F T} (f : IFun E F) : E T -> F T := f T.

Unwrap IFun as ~>.
Definition apply_IFun' {E F} (f : IFun E F) : E ~> F := f.

Wrap ~> as IFun.
Definition as_IFun {E F} (f : E ~> F) : IFun E F := f.

Equivalence of indexed functions is extensional equality.
#[global]
Instance Eq2_IFun : Eq2 IFun :=
  fun E F => i_pointwise (fun T => @eq (F T)).

The identity function.
#[global]
Instance Id_IFun : Id_ IFun :=
  fun E _ e => e.

Function composition.
#[global]
Instance Cat_IFun : Cat IFun :=
  fun E F G f1 f2 R e => f2 _ (f1 _ e).

void1 is the initial object.
#[global]
Instance Initial_void1 : Initial IFun void1 := @elim_void1.

The coproduct is case analysis on sums.
Definition case_sum1 {A B C : Type -> Type} (f : A ~> C) (g : B ~> C)
  : A +' B ~> C
  := fun _ ab =>
       match ab with
       | inl1 a => f _ a
       | inr1 b => g _ b
       end.

#[global]
Instance Case_sum1 : Case IFun sum1 := @case_sum1.
#[global]
Instance Inl_sum1 : Inl IFun sum1 := @inl1.
#[global]
Instance Inr_sum1 : Inr IFun sum1 := @inr1.