instance sigma

typeside t
schema s1 : t
schema s2 : t
mapping m : s1 -> s2
instance i : s1
----------------------------------
instance (sigma m i) : s2

Performs a left kan extension. Operationally, each generator g of entity e becomes translated to the target schema as a generator of entity f(e), where f is the mapping. Hence sigma can be thought of as substitution along a theory morphism.

Appears in:

All_Syntax
Dataversity
Delta
Demo
Dopfib
FinanceColim1
Inverse
LambdaConf
NewDemo
NewDemoPsuedo
OuterJoin
Petri
PharmaColim2
Quotient
Sigma
Tutorial
vsSQL2

Options:

allow_empty_sorts_unsafe
allow_java_eqs_unsafe
always_reload
completion_compose
completion_filter_subsumed
completion_precedence
completion_sort
completion_syntactic_ac
completion_unfailing
dont_verify_is_appropriate_for_prover_unsafe
e_path
e_use_auto
maedmax_path
num_threads
program_allow_nonconfluence_unsafe
program_allow_nontermination_unsafe
prover
prover_simplify_max
require_consistency
second_prover
talg_reduction
timeout
triviality_check_best_effort
vampire_path