Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

affine_traversal_ty

AffineTraversal : Type → Type → Type

algebraic_effect_ty

AlgebraicEffect : Type → Type → Type

ana_ty

Ana : (A → F A) → A → Fix F (anamorphism type template)

app

app2

app3

applicative_law_ty

ApplicativeLaw : (Type → Type) → Type → Prop

applicative_ty

Applicative : (Type → Type) → Type

approximation_order_ty

ApproximationOrder : Type → Type → Prop

arrow

arrow_apply_ty

ArrowApply : Type → Type → Type

arrow_choice_ty

ArrowChoice : Type → Type → Type

arrow_first_ty

ArrowFirst : Type → Type → Type → Type

arrow_law_ty

ArrowLaw : Type → Type → Prop

arrow_ty

Arrow : Type → Type → Type

banach_fixed_point_ty

BanachFixedPoint : Type → Type → Prop

build_env

Build the functional programming foundations environment: register all axioms.

bvar

cata_ty

Cata : (F A → A) → Fix F → A (catamorphism type template)

catamorphism_fusion_ty

CatamorphismFusion : ∀ (F : Type → Type) (A B : Type), Prop

catamorphism_ty

Catamorphism : (Type → Type) → Type → Type

cellular_automata_comonad_ty

CellularAutomataComonad : Type → Type

chronomorphism_ty

Chronomorphism : (Type → Type) → Type → Type

coerce_ty

Coerce : Type → Type → Prop

cofree_comonad_unfold_ty

CofreeComonadUnfold : ∀ (F : Type → Type) (A : Type), Prop

cofree_ty

Cofree : (Type → Type) → Type → Type

comonad_law_ty

ComonadLaw : (Type → Type) → Type → Prop

comonad_ty

Comonad : (Type → Type) → Type

cont_t_ty

ContT : Type → (Type → Type) → Type → Type

cps_transform_ty

CpsTransform : Type → Type → Type

cst

day_convolution_ty

DayConvolution : (Type → Type) → (Type → Type) → Type → Type

deep_handler_ty

DeepHandler : Type → Type → Type → Type

dimap_ty

Dimap : ∀ (P : Type → Type → Type) (A B C D : Type), Prop

double_negation_translation_ty

DoubleNegationTranslation : Type → Prop

effect_handler_ty

EffectHandler : Type → Type → Type → Type

effect_row_ty

EffectRow : Type

effect_subrow_ty

EffectSubrow : Type → Type → Prop

effect_ty

Effect : Type → Type → Type

final_coalgebra_ty

FinalCoalgebra : (Type → Type) → Type → Prop

fixed_point_semantics_ty

FixedPointSemantics : (Type → Type) → Type → Prop

fixpoint_ty

FixPoint : (Type → Type) → Type

fixpoint_type_ty

FixpointType : (Type → Type) → Type

fn_ty

free_applicative_ty

FreeApplicative : (Type → Type) → Type → Type

free_monad_bind_ty

FreeMonadBind : ∀ (F : Type → Type) (A B : Type), Prop

free_monad_left_unit_ty

FreeMonadLeftUnit : ∀ (F : Type → Type) (A : Type), Prop

free_monad_right_unit_ty

FreeMonadRightUnit : ∀ (F : Type → Type) (A : Type), Prop

free_monad_ty

FreeMonad : (Type → Type) → Type → Type

free_selective_ty

FreeSelective : (Type → Type) → Type → Type

freer_lift_ty

FreerLift : ∀ (F : Type → Type) (A : Type), F A → FreerMonad F A

freer_monad_ty

FreerMonad : (Type → Type) → Type → Type

full_abstraction_ty

FullAbstraction : Type → Type → Prop

futumorphism_ty

Futumorphism : (Type → Type) → Type → Type

histomorphism_ty

Histomorphism : (Type → Type) → Type → Type

hlist_ty

HList : Type

hmap_ty

HMap : Type → Type → Type

hylo_fusion_ty

HyloFusion : ∀ (F : Type → Type) (A B : Type), Prop

hylo_ty

Hylo : (F B → B) → (A → F A) → A → B (hylomorphism)

hylomorphism_ty

Hylomorphism : (Type → Type) → Type → Type → Type

idiom_bracket_ty

IdiomBracket : (Type → Type) → Type → Type

initial_algebra_ty

InitialAlgebra : (Type → Type) → Type → Prop

iso_roundtrip_ty

IsoRoundtrip : ∀ (S A : Type), Iso S A → Prop

iso_ty

Iso : Type → Type → Type

least_upper_bound_ty

LeastUpperBound : Type → Type → Prop

lens_get_set_ty

LensGetSet : ∀ (S A : Type), Lens S A → Prop

lens_set_get_ty

LensSetGet : ∀ (S A : Type), Lens S A → Prop

lens_set_set_ty

LensSetSet : ∀ (S A : Type), Lens S A → Prop

lens_ty

Lens : Type → Type → Type

linear_type_ty

LinearType : Type → Type

linearity_law_ty

LinearityLaw : Type → Prop

list_ana

An anamorphism (unfold) producing a list from a seed.

list_cata

A catamorphism (fold) over a list as a stand-in for Fix F.

list_hylo

A hylomorphism (fold ∘ unfold) without materialising the intermediate structure.

list_para

A paramorphism over a list (extended fold with original tail access).

mu_ty

Mu : (Type → Type) → Type

nu_ty

Nu : (Type → Type) → Type

paramorphism_ty

Paramorphism : (Type → Type) → Type → Type

pi

prism_law_ty

PrismLaw : ∀ (S A : Type), Prism S A → Prop

prism_ty

Prism : Type → Type → Type

profunctor_optic_ty

ProfunctorOpticTy : Type → Type → Type → Type → Type

profunctor_ty

Profunctor : Type → Type → Type

prop

reset_ty

Reset : Type → Type → Type

scoped_effect_ty

ScopedEffect : Type → Type → Type

scott_continuous_ty

ScottContinuous : Type → Type → Prop

scott_domain_ty

ScottDomain : Type

shallow_handler_ty

ShallowHandler : Type → Type → Type → Type

shift_ty

Shift : Type → Type → Type

singleton_ty

Singleton : Type → Type

stream_comonad_ty

StreamComonad : Type → Type

strong_profunctor_ty

StrongProfunctor : Type → Type → Type

tambara_module_ty

TambaraModule : Type → Type → Type

traversal_compose_ty

TraversalCompose : ∀ (S A : Type), Traversal S A → Prop

traversal_ty

Traversal : Type → Type → Type

type0

type_equality_ty

TypeEquality : Type → Type → Prop

unique_type_ty

UniqueType : Type → Type

uniqueness_law_ty

UniquenessLaw : Type → Prop

van_laarhoven_lens_ty

VanLaarhovenLens : Type → Type → Type