| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1380 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (68 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (137 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (51 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (311 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (77 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (241 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (495 entries) |
Global Index
A
absIdx [definition, in Modules.SoftEquations.Examples.LCBetaEta]abs_app_halfeq [lemma, in Modules.SoftEquations.Examples.LCBetaEta]
ab_epi2 [lemma, in Modules.Signatures.EpiSigRepresentability]
action_sig_over_mor [definition, in Modules.SoftEquations.SignatureOver]
AdjunctionEquationRep [library]
adj_law2 [lemma, in Modules.Prelims.deriveadj]
adj_law1 [lemma, in Modules.Prelims.deriveadj]
adj1 [definition, in Modules.Prelims.deriveadj]
algebraic_model_Epi [lemma, in Modules.Signatures.BindingSig]
algebraic_sig_initial [definition, in Modules.Signatures.BindingSig]
algebraic_sig_effective [lemma, in Modules.Signatures.BindingSig]
algSig_NatEpi [lemma, in Modules.Signatures.PreservesEpi]
alg_initialR [definition, in Modules.Signatures.BindingSig]
all_purpose [section, in Modules.Signatures.EpiSigRepresentability]
appIdx [definition, in Modules.SoftEquations.Examples.LCBetaEta]
ArAreEpiEpiSig [lemma, in Modules.Signatures.BindingSig]
ArAreEpiSig [lemma, in Modules.Signatures.BindingSig]
arity_abs_eq [lemma, in Modules.SoftEquations.Examples.LCBetaEta]
arity_abs_mod_eq_mult [lemma, in Modules.SoftEquations.Examples.LCBetaEta]
arity_abs [definition, in Modules.SoftEquations.Examples.LCBetaEta]
arity_to_one_sigHSET [definition, in Modules.Signatures.BindingSig]
Arity_to_SignatureHSET [definition, in Modules.Signatures.BindingSig]
arity_to_one_sig [definition, in Modules.Signatures.BindingSig]
ArToSig [abbreviation, in Modules.Signatures.BindingSig]
assoc_ppprojR [lemma, in Modules.Prelims.quotientmonad]
B
BC [abbreviation, in Modules.Signatures.ModelCat]BC [abbreviation, in Modules.SoftEquations.Summary]
BC [abbreviation, in Modules.SoftEquations.quotientequation]
bcO [abbreviation, in Modules.Signatures.ModelCat]
BCP [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]
bcpS [abbreviation, in Modules.Prelims.deriveadj]
bcpS [abbreviation, in Modules.Prelims.deriveadj]
beta_eta_equations [definition, in Modules.SoftEquations.Examples.LCBetaEta]
beta_equation [definition, in Modules.SoftEquations.Examples.LCBetaEta]
beta_sig_source [definition, in Modules.SoftEquations.Examples.LCBetaEta]
BinCoproductComplements [library]
BinCoproducts_from_CoproductsBool [definition, in Modules.Prelims.BinCoproductComplements]
bincoproduct_Epis [lemma, in Modules.Prelims.EpiComplements]
BindingSig [library]
BindingSig [library]
BindingSigAreEpiEpiSig [lemma, in Modules.Signatures.BindingSig]
BindingSigAreEpiSig [lemma, in Modules.Signatures.BindingSig]
bindingSigHSET_Initial [definition, in Modules.SoftEquations.BindingSig]
BindingSigIndexhSet [definition, in Modules.Signatures.BindingSig]
BindingSigIndexhSet_coprod [definition, in Modules.Signatures.BindingSig]
BindingSigOp [section, in Modules.SoftEquations.Examples.LCBetaEta]
_ ×× _ [notation, in Modules.SoftEquations.Examples.LCBetaEta]
∂ [notation, in Modules.SoftEquations.Examples.LCBetaEta]
bindingSig_op_to_sig_morHSET [definition, in Modules.SoftEquations.BindingSig]
bindingSig_op_to_sig_mor [definition, in Modules.SoftEquations.BindingSig]
BindingSig_on_model_isEpi [lemma, in Modules.Signatures.BindingSig]
binding_Sig_iso [definition, in Modules.Signatures.BindingSig]
binding_to_one_sigHSET [definition, in Modules.Signatures.BindingSig]
binding_to_one_sig [definition, in Modules.Signatures.BindingSig]
Binprod [section, in Modules.Signatures.SignatureBinproducts]
Binprod [section, in Modules.SoftEquations.SignatureOverBinproducts]
BinProdComplements [section, in Modules.Prelims.BinProductComplements]
binProdFunc [abbreviation, in Modules.Signatures.BindingSig]
binProdSig [abbreviation, in Modules.Signatures.BindingSig]
BinProductComplements [library]
BinProductsLModule [section, in Modules.Prelims.LModulesBinProducts]
BinProductWith1_iso [definition, in Modules.Prelims.BinProductComplements]
BinProductWith1_is_inverse [lemma, in Modules.Prelims.BinProductComplements]
BinProduct_pw_iso [definition, in Modules.Prelims.BinProductComplements]
BinProduct_pw_iso_is_inverse [definition, in Modules.Prelims.BinProductComplements]
BinProduct_pw_eq_id [lemma, in Modules.Prelims.BinProductComplements]
BinProduct_pw_iso_mor [definition, in Modules.Prelims.BinProductComplements]
BinProduct_commutative_iso [definition, in Modules.Prelims.BinProductComplements]
BinProduct_commutative_id_commute [lemma, in Modules.Prelims.BinProductComplements]
BinProduct_commutative [definition, in Modules.Prelims.BinProductComplements]
binprod_sigs_har_iso [definition, in Modules.Signatures.HssSignatureCommutation]
binprod_sigs_har_eq [lemma, in Modules.Signatures.HssSignatureCommutation]
binprod_sigs_har_mod_eq_mult [lemma, in Modules.Signatures.HssSignatureCommutation]
binprod_pbm_to_pbm_binprod [definition, in Modules.Prelims.LModulesBinProducts]
binprod_pbm_to_pbm_iso [definition, in Modules.Prelims.LModulesBinProducts]
binprod_pbm_to_pbm_eq_mult [lemma, in Modules.Prelims.LModulesBinProducts]
binprod_pbm [definition, in Modules.Prelims.LModulesBinProducts]
binProd_epiSigSET [definition, in Modules.Signatures.PreservesEpi]
binProd_epiSig [lemma, in Modules.Signatures.PreservesEpi]
Binprod.ab [variable, in Modules.Signatures.SignatureBinproducts]
Binprod.ab [variable, in Modules.SoftEquations.SignatureOverBinproducts]
Binprod.cpFunc [variable, in Modules.Signatures.SignatureBinproducts]
Binprod.cpFunc [variable, in Modules.SoftEquations.SignatureOverBinproducts]
Binprod.cpLM [variable, in Modules.Signatures.SignatureBinproducts]
Binprod.cpLM [variable, in Modules.SoftEquations.SignatureOverBinproducts]
BMOD [abbreviation, in Modules.Signatures.Signature]
BMOD [abbreviation, in Modules.Signatures.Signature]
bmod_disp [definition, in Modules.Prelims.LModulesFibration]
bmod_axioms [lemma, in Modules.Prelims.LModulesFibration]
bmod_transport [lemma, in Modules.Prelims.LModulesFibration]
bmod_data [definition, in Modules.Prelims.LModulesFibration]
bmod_id_comp [definition, in Modules.Prelims.LModulesFibration]
bmod_disp_ob_mor [definition, in Modules.Prelims.LModulesFibration]
BP [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]
BP [abbreviation, in Modules.Prelims.LModulesBinProducts]
bpCC [abbreviation, in Modules.Prelims.deriveadj]
bpFunc [abbreviation, in Modules.Prelims.deriveadj]
bpFunct [abbreviation, in Modules.Prelims.LModulesBinProducts]
BPO [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]
BPO [abbreviation, in Modules.Prelims.BinProductComplements]
BPO [abbreviation, in Modules.Signatures.HssSignatureCommutation]
BPO [abbreviation, in Modules.Signatures.SignatureBinproducts]
BPO [abbreviation, in Modules.Prelims.LModulesBinProducts]
BPO [abbreviation, in Modules.Prelims.CoproductsComplements]
BPO [abbreviation, in Modules.SoftEquations.SignatureOverBinproducts]
bpS [abbreviation, in Modules.Prelims.deriveadj]
bpS [abbreviation, in Modules.Prelims.deriveadj]
bp_coprod_isDistributive [definition, in Modules.Prelims.CoproductsComplements]
bp_coprod_mor [definition, in Modules.Prelims.CoproductsComplements]
bp_coprod_In [definition, in Modules.Prelims.CoproductsComplements]
C
cancel_ar_on [lemma, in Modules.Signatures.EpiSigRepresentability]catiso_modelcat_eq [definition, in Modules.SoftEquations.CatOfTwoSignatures]
catiso_modelcat [definition, in Modules.Signatures.ModelCat]
catiso_initial [lemma, in Modules.Prelims.lib]
CatOfTwoSignatures [library]
CAT_SIGNATURE [abbreviation, in Modules.Signatures.EpiSigRepresentability]
changef_path_pw [lemma, in Modules.Prelims.lib]
changef_path [lemma, in Modules.Prelims.lib]
cleaving_bmod [definition, in Modules.Prelims.LModulesFibration]
cocartesian_lifts_iso_commutes [definition, in Modules.Prelims.Opfibration]
cocartesian_lifts_iso [definition, in Modules.Prelims.Opfibration]
cocartesian_lift_is_cocartesian [definition, in Modules.Prelims.Opfibration]
cocartesian_lift [definition, in Modules.Prelims.Opfibration]
cocartesian_factorisation_commutes' [definition, in Modules.Prelims.Opfibration]
cocartesian_factorisation' [definition, in Modules.Prelims.Opfibration]
cocartesian_factorisation_unique [definition, in Modules.Prelims.Opfibration]
cocartesian_factorisation_commutes [definition, in Modules.Prelims.Opfibration]
cocartesian_factorisation [definition, in Modules.Prelims.Opfibration]
coFunc [abbreviation, in Modules.Prelims.LModulesColims]
colimOfArrows_Epi [lemma, in Modules.Prelims.EpiComplements]
ColimsModule [section, in Modules.Prelims.LModulesColims]
ColimsModule [section, in Modules.Prelims.LModulesCoproducts]
ColimsModule.d [variable, in Modules.Prelims.LModulesColims]
ColimsModule.d [variable, in Modules.Prelims.LModulesCoproducts]
ColimsSig [section, in Modules.Signatures.SignaturesColims]
ColimsSig.coMod [variable, in Modules.Signatures.SignaturesColims]
ColimsSig.d [variable, in Modules.Signatures.SignaturesColims]
ColimsSig.d' [variable, in Modules.Signatures.SignaturesColims]
ColimsSig.F [variable, in Modules.Signatures.SignaturesColims]
ColimsSig.FORGET [variable, in Modules.Signatures.SignaturesColims]
ColimsSig.F' [variable, in Modules.Signatures.SignaturesColims]
ColimsSig.hsC [variable, in Modules.Signatures.SignaturesColims]
ColimsSig.limMod [variable, in Modules.Signatures.SignaturesColims]
Colim_Functor_Preserves_Epi [lemma, in Modules.Prelims.EpiComplements]
commuteBinProdSig [section, in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.a [variable, in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.ar_b [variable, in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.ar_a [variable, in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.b [variable, in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.bpSig [variable, in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.hss_bpSig [variable, in Modules.Signatures.HssSignatureCommutation]
commutes_binproduct_derivation [definition, in Modules.Prelims.deriveadj]
commutes_binproduct_derivation_laws [lemma, in Modules.Prelims.deriveadj]
compat_μ_projR_def [definition, in Modules.Prelims.quotientmonad]
compat_μ_slice [lemma, in Modules.Prelims.quotientmonadslice]
compat_slice [lemma, in Modules.Prelims.quotientmonadslice]
compat_model_τ_projR [lemma, in Modules.Signatures.EpiSigRepresentability]
composite_preserves_Epi [definition, in Modules.Prelims.EpiComplements]
comp_cat_comp [lemma, in Modules.Prelims.lib]
cond_isEpi_hab [definition, in Modules.Signatures.EpiSigRepresentability]
congr_equivc [lemma, in Modules.Prelims.quotientmonadslice]
const_preserves_Epi [definition, in Modules.Prelims.EpiComplements]
Const1Sig_isTerminal [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
Coprod [section, in Modules.Signatures.SignatureCoproduct]
CoprodAr [section, in Modules.Signatures.HssSignatureCommutation]
CoprodAr [section, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.ars [variable, in Modules.Signatures.HssSignatureCommutation]
CoprodAr.b [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.Ba [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.bpFunct [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.bpMOD [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.bpSig [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.cpFunct [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.cpMOD [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.cpSig [variable, in Modules.Signatures.HssSignatureCommutation]
CoprodAr.cpSig [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.epiBinProd [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.epiFa [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.Fa [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.FuncBP [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.FuncCP [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.hss_cpSig [variable, in Modules.Signatures.HssSignatureCommutation]
CoprodAr.I [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.isDistC [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.MOD [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.p_alg_ar' [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.Sa' [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.sigs [variable, in Modules.Signatures.HssSignatureCommutation]
CoprodAr.Sig_cp [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.Sig_bp [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.toSig [variable, in Modules.Signatures.PresentableSignatureBinProdR]
CoprodBindingSig [section, in Modules.Signatures.BindingSig]
CoprodBindingSig.ArToSig [variable, in Modules.Signatures.BindingSig]
CoprodBindingSig.cpSig [variable, in Modules.Signatures.BindingSig]
CoprodBindingSig.CP_from_BindingSig [variable, in Modules.Signatures.BindingSig]
CoprodBindingSig.hsSig [variable, in Modules.Signatures.BindingSig]
CoprodBindingSig.toSig [variable, in Modules.Signatures.BindingSig]
CoprodBinprod [section, in Modules.Prelims.CoproductsComplements]
CoprodEpis [section, in Modules.Prelims.CoproductsComplements]
CoprodPresentable [section, in Modules.Signatures.PresentableSignatureCoproducts]
CoprodPresentable.bind_α [variable, in Modules.Signatures.PresentableSignatureCoproducts]
CoprodPresentable.cpSig [variable, in Modules.Signatures.PresentableSignatureCoproducts]
CoprodPresentable.toSig [variable, in Modules.Signatures.PresentableSignatureCoproducts]
CoprodPwIso [section, in Modules.Prelims.CoproductsComplements]
CoprodPwIso.cpB'2 [variable, in Modules.Prelims.CoproductsComplements]
CoprodSigma [section, in Modules.Prelims.CoproductsComplements]
CoprodSigma.BS [variable, in Modules.Prelims.CoproductsComplements]
CoproductOfArrows_isEpi [lemma, in Modules.Prelims.CoproductsComplements]
CoproductsComplements [library]
Coproducts_Unit [definition, in Modules.Prelims.CoproductsComplements]
coproduct_Epis [lemma, in Modules.Prelims.EpiComplements]
coproduct_unique [section, in Modules.Prelims.CoproductsComplements]
coprod_sigs_har_iso [definition, in Modules.Signatures.HssSignatureCommutation]
coprod_sigs_har_eq [lemma, in Modules.Signatures.HssSignatureCommutation]
coprod_sigs_har_mod_eq_mult [lemma, in Modules.Signatures.HssSignatureCommutation]
coprod_BindingSig [definition, in Modules.Signatures.BindingSig]
coprod_pw_iso [definition, in Modules.Prelims.CoproductsComplements]
coprod_pw_iso_isCoproduct [definition, in Modules.Prelims.CoproductsComplements]
coprod_pbm_to_pbm_coprod [definition, in Modules.Prelims.LModulesCoproducts]
coprod_pbm_to_pbm_coprod_aux [lemma, in Modules.Prelims.LModulesCoproducts]
coprod_pbm [definition, in Modules.Prelims.LModulesCoproducts]
coprod_isPresentable [definition, in Modules.Signatures.PresentableSignatureCoproducts]
coprod_epi_p_mor [lemma, in Modules.Signatures.PresentableSignatureCoproducts]
coprod_ρ_mor [definition, in Modules.Signatures.PresentableSignatureCoproducts]
Coprod.cpFunc [variable, in Modules.Signatures.SignatureCoproduct]
Coprod.cpLM [variable, in Modules.Signatures.SignatureCoproduct]
counit [abbreviation, in Modules.Prelims.deriveadj]
counit_subst_adjunction [lemma, in Modules.Prelims.deriveadj]
CP [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]
cpFunc [abbreviation, in Modules.Prelims.LModulesCoproducts]
CPO [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]
CPO [abbreviation, in Modules.Signatures.HssSignatureCommutation]
CPO [abbreviation, in Modules.Prelims.CoproductsComplements]
CPO [abbreviation, in Modules.Prelims.CoproductsComplements]
CPO [abbreviation, in Modules.Prelims.CoproductsComplements]
CPO [abbreviation, in Modules.Signatures.PresentableSignatureBinProdR]
CPO [abbreviation, in Modules.Signatures.PresentableSignatureCoproducts]
Cset [abbreviation, in Modules.Signatures.BindingSig]
D
d [section, in Modules.Prelims.PushoutsFromCoeqBinCoproducts]DAr [section, in Modules.Signatures.SignatureDerivation]
DAr [section, in Modules.SoftEquations.SignatureOverDerivation]
DAr [section, in Modules.SoftEquations.SignatureOverDerivation]
DAr.a [variable, in Modules.Signatures.SignatureDerivation]
DAr.a [variable, in Modules.SoftEquations.SignatureOverDerivation]
DAr.a [variable, in Modules.SoftEquations.SignatureOverDerivation]
∂ [notation, in Modules.Signatures.SignatureDerivation]
∂ [notation, in Modules.SoftEquations.SignatureOverDerivation]
∂ [notation, in Modules.SoftEquations.SignatureOverDerivation]
derivadj [section, in Modules.Prelims.deriveadj]
_ × _ (set_scope) [notation, in Modules.Prelims.deriveadj]
_ + _ (set_scope) [notation, in Modules.Prelims.deriveadj]
∂ [notation, in Modules.Prelims.deriveadj]
×ℜ [notation, in Modules.Prelims.deriveadj]
DerivationIsFunctorial [library]
DerivCounit [section, in Modules.Prelims.deriveadj]
_ ×× _ [notation, in Modules.Prelims.deriveadj]
∂ [notation, in Modules.Prelims.deriveadj]
×ℜ [notation, in Modules.Prelims.deriveadj]
deriveadj [library]
DerivFunctor [section, in Modules.Prelims.DerivationIsFunctorial]
_ ' [notation, in Modules.Prelims.DerivationIsFunctorial]
∂ [notation, in Modules.Prelims.DerivationIsFunctorial]
deriv_adj [lemma, in Modules.Prelims.deriveadj]
deriv_counit [definition, in Modules.Prelims.deriveadj]
deriv_counit_is_nat_trans [lemma, in Modules.Prelims.deriveadj]
deriv_counit_data [definition, in Modules.Prelims.deriveadj]
deriv_epiSig [lemma, in Modules.Signatures.PreservesEpi]
discrete_opfibration [definition, in Modules.Prelims.Opfibration]
Discrete_OpFibrations [section, in Modules.Prelims.Opfibration]
disp_InitialArrowUnique [lemma, in Modules.Prelims.FibrationInitialPushout]
disp_InitialArrow [definition, in Modules.Prelims.FibrationInitialPushout]
disp_mor_to_total_mor [definition, in Modules.Prelims.FibrationInitialPushout]
disp_mor_unique_disc_opfib [lemma, in Modules.Prelims.Opfibration]
d' [abbreviation, in Modules.Prelims.LModulesColims]
d' [abbreviation, in Modules.Prelims.LModulesCoproducts]
E
elementary_equations_preserve_initiality_choice [lemma, in Modules.SoftEquations.AdjunctionEquationRep]elementary_equations_on_alg_preserve_initiality [definition, in Modules.SoftEquations.AdjunctionEquationRep]
elementary_equations_preserve_initiality [lemma, in Modules.SoftEquations.AdjunctionEquationRep]
elementary_equation [definition, in Modules.SoftEquations.quotientequation]
EndAlg [abbreviation, in Modules.Signatures.HssInitialModel]
EndSet [abbreviation, in Modules.Signatures.HssInitialModel]
EndSet [abbreviation, in Modules.Signatures.BindingSig]
EndSet [abbreviation, in Modules.Signatures.PresentableSignature]
EpiArePointwise [library]
EpiComplements [library]
EpiSignatureSig [section, in Modules.Signatures.HssInitialModel]
EpiSignatureSig [section, in Modules.Signatures.BindingSig]
EpiSignatureSig.isEpiEpiFunc [variable, in Modules.Signatures.BindingSig]
EpiSignatureSig.isEpiSig [variable, in Modules.Signatures.BindingSig]
EpiSignatureThetaTheta [definition, in Modules.Signatures.EpiSigRepresentability]
EpiSigRepresentability [library]
epiSigR' [lemma, in Modules.SoftEquations.quotientrepslice]
epiSig_equiv_pwEpi_SET [lemma, in Modules.Signatures.EpiArePointwise]
epiSig_is_pwEpi [lemma, in Modules.Signatures.EpiArePointwise]
epiSig_NatEpi [lemma, in Modules.Signatures.PreservesEpi]
epis_are_pointwise [definition, in Modules.Prelims.EpiComplements]
epi_nt_preserves_Epi [lemma, in Modules.Prelims.EpiComplements]
epi_nt_SET_pw [lemma, in Modules.Prelims.EpiComplements]
epi_p_mor [definition, in Modules.Signatures.PresentableSignature]
eqrel_equivc [definition, in Modules.Prelims.quotientmonadslice]
EQS [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
equation [definition, in Modules.SoftEquations.Equation]
Equation [section, in Modules.SoftEquations.Equation]
Equation [library]
equivc [definition, in Modules.Prelims.quotientmonadslice]
equivc_xy_prop [definition, in Modules.Prelims.quotientmonadslice]
eq_projR_rel [lemma, in Modules.Prelims.quotientmonad]
eq_mr [lemma, in Modules.Signatures.EpiSigRepresentability]
eta_equation [definition, in Modules.SoftEquations.Examples.LCBetaEta]
F
F [abbreviation, in Modules.Prelims.LModulesColims]F [abbreviation, in Modules.Prelims.LModulesBinProducts]
F [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
F [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
F [abbreviation, in Modules.Prelims.LModulesCoproducts]
FaithfulFibrationEqualizer [library]
faithful_opfibration_coequalizer [lemma, in Modules.Prelims.FaithfulFibrationEqualizer]
faithful_reformulated [abbreviation, in Modules.Prelims.FaithfulFibrationEqualizer]
faithful_fibration_equalizer [lemma, in Modules.Prelims.FaithfulFibrationEqualizer]
faithful_reformulated [lemma, in Modules.Prelims.FaithfulFibrationEqualizer]
FIBER_CAT [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
FIBER_CAT [abbreviation, in Modules.Signatures.ModelCat]
FibrationInitialPushout [library]
fib_to_dir_is_functor [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
fib_to_dir_functor_data [definition, in Modules.SoftEquations.CatOfTwoSignatures]
fib_to_dir_mor_weq [definition, in Modules.SoftEquations.CatOfTwoSignatures]
fib_to_dir_functor [definition, in Modules.Signatures.ModelCat]
fib_to_dir_is_functor [lemma, in Modules.Signatures.ModelCat]
fib_to_dir_functor_data [definition, in Modules.Signatures.ModelCat]
fib_to_dir_mor_weq [definition, in Modules.Signatures.ModelCat]
fib_to_dir_weq [definition, in Modules.Signatures.ModelCat]
FORGET [abbreviation, in Modules.Prelims.LModulesColims]
ForgetSigFunctor [section, in Modules.Signatures.Signature]
forget_Sig [definition, in Modules.Signatures.Signature]
forget_Sig_is_functor [definition, in Modules.Signatures.Signature]
forget_Sig_data [definition, in Modules.Signatures.Signature]
forget_2model_is_right_adjoint [definition, in Modules.SoftEquations.AdjunctionEquationRep]
forget_2model_fully_faithful [definition, in Modules.SoftEquations.Equation]
forget_2model [definition, in Modules.SoftEquations.Equation]
from_Coproduct_to_Coproduct [definition, in Modules.Prelims.CoproductsComplements]
from_Coproducts_weq [definition, in Modules.Prelims.CoproductsComplements]
FS [abbreviation, in Modules.Signatures.ModelCat]
FSmor [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
FSmor [abbreviation, in Modules.Signatures.ModelCat]
FSob [abbreviation, in Modules.Signatures.ModelCat]
Functoriality [section, in Modules.Prelims.deriveadj]
_ ×a _ [notation, in Modules.Prelims.deriveadj]
∂ [notation, in Modules.Prelims.deriveadj]
functorial_counit_derivadj [lemma, in Modules.Prelims.deriveadj]
functor_cat_isDistributive [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
F' [abbreviation, in Modules.Prelims.LModulesColims]
G
GenericStrat [section, in Modules.Signatures.HssSignatureCommutation]GenericStrat [section, in Modules.SoftEquations.SignatureOverBinproducts]
GenericStrat.M1 [variable, in Modules.Signatures.HssSignatureCommutation]
GenericStrat.M2 [variable, in Modules.Signatures.HssSignatureCommutation]
GenericStrat.Sf12_eq [variable, in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S1 [variable, in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S1 [variable, in Modules.SoftEquations.SignatureOverBinproducts]
GenericStrat.S1_S2_R_iso [variable, in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S1_data [variable, in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S2 [variable, in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S2 [variable, in Modules.SoftEquations.SignatureOverBinproducts]
GenericStrat.S2_data [variable, in Modules.Signatures.HssSignatureCommutation]
H
hab [definition, in Modules.Signatures.EpiSigRepresentability]hab_alt [lemma, in Modules.Signatures.EpiSigRepresentability]
halfeq1 [definition, in Modules.SoftEquations.Equation]
halfeq2 [definition, in Modules.SoftEquations.Equation]
half_beta_subst [definition, in Modules.SoftEquations.Examples.LCBetaEta]
half_equation [definition, in Modules.SoftEquations.Equation]
half_elem_eqs [definition, in Modules.SoftEquations.quotientequation]
HAR [abbreviation, in Modules.Signatures.SignaturesColims]
HAR [abbreviation, in Modules.Signatures.Signature]
har_binprodR_isPresentable [definition, in Modules.Signatures.PresentableSignatureBinProdR]
har_binprodR_epi_p_mor [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
har_binprodR_p_mor [definition, in Modules.Signatures.PresentableSignatureBinProdR]
har_binprodR_commute_mor_mod [definition, in Modules.Signatures.PresentableSignatureBinProdR]
har_binprodR_p_sig [definition, in Modules.Signatures.PresentableSignatureBinProdR]
helper [lemma, in Modules.Signatures.ModelCat]
helper [lemma, in Modules.Signatures.EpiSigRepresentability]
hom_SET [abbreviation, in Modules.Signatures.HssInitialModel]
hom_SET [abbreviation, in Modules.Signatures.BindingSig]
hom_SET [abbreviation, in Modules.Signatures.PresentableSignature]
horcomp_assoc [lemma, in Modules.Prelims.lib]
hrel_equivc [definition, in Modules.Prelims.quotientmonadslice]
hsC [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]
hsC [abbreviation, in Modules.Prelims.deriveadj]
hsC [abbreviation, in Modules.Signatures.SignatureBinproducts]
hsC [abbreviation, in Modules.Signatures.SignatureCoproduct]
hsC [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
hsC [abbreviation, in Modules.SoftEquations.SignatureOverBinproducts]
hset_category_isDistributive [lemma, in Modules.Prelims.SetCatComplements]
hsS [abbreviation, in Modules.Prelims.deriveadj]
hsS [abbreviation, in Modules.Prelims.deriveadj]
HssInitialModel [library]
HssSignatureCommutation [library]
hss_sig_initial [definition, in Modules.Signatures.HssInitialModel]
hss_sig_effective [lemma, in Modules.Signatures.HssInitialModel]
hss_initial_arrow_unique [lemma, in Modules.Signatures.HssInitialModel]
hss_initial_arrow [definition, in Modules.Signatures.HssInitialModel]
hss_initial_arrow_law [definition, in Modules.Signatures.HssInitialModel]
hss_initial_arrow_mon [definition, in Modules.Signatures.HssInitialModel]
hss_initial_model [lemma, in Modules.Signatures.HssInitialModel]
I
ID [abbreviation, in Modules.Signatures.ModelCat]IdM [abbreviation, in Modules.Signatures.ModelCat]
IdM [abbreviation, in Modules.Signatures.ModelCat]
id_preserves_Epi [definition, in Modules.Prelims.EpiComplements]
iniHSS [abbreviation, in Modules.Signatures.HssInitialModel]
InitAlg [section, in Modules.Signatures.ModelCat]
_ ++f _ [notation, in Modules.Signatures.ModelCat]
_ + _ [notation, in Modules.Signatures.ModelCat]
[[ _ , _ ]] [notation, in Modules.Signatures.ModelCat]
InitAlg2 [section, in Modules.Signatures.ModelCat]
initial_cl_lift_square_eq [lemma, in Modules.Prelims.FibrationInitialPushout]
initial_universal_to_lift_initial [lemma, in Modules.Prelims.lib]
in_abs_halfeq [definition, in Modules.SoftEquations.Examples.LCBetaEta]
isaprop_rep_fiber_mor_law [lemma, in Modules.Signatures.ModelCat]
isaprop_is_signature_over_Mor [lemma, in Modules.SoftEquations.SignatureOver]
isaprop_is_signature_over [lemma, in Modules.SoftEquations.SignatureOver]
isaprop_is_signature_over [lemma, in Modules.SoftEquations.SignatureOverAsFiber]
isaprop_equivc_xy [lemma, in Modules.Prelims.quotientmonadslice]
isaprop_disc_opfib_hom [lemma, in Modules.Prelims.Opfibration]
isaprop_cocartesian_lifts [definition, in Modules.Prelims.Opfibration]
isaprop_is_cocartesian [lemma, in Modules.Prelims.Opfibration]
isaprop_model_mor_law [lemma, in Modules.Signatures.Signature]
isaprop_is_signature_Mor [lemma, in Modules.Signatures.Signature]
isaprop_is_signature [lemma, in Modules.Signatures.Signature]
isaset_rep_fiber_mor [lemma, in Modules.Signatures.ModelCat]
isaset_signature_over_Mor [lemma, in Modules.SoftEquations.SignatureOver]
isaset_fiber_discrete_opfibration [definition, in Modules.Prelims.Opfibration]
isaset_model_mor_mor [lemma, in Modules.Signatures.Signature]
isaset_signature_Mor [lemma, in Modules.Signatures.Signature]
isEpiBinProd [definition, in Modules.Signatures.PresentableSignatureBinProdR]
isEpiBinProdHSET [lemma, in Modules.Prelims.SetCatComplements]
isEpi_beta_sig_source [lemma, in Modules.SoftEquations.Examples.LCBetaEta]
isEpi_projR_monad [lemma, in Modules.Prelims.quotientmonad]
isEpi_projR_projR_projR_pw [lemma, in Modules.Prelims.quotientmonad]
isEpi_projR_projR [lemma, in Modules.Prelims.quotientmonad]
isEpi_R_projR_projR_pw [lemma, in Modules.Prelims.quotientmonad]
isEpi_projR_projR_pw [lemma, in Modules.Prelims.quotientmonad]
isEpi_projR [lemma, in Modules.Prelims.quotientmonad]
isEpi_RprojR_pw [lemma, in Modules.Prelims.quotientmonad]
isEpi_projR_pw [lemma, in Modules.Prelims.quotientmonad]
isEpi_horcomp_pw2 [lemma, in Modules.Prelims.EpiComplements]
isEpi_horcomp_pw [lemma, in Modules.Prelims.EpiComplements]
isEpi_projR_rep [lemma, in Modules.SoftEquations.quotientrepslice]
isEpi_binProdSig [lemma, in Modules.Signatures.BindingSig]
isEpi_sig_isEpi_overSig [definition, in Modules.SoftEquations.quotientequation]
isEpi_overSig [definition, in Modules.SoftEquations.quotientequation]
isEpi_def_R'_model_τ [lemma, in Modules.Signatures.EpiSigRepresentability]
iseqrel_equivc [lemma, in Modules.Prelims.quotientmonadslice]
isoRIdM [lemma, in Modules.Signatures.ModelCat]
isounit_coreflection [lemma, in Modules.Prelims.lib]
iso_mod_id_model [lemma, in Modules.Signatures.ModelCat]
iso_from_isDistributive [definition, in Modules.Prelims.CoproductsComplements]
iso_from_Coproduct_to_Coproduct [definition, in Modules.Prelims.CoproductsComplements]
isPresentable [definition, in Modules.Signatures.PresentableSignature]
isSoft [definition, in Modules.SoftEquations.quotientequation]
isSoft_eq [definition, in Modules.SoftEquations.quotientequation]
isSoft_finite_deriv_tauto [lemma, in Modules.SoftEquations.quotientequation]
isSoft_derivative [lemma, in Modules.SoftEquations.quotientequation]
isSoft_tauto [lemma, in Modules.SoftEquations.quotientequation]
is_precategory_rep_fiber_precategory_data [lemma, in Modules.Signatures.ModelCat]
is_rep_fiber_comp [lemma, in Modules.Signatures.ModelCat]
is_rep_fiber_id [lemma, in Modules.Signatures.ModelCat]
is_precategory_signature_over_precategory_data [lemma, in Modules.SoftEquations.SignatureOver]
is_signature_over_Mor_comp [lemma, in Modules.SoftEquations.SignatureOver]
is_signature_over_Mor_id [lemma, in Modules.SoftEquations.SignatureOver]
is_signature_over_Mor [definition, in Modules.SoftEquations.SignatureOver]
is_sig_over_from_sig [lemma, in Modules.SoftEquations.SignatureOver]
is_signature_over [definition, in Modules.SoftEquations.SignatureOver]
is_signature_over [definition, in Modules.SoftEquations.SignatureOverAsFiber]
is_discrete_opfibration [definition, in Modules.Prelims.Opfibration]
is_opcleaving [definition, in Modules.Prelims.Opfibration]
is_cocartesian_disp_functor [definition, in Modules.Prelims.Opfibration]
is_cocartesian [definition, in Modules.Prelims.Opfibration]
is_precategory_signature_precategory_data [lemma, in Modules.Signatures.Signature]
is_signature_Mor_id [lemma, in Modules.Signatures.Signature]
is_signature_Mor_comp [lemma, in Modules.Signatures.Signature]
is_signature_Mor [definition, in Modules.Signatures.Signature]
is_signature [definition, in Modules.Signatures.Signature]
is_iso_from_Coproduct_to_Coproduct [lemma, in Modules.Prelims.CoproductsComplements]
is_right_adjoint_functor_of_reps_from_pw_epi_choice [lemma, in Modules.Signatures.EpiSigRepresentability]
is_right_adjoint_functor_of_reps_from_pw_epi [lemma, in Modules.Signatures.EpiSigRepresentability]
is_right_adjoint_functor_of_reps [definition, in Modules.Signatures.EpiSigRepresentability]
L
LamOneSig [definition, in Modules.SoftEquations.Examples.LCBetaEta]LamOneSigHSET [definition, in Modules.SoftEquations.Examples.LCBetaEta]
LamOneSigHSET_Initial [definition, in Modules.SoftEquations.Examples.LCBetaEta]
LamOneSigHSET_epiSig [definition, in Modules.SoftEquations.Examples.LCBetaEta]
LargeCatMod [section, in Modules.Prelims.LModulesFibration]
LargeCatRep [section, in Modules.Signatures.Signature]
LCBetaEta [definition, in Modules.SoftEquations.Examples.LCBetaEta]
LCBetaEta [library]
leftadjoint [section, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.FF [variable, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.uModel [section, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.R'Model [section, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.Instantiating_Quotient_Constructions [section, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.ff [variable, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.dd [variable, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.J [variable, in Modules.Signatures.EpiSigRepresentability]
## _ [notation, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a [section, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.Rep_b [variable, in Modules.Signatures.EpiSigRepresentability]
leftadjoint.Rep_a [variable, in Modules.Signatures.EpiSigRepresentability]
SET [notation, in Modules.Signatures.EpiSigRepresentability]
lib [library]
liftlmodule [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
liftlmodule [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
LiftLModuleMor [section, in Modules.Signatures.SigWithStrengthToSignature]
p _ [notation, in Modules.Signatures.SigWithStrengthToSignature]
lift_pb_LModule [definition, in Modules.Signatures.SigWithStrengthToSignature]
lift_pb_LModule_iso [lemma, in Modules.Signatures.SigWithStrengthToSignature]
lift_pb_LModule_eq_mult [lemma, in Modules.Signatures.SigWithStrengthToSignature]
lift_lmodule_mor [definition, in Modules.Signatures.SigWithStrengthToSignature]
lift_lmodule_mor_law [lemma, in Modules.Signatures.SigWithStrengthToSignature]
limFunc [abbreviation, in Modules.Prelims.LModulesColims]
LMOD [abbreviation, in Modules.Prelims.DerivationIsFunctorial]
LMOD [abbreviation, in Modules.Prelims.deriveadj]
LMOD [abbreviation, in Modules.Prelims.LModulesBinProducts]
LMOD [abbreviation, in Modules.Prelims.LModulesBinProducts]
LModulesBinProducts [library]
LModulesColims [library]
LModulesComplements [library]
LModulesCoproducts [library]
LModulesFibration [library]
LModule_to_deriv_functor [definition, in Modules.Prelims.DerivationIsFunctorial]
LModule_to_deriv_is_nt [lemma, in Modules.Prelims.DerivationIsFunctorial]
LModule_to_deriv [definition, in Modules.Prelims.DerivationIsFunctorial]
LModule_to_deriv_laws [lemma, in Modules.Prelims.DerivationIsFunctorial]
LModule_to_deriv_nt [definition, in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_functor [definition, in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_is_functor [lemma, in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_functor_data [definition, in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_Mor [definition, in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_Mor_laws [lemma, in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_Mor_nt [definition, in Modules.Prelims.DerivationIsFunctorial]
LModule_Lims_of_shape [definition, in Modules.Prelims.LModulesColims]
LModule_Colims_of_shape [definition, in Modules.Prelims.LModulesColims]
LModule_LimCone [definition, in Modules.Prelims.LModulesColims]
LModule_ColimCocone [definition, in Modules.Prelims.LModulesColims]
LModule_isLimCone [lemma, in Modules.Prelims.LModulesColims]
LModule_isColimCocone [lemma, in Modules.Prelims.LModulesColims]
LModule_limArrow [definition, in Modules.Prelims.LModulesColims]
LModule_colimArrow [definition, in Modules.Prelims.LModulesColims]
LModule_limArrow_laws [definition, in Modules.Prelims.LModulesColims]
LModule_colimArrow_laws [definition, in Modules.Prelims.LModulesColims]
LModule_lim_cone [definition, in Modules.Prelims.LModulesColims]
LModule_colim_cocone [definition, in Modules.Prelims.LModulesColims]
LModule_coneOut_commutes [lemma, in Modules.Prelims.LModulesColims]
LModule_coconeIn_commutes [lemma, in Modules.Prelims.LModulesColims]
LModule_coneOut [definition, in Modules.Prelims.LModulesColims]
LModule_coconeIn [definition, in Modules.Prelims.LModulesColims]
LModule_coneOut_laws [lemma, in Modules.Prelims.LModulesColims]
LModule_coconeIn_laws [lemma, in Modules.Prelims.LModulesColims]
LModule_lim [definition, in Modules.Prelims.LModulesColims]
LModule_colim [definition, in Modules.Prelims.LModulesColims]
LModule_lim_laws [lemma, in Modules.Prelims.LModulesColims]
LModule_colim_laws [lemma, in Modules.Prelims.LModulesColims]
LModule_lim_data [definition, in Modules.Prelims.LModulesColims]
LModule_colim_data [definition, in Modules.Prelims.LModulesColims]
LModule_lim_mult [definition, in Modules.Prelims.LModulesColims]
LModule_colim_mult [definition, in Modules.Prelims.LModulesColims]
LModule_lim_mult_is_nat_trans [lemma, in Modules.Prelims.LModulesColims]
LModule_colim_mult_is_nat_trans [lemma, in Modules.Prelims.LModulesColims]
LModule_lim_mult_data [definition, in Modules.Prelims.LModulesColims]
LModule_colim_mult_data [definition, in Modules.Prelims.LModulesColims]
LModule_BinProducts [definition, in Modules.Prelims.LModulesBinProducts]
LModule_ProductCone [definition, in Modules.Prelims.LModulesBinProducts]
LModule_isBinProductCone [lemma, in Modules.Prelims.LModulesBinProducts]
LModule_BinProductPr2Commutes [lemma, in Modules.Prelims.LModulesBinProducts]
LModule_BinProductPr1Commutes [lemma, in Modules.Prelims.LModulesBinProducts]
LModule_BinProductArrow [definition, in Modules.Prelims.LModulesBinProducts]
LModule_BinProductArrow_laws [definition, in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr2 [definition, in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr1 [definition, in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr2_laws [lemma, in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr1_laws [lemma, in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr2_nt [definition, in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr1_nt [definition, in Modules.Prelims.LModulesBinProducts]
LModule_binproduct [definition, in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_laws [lemma, in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_data [definition, in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_mult [definition, in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_mult_is_nat_trans [lemma, in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_mult_data [definition, in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_functor [definition, in Modules.Prelims.LModulesBinProducts]
LModule_Coproducts [definition, in Modules.Prelims.LModulesCoproducts]
LModule_Coproduct [definition, in Modules.Prelims.LModulesCoproducts]
LModule_isCoproduct [lemma, in Modules.Prelims.LModulesCoproducts]
LModule_coproductArrow [definition, in Modules.Prelims.LModulesCoproducts]
LModule_coproductArrow_laws [definition, in Modules.Prelims.LModulesCoproducts]
LModule_coproductIn [definition, in Modules.Prelims.LModulesCoproducts]
LModule_coproductIn_laws [lemma, in Modules.Prelims.LModulesCoproducts]
LModule_coproduct [definition, in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_laws [lemma, in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_data [definition, in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_mult [definition, in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_mult_is_nat_trans [lemma, in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_mult_data [definition, in Modules.Prelims.LModulesCoproducts]
LMOD_bp [abbreviation, in Modules.Prelims.deriveadj]
LMOD_bp [abbreviation, in Modules.Prelims.deriveadj]
LMOD_bp [abbreviation, in Modules.Prelims.deriveadj]
LMOD_bp [abbreviation, in Modules.Prelims.deriveadj]
LMod_isDistributive [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
LMod_isDistributive_is_inverse [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
LMod_isDistributive_inv [definition, in Modules.Signatures.PresentableSignatureBinProdR]
LMod_isDistributive_inv_laws [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
M
mkSignature_over_Mor [definition, in Modules.SoftEquations.SignatureOver]mk_soft_equation [definition, in Modules.SoftEquations.quotientequation]
MOD [abbreviation, in Modules.Signatures.SignatureDerivation]
MOD [abbreviation, in Modules.Signatures.SignaturesColims]
MOD [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
MOD [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
MOD [abbreviation, in Modules.Prelims.LModulesColims]
MOD [abbreviation, in Modules.Signatures.SignatureBinproducts]
MOD [abbreviation, in Modules.Signatures.SignatureCoproduct]
MOD [abbreviation, in Modules.Signatures.Signature]
MOD [abbreviation, in Modules.SoftEquations.quotientrepslice]
MOD [abbreviation, in Modules.SoftEquations.quotientrepslice]
MOD [abbreviation, in Modules.SoftEquations.quotientrepslice]
MOD [abbreviation, in Modules.Signatures.EpiArePointwise]
MOD [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
MOD [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
MOD [abbreviation, in Modules.Prelims.LModulesCoproducts]
MOD [abbreviation, in Modules.SoftEquations.quotientequation]
MOD [abbreviation, in Modules.SoftEquations.SignatureOverBinproducts]
MODEL [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
MODEL [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
model [definition, in Modules.Signatures.Signature]
ModelCat [section, in Modules.Signatures.ModelCat]
ModelCat [library]
MODEL_CAT [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
MODEL_CAT [abbreviation, in Modules.Signatures.ModelCat]
MODEL_MOR [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
MODEL_MOR [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
model_mor_mor_equiv [lemma, in Modules.Signatures.Signature]
model_mor_ax [definition, in Modules.Signatures.Signature]
model_mor_mor [definition, in Modules.Signatures.Signature]
model_mor_law [definition, in Modules.Signatures.Signature]
model_τ [definition, in Modules.Signatures.Signature]
model_equations_eq [definition, in Modules.SoftEquations.Equation]
model_equations [definition, in Modules.SoftEquations.Equation]
Modularity [library]
Modularity [library]
MODULE [abbreviation, in Modules.Prelims.LModulesFibration]
MODULE [abbreviation, in Modules.SoftEquations.Summary]
mod_id_model_mor [definition, in Modules.Signatures.ModelCat]
mod_id_model_mor_laws [definition, in Modules.Signatures.ModelCat]
mod_id_model [definition, in Modules.Signatures.ModelCat]
mod_id_model_action [definition, in Modules.Signatures.ModelCat]
mod_id_model_monad [definition, in Modules.Signatures.ModelCat]
mod_M_idM_mod_Mor [definition, in Modules.Signatures.ModelCat]
mod_M_idM_mod_laws [lemma, in Modules.Signatures.ModelCat]
mod_id_monad_mor [definition, in Modules.Signatures.ModelCat]
mod_id_monad_mor_laws [lemma, in Modules.Signatures.ModelCat]
mod_id_monad [definition, in Modules.Signatures.ModelCat]
mod_id_monad_laws [lemma, in Modules.Signatures.ModelCat]
mod_id_M_mod_law2 [lemma, in Modules.Signatures.ModelCat]
mod_id_monad_data [definition, in Modules.Signatures.ModelCat]
mod_id_μ [definition, in Modules.Signatures.ModelCat]
mod_id_M_mod_law1 [lemma, in Modules.Signatures.ModelCat]
mod_id_M_mod [definition, in Modules.Signatures.ModelCat]
mod_M_idM [definition, in Modules.Signatures.ModelCat]
mod_id_η [definition, in Modules.Signatures.ModelCat]
mod_id_nt [definition, in Modules.Signatures.ModelCat]
mod_id_functor [definition, in Modules.Signatures.ModelCat]
MOD1 [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
MOD2 [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
MONAD [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
MONAD [abbreviation, in Modules.Signatures.ModelCat]
MONAD [abbreviation, in Modules.SoftEquations.SignatureOver]
MONAD [abbreviation, in Modules.SoftEquations.SignatureOverAsFiber]
MONAD [abbreviation, in Modules.Prelims.LModulesFibration]
MONAD [abbreviation, in Modules.SoftEquations.Summary]
MONAD [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
MONAD [abbreviation, in Modules.Signatures.Signature]
MONAD [abbreviation, in Modules.Signatures.Signature]
MONAD [abbreviation, in Modules.SoftEquations.quotientrepslice]
MONAD [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
MONAD [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
MONAD [abbreviation, in Modules.SoftEquations.quotientequation]
monad_mor_to_lmodule [definition, in Modules.Prelims.LModulesComplements]
monad_mor_to_lmodule_law [lemma, in Modules.Prelims.LModulesComplements]
mor_disp_of_cocartesian_lift [definition, in Modules.Prelims.Opfibration]
M_alg [abbreviation, in Modules.Signatures.HssInitialModel]
M_IdM_mod [definition, in Modules.Signatures.ModelCat]
N
nat_trans_comp_pointwise' [definition, in Modules.Prelims.lib]O
object_of_cocartesian_lift [definition, in Modules.Prelims.Opfibration]OneMod_to_TwoMod_fully_faithful [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
OneMod_to_TwoMod [definition, in Modules.SoftEquations.CatOfTwoSignatures]
OneSig_to_TwoSig_fully_faithful [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
OneSig_to_TwoSig [definition, in Modules.SoftEquations.CatOfTwoSignatures]
opcleaving [definition, in Modules.Prelims.Opfibration]
opcleaving_mor [definition, in Modules.Prelims.Opfibration]
opcleaving_ob [definition, in Modules.Prelims.Opfibration]
opfibration [definition, in Modules.Prelims.Opfibration]
Opfibration [library]
Opfibrations [section, in Modules.Prelims.Opfibration]
opfibration_from_discrete_opfibration [definition, in Modules.Prelims.Opfibration]
opfib_two_sig [definition, in Modules.SoftEquations.CatOfTwoSignatures]
oppr [section, in Modules.Prelims.FaithfulFibrationEqualizer]
oppr.faithful_opfibration [variable, in Modules.Prelims.FaithfulFibrationEqualizer]
OSig [abbreviation, in Modules.SoftEquations.SignatureOver]
OSIG [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
OSIG [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
OverSignatures [section, in Modules.SoftEquations.SignatureOver]
OverSignatures.comp [variable, in Modules.SoftEquations.SignatureOver]
_ ⟹ _ (signature_over_scope) [notation, in Modules.SoftEquations.SignatureOver]
# _ (signature_over_scope) [notation, in Modules.SoftEquations.SignatureOver]
_ →→s _ [notation, in Modules.SoftEquations.SignatureOver]
_ ;; _ [notation, in Modules.SoftEquations.SignatureOver]
_ →→ _ [notation, in Modules.SoftEquations.SignatureOver]
P
pbm_binprod [definition, in Modules.Prelims.LModulesBinProducts]pbm_coprod [definition, in Modules.Prelims.LModulesCoproducts]
pb_modeq [definition, in Modules.SoftEquations.CatOfTwoSignatures]
pb_rep_comp [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
pb_rep_id [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
pb_rep_mor_id [lemma, in Modules.Signatures.ModelCat]
pb_rep_mor_comp [lemma, in Modules.Signatures.ModelCat]
pb_rep_mor [definition, in Modules.Signatures.ModelCat]
pb_rep_mor_law [lemma, in Modules.Signatures.ModelCat]
pb_LModule_lim_iso [definition, in Modules.Prelims.LModulesColims]
pb_LModule_colim_iso [definition, in Modules.Prelims.LModulesColims]
pb_lims_eq_mult [lemma, in Modules.Prelims.LModulesColims]
pb_colims_eq_mult [lemma, in Modules.Prelims.LModulesColims]
pb_rep_to_cartesian [definition, in Modules.Signatures.Signature]
pb_rep_to [definition, in Modules.Signatures.Signature]
pb_rep_to_law [lemma, in Modules.Signatures.Signature]
pb_rep [definition, in Modules.Signatures.Signature]
PO [abbreviation, in Modules.Signatures.PresentableSignatureBinProdR]
postcomp_nt [definition, in Modules.Signatures.ModelCat]
postcomp_with_iso_disp_is_inj [definition, in Modules.Prelims.Opfibration]
po_signature_over_mor [definition, in Modules.SoftEquations.SignatureOver]
po_signature_over [definition, in Modules.SoftEquations.SignatureOver]
po_is_signature_over [lemma, in Modules.SoftEquations.SignatureOver]
po_signature_over_data [definition, in Modules.SoftEquations.SignatureOver]
PO_eqdiag [lemma, in Modules.Signatures.EpiArePointwise]
po_satisfies_equation [definition, in Modules.SoftEquations.Equation]
po_equation [definition, in Modules.SoftEquations.Equation]
pr [section, in Modules.Prelims.FibrationInitialPushout]
pr [section, in Modules.Prelims.FaithfulFibrationEqualizer]
precategory_model_equations [definition, in Modules.SoftEquations.Equation]
PRECAT_SIGNATURE [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
PRECAT_SIGNATURE [abbreviation, in Modules.Signatures.Signature]
precompEpiEpiFunc [lemma, in Modules.Signatures.BindingSig]
precompEpiEpiFuncSn [lemma, in Modules.Signatures.BindingSig]
precompEpiFunc [lemma, in Modules.Signatures.BindingSig]
precompToFunc [abbreviation, in Modules.Signatures.BindingSig]
precompToSig [abbreviation, in Modules.Signatures.BindingSig]
precomp_func_preserveEpi [lemma, in Modules.Signatures.BindingSig]
precomp_functor [abbreviation, in Modules.Signatures.BindingSig]
PresentableDefinition [section, in Modules.Signatures.PresentableSignature]
PresentableDefinition.toSig [variable, in Modules.Signatures.PresentableSignature]
PresentableisEffective [lemma, in Modules.Signatures.PresentableSignature]
PresentableProjections [section, in Modules.Signatures.PresentableSignature]
PresentableProjections.toSig [variable, in Modules.Signatures.PresentableSignature]
PresentableSignature [library]
PresentableSignatureBinProdR [library]
PresentableSignatureCoproducts [library]
preserveEpi_precomp [lemma, in Modules.Prelims.EpiComplements]
preserveEpi_binCoprodFunc [lemma, in Modules.Prelims.EpiComplements]
preserveEpi_sumFuncs [lemma, in Modules.Prelims.EpiComplements]
preserveEpi_binProdFuncSET [definition, in Modules.Prelims.EpiComplements]
preserveEpi_binProdFunc [lemma, in Modules.Prelims.EpiComplements]
PreservesEpi [library]
preserves_Epi_option [lemma, in Modules.Prelims.EpiComplements]
preserves_to_HSET_isEpi [lemma, in Modules.Prelims.EpiComplements]
preserves_Epi [definition, in Modules.Prelims.EpiComplements]
PRE_MONAD [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
pre_subst_nt [definition, in Modules.Prelims.deriveadj]
pre_subst_is_nat_trans [lemma, in Modules.Prelims.deriveadj]
pre_subst_nt_data [definition, in Modules.Prelims.deriveadj]
PRE_MONAD [abbreviation, in Modules.SoftEquations.SignatureOver]
PRE_MONAD [abbreviation, in Modules.SoftEquations.SignatureOverAsFiber]
PRE_MONAD [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
PRE_MONAD [abbreviation, in Modules.Signatures.Signature]
PRE_MONAD [abbreviation, in Modules.Signatures.Signature]
productEpisFunc [lemma, in Modules.Prelims.EpiComplements]
productEpisSET [lemma, in Modules.Prelims.EpiComplements]
ProductModule [section, in Modules.Prelims.LModulesBinProducts]
products_preserves_Epis [definition, in Modules.Prelims.EpiComplements]
projR [definition, in Modules.Prelims.quotientmonad]
projR [definition, in Modules.Signatures.EpiSigRepresentability]
projR_monad [definition, in Modules.Prelims.quotientmonad]
projR_monad_laws [lemma, in Modules.Prelims.quotientmonad]
projR_monad [definition, in Modules.Prelims.quotientmonadslice]
projR_rep [definition, in Modules.SoftEquations.quotientrepslice]
projR_rep [definition, in Modules.Signatures.EpiSigRepresentability]
projR_rep_laws [lemma, in Modules.Signatures.EpiSigRepresentability]
pr.faithful_fibration [variable, in Modules.Prelims.FaithfulFibrationEqualizer]
pr.ff1 [variable, in Modules.Prelims.FibrationInitialPushout]
pr.ff2 [variable, in Modules.Prelims.FibrationInitialPushout]
pr.gg1 [variable, in Modules.Prelims.FibrationInitialPushout]
pr.gg2 [variable, in Modules.Prelims.FibrationInitialPushout]
## [notation, in Modules.Prelims.FibrationInitialPushout]
ptd_mor_from_Monad_mor [definition, in Modules.Signatures.SigWithStrengthToSignature]
pullback_lims.lR [variable, in Modules.Prelims.LModulesColims]
pullback_lims.cR [variable, in Modules.Prelims.LModulesColims]
pullback_lims.lS [variable, in Modules.Prelims.LModulesColims]
pullback_lims.cS [variable, in Modules.Prelims.LModulesColims]
pullback_lims.dR [variable, in Modules.Prelims.LModulesColims]
pullback_lims.dS [variable, in Modules.Prelims.LModulesColims]
pullback_lims.lMod [variable, in Modules.Prelims.LModulesColims]
pullback_lims.cMod [variable, in Modules.Prelims.LModulesColims]
pullback_lims.MOD [variable, in Modules.Prelims.LModulesColims]
pullback_lims [section, in Modules.Prelims.LModulesColims]
pullback_binprod.cpFunc [variable, in Modules.Prelims.LModulesBinProducts]
pullback_binprod.cpLM [variable, in Modules.Prelims.LModulesBinProducts]
pullback_binprod [section, in Modules.Prelims.LModulesBinProducts]
pullback_coprod.pbm_α [variable, in Modules.Prelims.LModulesCoproducts]
pullback_coprod.αF [variable, in Modules.Prelims.LModulesCoproducts]
pullback_coprod.cpFunc [variable, in Modules.Prelims.LModulesCoproducts]
pullback_coprod.cpLM [variable, in Modules.Prelims.LModulesCoproducts]
pullback_coprod [section, in Modules.Prelims.LModulesCoproducts]
PushoutOverSig [section, in Modules.SoftEquations.SignatureOver]
PushoutsFromCoeqBinCoproducts [library]
pushouts_from_coeq_bincoprod [definition, in Modules.Prelims.PushoutsFromCoeqBinCoproducts]
pushout_in_big_rep [definition, in Modules.SoftEquations.Modularity]
pushout_total_initial [lemma, in Modules.Prelims.FibrationInitialPushout]
pushout_total [lemma, in Modules.Prelims.FibrationInitialPushout]
pushout_in_big_rep [definition, in Modules.Signatures.Modularity]
pushout_FFpw [definition, in Modules.Signatures.EpiArePointwise]
push_initiality [definition, in Modules.SoftEquations.AdjunctionEquationRep]
push_initiality_weaker_choice [lemma, in Modules.Signatures.EpiSigRepresentability]
push_initiality [lemma, in Modules.Signatures.EpiSigRepresentability]
push_initiality_weaker [lemma, in Modules.Signatures.EpiSigRepresentability]
pwEpiAr [section, in Modules.Signatures.EpiArePointwise]
pwEpiAr.pushout_FF [variable, in Modules.Signatures.EpiArePointwise]
pwEpiSig_isEpi [lemma, in Modules.Signatures.EpiArePointwise]
p_mor [definition, in Modules.Signatures.PresentableSignature]
p_alg_ar [definition, in Modules.Signatures.PresentableSignature]
p_sig [definition, in Modules.Signatures.PresentableSignature]
Q
quotientequation [library]QuotientMonad [section, in Modules.Prelims.quotientmonad]
QuotientMonad [section, in Modules.Prelims.quotientmonadslice]
QuotientMonad [section, in Modules.Signatures.quotientrep]
quotientmonad [library]
quotientmonadslice [library]
QuotientMonad.compatm [variable, in Modules.Prelims.quotientmonad]
QuotientMonad.compat_μ_projR [variable, in Modules.Prelims.quotientmonad]
QuotientMonad.compat_m_rep [variable, in Modules.Signatures.quotientrep]
QuotientMonad.equivc [variable, in Modules.Prelims.quotientmonad]
QuotientMonad.equivc [variable, in Modules.Signatures.quotientrep]
QuotientMonad.m [variable, in Modules.Prelims.quotientmonad]
QuotientMonad.projR [variable, in Modules.Prelims.quotientmonadslice]
QuotientMonad.projR [variable, in Modules.Signatures.quotientrep]
QuotientMonad.projR_monad [variable, in Modules.Signatures.quotientrep]
QuotientMonad.R' [variable, in Modules.Prelims.quotientmonadslice]
QuotientMonad.R' [variable, in Modules.Signatures.quotientrep]
QuotientMonad.R'_monad [variable, in Modules.Signatures.quotientrep]
QuotientMonad.S [variable, in Modules.Prelims.quotientmonad]
QuotientMonad.u_monad [variable, in Modules.Signatures.quotientrep]
QuotientRep [section, in Modules.SoftEquations.quotientrepslice]
QuotientRep [section, in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep [section, in Modules.SoftEquations.quotientequation]
quotientrep [library]
QuotientRepInit [section, in Modules.SoftEquations.AdjunctionEquationRep]
quotientrepslice [library]
QuotientRep.choice [variable, in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.d [variable, in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.ff [variable, in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.J [variable, in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.projR [variable, in Modules.SoftEquations.quotientrepslice]
QuotientRep.projR [variable, in Modules.SoftEquations.quotientequation]
QuotientRep.projR_rep [variable, in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.R' [variable, in Modules.SoftEquations.quotientrepslice]
QuotientRep.R' [variable, in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.R' [variable, in Modules.SoftEquations.quotientequation]
QuotientRep.u [variable, in Modules.SoftEquations.quotientrepslice]
_ ^( _ ) [notation, in Modules.SoftEquations.quotientequation]
R
rel_eq_projR [lemma, in Modules.Prelims.quotientmonad]REP [abbreviation, in Modules.SoftEquations.SignatureOver]
REP [abbreviation, in Modules.SoftEquations.SignatureOverAsFiber]
REP [abbreviation, in Modules.SoftEquations.quotientrepslice]
REP [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
REP [abbreviation, in Modules.SoftEquations.Equation]
REP [abbreviation, in Modules.SoftEquations.quotientequation]
REP [abbreviation, in Modules.Signatures.EpiSigRepresentability]
rep_mor_to_alg_mor [definition, in Modules.Signatures.HssInitialModel]
rep_mor_to_alg_is_alg_mor [lemma, in Modules.Signatures.HssInitialModel]
rep_fiber_category [definition, in Modules.Signatures.ModelCat]
rep_fiber_category_has_homsets [lemma, in Modules.Signatures.ModelCat]
rep_fiber_precategory [definition, in Modules.Signatures.ModelCat]
rep_fiber_precategory_data [definition, in Modules.Signatures.ModelCat]
rep_fiber_precategory_ob_mor [definition, in Modules.Signatures.ModelCat]
rep_fiber_comp [definition, in Modules.Signatures.ModelCat]
rep_fiber_id [definition, in Modules.Signatures.ModelCat]
rep_fiber_mor_eq [lemma, in Modules.Signatures.ModelCat]
rep_fiber_mor_eq_nt [lemma, in Modules.Signatures.ModelCat]
rep_fiber_mor_ax [definition, in Modules.Signatures.ModelCat]
rep_fiber_mor [definition, in Modules.Signatures.ModelCat]
rep_fiber_mor_law [definition, in Modules.Signatures.ModelCat]
REP_CAT [abbreviation, in Modules.SoftEquations.SignatureOver]
rep_cleaving [lemma, in Modules.Signatures.Signature]
rep_mor_pb [lemma, in Modules.Signatures.Signature]
rep_mor_law_pb [lemma, in Modules.Signatures.Signature]
rep_disp [definition, in Modules.Signatures.Signature]
rep_axioms [lemma, in Modules.Signatures.Signature]
rep_data [definition, in Modules.Signatures.Signature]
rep_id_comp [definition, in Modules.Signatures.Signature]
rep_comp [definition, in Modules.Signatures.Signature]
rep_comp_law [lemma, in Modules.Signatures.Signature]
rep_id [definition, in Modules.Signatures.Signature]
rep_id_law [lemma, in Modules.Signatures.Signature]
rep_disp_ob_mor [definition, in Modules.Signatures.Signature]
REP_CAT [abbreviation, in Modules.SoftEquations.quotientrepslice]
REP_EQ_PRECAT [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
REP_EQ [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
REP_CAT [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
rep_of_b_in_R' [definition, in Modules.Signatures.EpiSigRepresentability]
Rep_mor_is_composition [lemma, in Modules.Signatures.EpiSigRepresentability]
R' [definition, in Modules.Prelims.quotientmonad]
R' [definition, in Modules.Signatures.EpiSigRepresentability]
R'_preserves_Epi [lemma, in Modules.Prelims.quotientmonad]
R'_monad [definition, in Modules.Prelims.quotientmonad]
R'_Monad_laws [lemma, in Modules.Prelims.quotientmonad]
R'_Monad_law_μ [lemma, in Modules.Prelims.quotientmonad]
R'_Monad_law_η2 [lemma, in Modules.Prelims.quotientmonad]
R'_Monad_law_η1 [lemma, in Modules.Prelims.quotientmonad]
R'_Monad_data [definition, in Modules.Prelims.quotientmonad]
R'_μ_def [lemma, in Modules.Prelims.quotientmonad]
R'_μ [definition, in Modules.Prelims.quotientmonad]
R'_η [definition, in Modules.Prelims.quotientmonad]
R'_monad [definition, in Modules.Prelims.quotientmonadslice]
R'_model [definition, in Modules.SoftEquations.quotientrepslice]
R'_action [definition, in Modules.SoftEquations.quotientrepslice]
R'_action_compat [lemma, in Modules.SoftEquations.quotientrepslice]
R'_model_equations [definition, in Modules.SoftEquations.quotientequation]
R'_satisfies_all_equations [definition, in Modules.SoftEquations.quotientequation]
R'_satisfies_eq [lemma, in Modules.SoftEquations.quotientequation]
R'_model_τ_def [definition, in Modules.Signatures.EpiSigRepresentability]
R'_model_τ_module [definition, in Modules.Signatures.EpiSigRepresentability]
R'_model_τ_module [definition, in Modules.Signatures.quotientrep]
R'_model_τ_module_laws [lemma, in Modules.Signatures.quotientrep]
R'_model_τ_def [definition, in Modules.Signatures.quotientrep]
R'_model_τ [definition, in Modules.Signatures.quotientrep]
S
satisfies_all_equations_hp [definition, in Modules.SoftEquations.Equation]satisfies_equation_hp [definition, in Modules.SoftEquations.Equation]
satisfies_equation_isaprop [definition, in Modules.SoftEquations.Equation]
satisfies_equation [definition, in Modules.SoftEquations.Equation]
SetCatComplements [library]
SIG [abbreviation, in Modules.Signatures.HssSignatureCommutation]
SIG [abbreviation, in Modules.Signatures.HssSignatureCommutation]
SIG [abbreviation, in Modules.Signatures.HssSignatureCommutation]
Sig [abbreviation, in Modules.Signatures.HssInitialModel]
SIG [abbreviation, in Modules.Signatures.ModelCat]
SIG [abbreviation, in Modules.SoftEquations.SignatureOver]
SIG [abbreviation, in Modules.SoftEquations.SignatureOverAsFiber]
SIG [abbreviation, in Modules.SoftEquations.quotientrepslice]
SIG [abbreviation, in Modules.Signatures.BindingSig]
Sig [abbreviation, in Modules.Signatures.BindingSig]
SIG [abbreviation, in Modules.Signatures.EpiArePointwise]
SIG [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
SIG [abbreviation, in Modules.SoftEquations.AdjunctionEquationRep]
SIG [abbreviation, in Modules.Signatures.PresentableSignatureBinProdR]
Sig [abbreviation, in Modules.Signatures.PresentableSignature]
SIG [abbreviation, in Modules.SoftEquations.quotientequation]
sigma_coprod_iso [definition, in Modules.Prelims.CoproductsComplements]
sigma_Coproduct [definition, in Modules.Prelims.CoproductsComplements]
sigma_coprod_isCoproduct [definition, in Modules.Prelims.CoproductsComplements]
sigma_coprod_In [definition, in Modules.Prelims.CoproductsComplements]
signature [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
Signature [abbreviation, in Modules.Signatures.SignatureDerivation]
Signature [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
Signature [abbreviation, in Modules.SoftEquations.SignatureOverDerivation]
SIGNATURE [abbreviation, in Modules.SoftEquations.Summary]
Signature [abbreviation, in Modules.Signatures.SignatureBinproducts]
Signature [abbreviation, in Modules.Signatures.SignatureCoproduct]
SIGNATURE [abbreviation, in Modules.Signatures.Signature]
signature [abbreviation, in Modules.Signatures.Signature]
signature [definition, in Modules.Signatures.Signature]
Signature [abbreviation, in Modules.SoftEquations.SignatureOverBinproducts]
Signature [library]
SignatureBinproducts [library]
SignatureCoproduct [library]
SignatureDerivation [library]
SignatureOver [library]
SignatureOverAsFiber [library]
SignatureOverBinproducts [library]
SignatureOverDerivation [library]
SignatureOverDerivation [library]
Signatures [section, in Modules.SoftEquations.SignatureOverAsFiber]
Signatures [section, in Modules.Signatures.Signature]
SignaturesColims [library]
Signatures.comp [variable, in Modules.SoftEquations.SignatureOverAsFiber]
# _ (signature_over_scope) [notation, in Modules.SoftEquations.SignatureOverAsFiber]
_ ⟹ _ (signature_scope) [notation, in Modules.Signatures.Signature]
# _ (signature_scope) [notation, in Modules.Signatures.Signature]
_ ;; _ [notation, in Modules.SoftEquations.SignatureOverAsFiber]
_ →→ _ [notation, in Modules.SoftEquations.SignatureOverAsFiber]
signature_S1_S2_iso [definition, in Modules.Signatures.HssSignatureCommutation]
signature_S1_S2_is_inverse [lemma, in Modules.Signatures.HssSignatureCommutation]
signature_S2_S1 [definition, in Modules.Signatures.HssSignatureCommutation]
signature_S1_S2 [definition, in Modules.Signatures.HssSignatureCommutation]
signature_S2_S1_laws [definition, in Modules.Signatures.HssSignatureCommutation]
signature_S1_S2_laws [definition, in Modules.Signatures.HssSignatureCommutation]
signature_deriv_n [definition, in Modules.Signatures.SignatureDerivation]
signature_to_deriv [definition, in Modules.Signatures.SignatureDerivation]
signature_to_deriv_laws [lemma, in Modules.Signatures.SignatureDerivation]
signature_deriv [definition, in Modules.Signatures.SignatureDerivation]
signature_deriv_is_signature [lemma, in Modules.Signatures.SignatureDerivation]
signature_deriv_data [definition, in Modules.Signatures.SignatureDerivation]
signature_deriv_on_morphisms [definition, in Modules.Signatures.SignatureDerivation]
signature_deriv_on_objects [definition, in Modules.Signatures.SignatureDerivation]
signature_over_category [definition, in Modules.SoftEquations.SignatureOver]
signature_over_category_has_homsets [lemma, in Modules.SoftEquations.SignatureOver]
signature_over_precategory [definition, in Modules.SoftEquations.SignatureOver]
signature_over_precategory_data [definition, in Modules.SoftEquations.SignatureOver]
signature_over_Mor_comp [definition, in Modules.SoftEquations.SignatureOver]
signature_over_Mor_id [definition, in Modules.SoftEquations.SignatureOver]
signature_over_precategory_ob_mor [definition, in Modules.SoftEquations.SignatureOver]
signature_over_Mor_eq [lemma, in Modules.SoftEquations.SignatureOver]
signature_over_Mor_ax_pw [lemma, in Modules.SoftEquations.SignatureOver]
signature_over_Mor_ax [definition, in Modules.SoftEquations.SignatureOver]
signature_over_Mor_data [definition, in Modules.SoftEquations.SignatureOver]
signature_over_Mor [definition, in Modules.SoftEquations.SignatureOver]
signature_over_comp [definition, in Modules.SoftEquations.SignatureOver]
signature_over_id [definition, in Modules.SoftEquations.SignatureOver]
signature_over_data_from_signature_over [definition, in Modules.SoftEquations.SignatureOver]
signature_over [definition, in Modules.SoftEquations.SignatureOver]
signature_over_compax [definition, in Modules.SoftEquations.SignatureOver]
signature_over_idax [definition, in Modules.SoftEquations.SignatureOver]
signature_over_on_morphisms_cancel_pw [definition, in Modules.SoftEquations.SignatureOver]
signature_over_on_morphisms [definition, in Modules.SoftEquations.SignatureOver]
signature_over_on_objects [definition, in Modules.SoftEquations.SignatureOver]
signature_over_data [definition, in Modules.SoftEquations.SignatureOver]
signature_over_comp [definition, in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_id [definition, in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_data_from_signature_over [definition, in Modules.SoftEquations.SignatureOverAsFiber]
signature_over [definition, in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_compax [definition, in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_idax [definition, in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_on_morphisms [definition, in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_on_objects [definition, in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_data [definition, in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_deriv_n [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_is_signature_over [lemma, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_data [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_on_morphisms [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_on_objects [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_n [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_is_signature_over [lemma, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_data [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_on_morphisms [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_on_objects [definition, in Modules.SoftEquations.SignatureOverDerivation]
signature_BinProducts [definition, in Modules.Signatures.SignatureBinproducts]
signature_BinProduct [definition, in Modules.Signatures.SignatureBinproducts]
signature_isBinProduct [lemma, in Modules.Signatures.SignatureBinproducts]
signature_binProductArrow [definition, in Modules.Signatures.SignatureBinproducts]
signature_binProductArrow_laws [definition, in Modules.Signatures.SignatureBinproducts]
signature_binProductPr2 [definition, in Modules.Signatures.SignatureBinproducts]
signature_binProductPr1 [definition, in Modules.Signatures.SignatureBinproducts]
signature_binProductPr2_laws [lemma, in Modules.Signatures.SignatureBinproducts]
signature_binProductPr1_laws [lemma, in Modules.Signatures.SignatureBinproducts]
signature_binProd [definition, in Modules.Signatures.SignatureBinproducts]
signature_binProd_is_signature [lemma, in Modules.Signatures.SignatureBinproducts]
signature_binProd_data [definition, in Modules.Signatures.SignatureBinproducts]
signature_BinProduct_on_morphisms [definition, in Modules.Signatures.SignatureBinproducts]
signature_BinProduct_on_objects [definition, in Modules.Signatures.SignatureBinproducts]
signature_Coproducts [definition, in Modules.Signatures.SignatureCoproduct]
signature_Coproduct [definition, in Modules.Signatures.SignatureCoproduct]
signature_isCoproduct [lemma, in Modules.Signatures.SignatureCoproduct]
signature_coproductArrow [definition, in Modules.Signatures.SignatureCoproduct]
signature_coproductArrow_laws [definition, in Modules.Signatures.SignatureCoproduct]
signature_coproductIn [definition, in Modules.Signatures.SignatureCoproduct]
signature_coproductIn_laws [lemma, in Modules.Signatures.SignatureCoproduct]
signature_coprod [definition, in Modules.Signatures.SignatureCoproduct]
signature_coprod_is_signature [lemma, in Modules.Signatures.SignatureCoproduct]
signature_coprod_data [definition, in Modules.Signatures.SignatureCoproduct]
signature_coprod_on_morphisms [definition, in Modules.Signatures.SignatureCoproduct]
signature_coprod_on_objects [definition, in Modules.Signatures.SignatureCoproduct]
signature_category [definition, in Modules.Signatures.Signature]
signature_category_has_homsets [lemma, in Modules.Signatures.Signature]
signature_precategory [definition, in Modules.Signatures.Signature]
signature_precategory_data [definition, in Modules.Signatures.Signature]
signature_Mor_comp [definition, in Modules.Signatures.Signature]
signature_Mor_id [definition, in Modules.Signatures.Signature]
signature_precategory_ob_mor [definition, in Modules.Signatures.Signature]
signature_Mor_eq [lemma, in Modules.Signatures.Signature]
signature_Mor_ax_pw [lemma, in Modules.Signatures.Signature]
signature_Mor_ax [definition, in Modules.Signatures.Signature]
signature_Mor_data [definition, in Modules.Signatures.Signature]
signature_Mor [definition, in Modules.Signatures.Signature]
signature_comp [definition, in Modules.Signatures.Signature]
signature_id [definition, in Modules.Signatures.Signature]
signature_data_from_signature [definition, in Modules.Signatures.Signature]
signature_compax [definition, in Modules.Signatures.Signature]
signature_idax [definition, in Modules.Signatures.Signature]
signature_on_morphisms [definition, in Modules.Signatures.Signature]
signature_on_objects [definition, in Modules.Signatures.Signature]
signature_data [definition, in Modules.Signatures.Signature]
Signature_to_signature_cons_iso [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
signature_over_BinProducts_commutes_sig [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_BinProducts [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S1_S2_iso [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S1_S2_is_inverse [lemma, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S2_S1 [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S1_S2 [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S2_S1_laws [lemma, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S1_S2_laws [lemma, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_BinProduct [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_isBinProduct [lemma, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductArrow [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductArrow_laws [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductPr2 [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductPr1 [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductPr2_laws [lemma, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductPr1_laws [lemma, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProd [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProd_is_signature_over [lemma, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProd_data [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_BinProduct_on_morphisms [definition, in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_BinProduct_on_objects [definition, in Modules.SoftEquations.SignatureOverBinproducts]
SigWithStrengthToSignature [section, in Modules.Signatures.SigWithStrengthToSignature]
SigWithStrengthToSignature [library]
SigWithStrengthToSignatureFunctor [section, in Modules.Signatures.SigWithStrengthToSignature]
SigWithStrengthToSignatureFunctor.Sig [variable, in Modules.Signatures.SigWithStrengthToSignature]
SigWithStrengthToSignatureMor [section, in Modules.Signatures.SigWithStrengthToSignature]
SigWithStrengthToSignatureMor.f [variable, in Modules.Signatures.SigWithStrengthToSignature]
SigWithStrengthToSignatureMor.Sig [variable, in Modules.Signatures.SigWithStrengthToSignature]
p _ [notation, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_functor [definition, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_is_functor [lemma, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_functor_data [definition, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_mor [definition, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_is_signature_Mor [lemma, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_mod_mor [definition, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_mod_mor_laws [lemma, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig [definition, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_is_signature [lemma, in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_data [definition, in Modules.Signatures.SigWithStrengthToSignature]
Sig_Lims_of_shape [definition, in Modules.Signatures.SignaturesColims]
Sig_Colims_of_shape [definition, in Modules.Signatures.SignaturesColims]
Sig_LimCone [definition, in Modules.Signatures.SignaturesColims]
Sig_ColimCocone [definition, in Modules.Signatures.SignaturesColims]
Sig_isLimCone [lemma, in Modules.Signatures.SignaturesColims]
Sig_isColimCocone [lemma, in Modules.Signatures.SignaturesColims]
Sig_limArrow [definition, in Modules.Signatures.SignaturesColims]
Sig_colimArrow [definition, in Modules.Signatures.SignaturesColims]
Sig_limArrow_laws [lemma, in Modules.Signatures.SignaturesColims]
Sig_colimArrow_laws [lemma, in Modules.Signatures.SignaturesColims]
Sig_lim_cone [definition, in Modules.Signatures.SignaturesColims]
Sig_colim_cocone [definition, in Modules.Signatures.SignaturesColims]
Sig_coneOut_commutes [lemma, in Modules.Signatures.SignaturesColims]
Sig_coconeIn_commutes [lemma, in Modules.Signatures.SignaturesColims]
Sig_coneOut [definition, in Modules.Signatures.SignaturesColims]
Sig_coconeIn [definition, in Modules.Signatures.SignaturesColims]
Sig_coneOut_laws [lemma, in Modules.Signatures.SignaturesColims]
Sig_coconeIn_laws [lemma, in Modules.Signatures.SignaturesColims]
Sig_lim [definition, in Modules.Signatures.SignaturesColims]
Sig_colim [definition, in Modules.Signatures.SignaturesColims]
Sig_lim_is_signature [lemma, in Modules.Signatures.SignaturesColims]
Sig_colim_is_signature [lemma, in Modules.Signatures.SignaturesColims]
Sig_lim_signature_data [definition, in Modules.Signatures.SignaturesColims]
Sig_colim_signature_data [definition, in Modules.Signatures.SignaturesColims]
Sig_lim_on_mor [definition, in Modules.Signatures.SignaturesColims]
Sig_colim_on_mor [definition, in Modules.Signatures.SignaturesColims]
sig_to_sig_over_functor [definition, in Modules.SoftEquations.SignatureOver]
sig_to_sig_over_is_functor [lemma, in Modules.SoftEquations.SignatureOver]
sig_sig_over_mor [definition, in Modules.SoftEquations.SignatureOver]
sig_over_data_from_sig [definition, in Modules.SoftEquations.SignatureOver]
sig_preservesNatEpiMonad_reduce_pw_SET [lemma, in Modules.Signatures.PreservesEpi]
sig_preservesNatEpiMonad_pw [definition, in Modules.Signatures.PreservesEpi]
sig_preservesNatEpiMonad [definition, in Modules.Signatures.PreservesEpi]
Sig_isDistributive [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
Sig_isDistributive_is_inverse [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
Sig_isDistributive_inv [definition, in Modules.Signatures.PresentableSignatureBinProdR]
Sig_isDistributive_inv_law [lemma, in Modules.Signatures.PresentableSignatureBinProdR]
soft_equations_preserve_initiality_choice [lemma, in Modules.SoftEquations.AdjunctionEquationRep]
soft_equations_preserve_initiality [lemma, in Modules.SoftEquations.AdjunctionEquationRep]
soft_equation_choice [definition, in Modules.SoftEquations.quotientequation]
soft_equation_isEpi [definition, in Modules.SoftEquations.quotientequation]
soft_equation_isSoft [definition, in Modules.SoftEquations.quotientequation]
soft_equation [definition, in Modules.SoftEquations.quotientequation]
source_abs_iso [definition, in Modules.SoftEquations.Examples.LCBetaEta]
source_app_iso [lemma, in Modules.SoftEquations.Examples.LCBetaEta]
source_equation [definition, in Modules.SoftEquations.Equation]
source_elem_epiSig [definition, in Modules.SoftEquations.quotientequation]
source_elem_eq [definition, in Modules.SoftEquations.quotientequation]
substitution [definition, in Modules.Prelims.deriveadj]
substitution [section, in Modules.Prelims.deriveadj]
substitution_nat_trans [definition, in Modules.Prelims.deriveadj]
substitution_laws [lemma, in Modules.Prelims.deriveadj]
substitution_nt [definition, in Modules.Prelims.deriveadj]
_ × _ (set_scope) [notation, in Modules.Prelims.deriveadj]
_ + _ (set_scope) [notation, in Modules.Prelims.deriveadj]
∂ [notation, in Modules.Prelims.deriveadj]
×ℜ [notation, in Modules.Prelims.deriveadj]
subst_is_nat_trans [lemma, in Modules.Prelims.deriveadj]
sumFuncs [abbreviation, in Modules.Signatures.BindingSig]
Summary [library]
sumSig [abbreviation, in Modules.Signatures.BindingSig]
T
T [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]T [abbreviation, in Modules.Prelims.deriveadj]
T [abbreviation, in Modules.Prelims.deriveadj]
T [abbreviation, in Modules.SoftEquations.Summary]
T [abbreviation, in Modules.SoftEquations.quotientequation]
target_equation [definition, in Modules.SoftEquations.Equation]
target_elem_eq [definition, in Modules.SoftEquations.quotientequation]
TautologicalPreserve [section, in Modules.Signatures.HssSignatureCommutation]
TautologicalPreserve.a [variable, in Modules.Signatures.HssSignatureCommutation]
TautologicalPreserve.b [variable, in Modules.Signatures.HssSignatureCommutation]
tautological_signature_over [definition, in Modules.SoftEquations.SignatureOver]
tautological_signature_over [definition, in Modules.SoftEquations.SignatureOverAsFiber]
tautological_signature_over_is_signature_over [lemma, in Modules.SoftEquations.SignatureOverAsFiber]
tautological_signature_over_data [definition, in Modules.SoftEquations.SignatureOverAsFiber]
tautological_signature_over_on_morphisms [definition, in Modules.SoftEquations.SignatureOverAsFiber]
tautological_signature_over_on_objects [definition, in Modules.SoftEquations.SignatureOverAsFiber]
tautological_signature [definition, in Modules.Signatures.Signature]
tautological_signature_is_signature [lemma, in Modules.Signatures.Signature]
tautological_signature_data [definition, in Modules.Signatures.Signature]
tautological_signature_on_morphisms [definition, in Modules.Signatures.Signature]
tautological_signature_on_objects [definition, in Modules.Signatures.Signature]
tautological_epiSig [definition, in Modules.Signatures.PreservesEpi]
tauto_sigs_har_iso [definition, in Modules.Signatures.HssSignatureCommutation]
TerminalSignature [definition, in Modules.Signatures.PresentableSignatureBinProdR]
Terminal_EndC_constant_terminal [definition, in Modules.Prelims.deriveadj]
TFunc [abbreviation, in Modules.Prelims.deriveadj]
toR' [definition, in Modules.Prelims.deriveadj]
toR'_MOD [definition, in Modules.Prelims.deriveadj]
toR'_laws [lemma, in Modules.Prelims.deriveadj]
toSig [abbreviation, in Modules.Signatures.BindingSig]
toSig [abbreviation, in Modules.Signatures.PresentableSignature]
transportf_bind [lemma, in Modules.Prelims.Opfibration]
transportf_postcompose_disp [lemma, in Modules.Prelims.Opfibration]
transport_signature_mor [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
transport_signature_mor [lemma, in Modules.Signatures.Signature]
TT [abbreviation, in Modules.SoftEquations.Modularity]
TT [abbreviation, in Modules.Prelims.FibrationInitialPushout]
TT [abbreviation, in Modules.Signatures.Modularity]
TwoMod_To_One_right_adjoint [definition, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSig [section, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature [definition, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_PushoutsSET [definition, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_CoproductsSET [definition, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_CoequalizersSET [definition, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_To_One_right_adjoint [definition, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_Mor_eq [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_Pushouts [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_Coproducts [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_Coequalizers [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_eqs [definition, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_index [definition, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_Mor [definition, in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_category [definition, in Modules.SoftEquations.CatOfTwoSignatures]
_ →→ _ [notation, in Modules.SoftEquations.CatOfTwoSignatures]
Two_to_OneMod_functor [definition, in Modules.SoftEquations.CatOfTwoSignatures]
Two_to_OneMod_is_functor [definition, in Modules.SoftEquations.CatOfTwoSignatures]
Two_to_OneMod_functor_data [definition, in Modules.SoftEquations.CatOfTwoSignatures]
two_mod_cleaving [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
two_model_disp [definition, in Modules.SoftEquations.CatOfTwoSignatures]
two_mod_axioms [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
two_mod_data [definition, in Modules.SoftEquations.CatOfTwoSignatures]
two_model_disp_ob_mor [definition, in Modules.SoftEquations.CatOfTwoSignatures]
two_model [definition, in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_is_coproduct [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_coproduct_in [definition, in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_coproduct [definition, in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_disp [definition, in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_axioms [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_data [definition, in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_comp_Mor [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_identity_Mor [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_disp_ob_mor [definition, in Modules.SoftEquations.CatOfTwoSignatures]
U
u [definition, in Modules.Prelims.quotientmonad]u [definition, in Modules.Prelims.quotientmonadslice]
u [definition, in Modules.Signatures.EpiSigRepresentability]
unique_lift_op [definition, in Modules.Prelims.Opfibration]
univalent_opfibration_is_cloven [definition, in Modules.Prelims.Opfibration]
universal_OneMod_to_TwoMod [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
universal_OneSig_to_TwoSig [lemma, in Modules.SoftEquations.CatOfTwoSignatures]
univ_surj_pb_lmod_nt_epi [definition, in Modules.SoftEquations.quotientrepslice]
univ_surj_pb_lmod_laws [lemma, in Modules.SoftEquations.quotientrepslice]
univ_pb_mod [section, in Modules.SoftEquations.quotientrepslice]
univ_surj_lmod_nt_epi [definition, in Modules.SoftEquations.quotientrepslice]
univ_surj_lmod_laws [lemma, in Modules.SoftEquations.quotientrepslice]
univ_mod [section, in Modules.SoftEquations.quotientrepslice]
u_monad_def [lemma, in Modules.Prelims.quotientmonad]
u_monad [definition, in Modules.Prelims.quotientmonad]
u_monad_laws [lemma, in Modules.Prelims.quotientmonad]
u_monad_mor_law2 [lemma, in Modules.Prelims.quotientmonad]
u_monad_mor_law1 [lemma, in Modules.Prelims.quotientmonad]
u_def_nt [lemma, in Modules.Prelims.quotientmonad]
u_def [lemma, in Modules.Prelims.quotientmonad]
u_monad_def [lemma, in Modules.Prelims.quotientmonadslice]
u_monad [definition, in Modules.Prelims.quotientmonadslice]
u_def_nt [lemma, in Modules.Prelims.quotientmonadslice]
u_def [lemma, in Modules.Prelims.quotientmonadslice]
u_rep_def [lemma, in Modules.SoftEquations.quotientrepslice]
u_rep [definition, in Modules.SoftEquations.quotientrepslice]
u_rep_laws [lemma, in Modules.SoftEquations.quotientrepslice]
u_rep_universal [lemma, in Modules.SoftEquations.AdjunctionEquationRep]
u_rep_arrow [definition, in Modules.SoftEquations.AdjunctionEquationRep]
u_rep_universal [lemma, in Modules.Signatures.EpiSigRepresentability]
u_rep_unique [lemma, in Modules.Signatures.EpiSigRepresentability]
u_rep [definition, in Modules.Signatures.EpiSigRepresentability]
u_rep_laws [lemma, in Modules.Signatures.EpiSigRepresentability]
u_def [lemma, in Modules.Signatures.EpiSigRepresentability]
u_rep_laws [lemma, in Modules.Signatures.quotientrep]
W
weak_opfibration [definition, in Modules.Prelims.Opfibration]WEQ [section, in Modules.Prelims.CoproductsComplements]
WEQ.a [variable, in Modules.Prelims.CoproductsComplements]
other
# _ (signature_over_scope) [notation, in Modules.SoftEquations.SignatureOver]# _ (signature_scope) [notation, in Modules.Signatures.Signature]
_ ××M _ [notation, in Modules.SoftEquations.Examples.LCBetaEta]
_ ×× _ [notation, in Modules.SoftEquations.Examples.LCBetaEta]
_ →→s _ [notation, in Modules.SoftEquations.Examples.LCBetaEta]
_ ;;; _ [notation, in Modules.Prelims.quotientmonad]
_ ∙∙ _ [notation, in Modules.Prelims.quotientmonad]
_ ;;; _ [notation, in Modules.Prelims.quotientmonadslice]
_ ∙∙ _ [notation, in Modules.Prelims.quotientmonadslice]
_ ⟹ _ [notation, in Modules.SoftEquations.Summary]
_ ^( _ ) [notation, in Modules.SoftEquations.Summary]
_ →→ _ [notation, in Modules.SoftEquations.Summary]
_ ′ [notation, in Modules.SoftEquations.Summary]
_ ::= _ [notation, in Modules.SoftEquations.Summary]
_ →→ _ [notation, in Modules.SoftEquations.quotientrepslice]
_ →→ _ [notation, in Modules.SoftEquations.AdjunctionEquationRep]
_ ∙∙ _ [notation, in Modules.Prelims.lib]
_ ⟶ _ [notation, in Modules.Prelims.lib]
_ □ _ [notation, in Modules.Prelims.lib]
_ →→ _ [notation, in Modules.SoftEquations.Equation]
_ →→ _ [notation, in Modules.SoftEquations.quotientequation]
_ ∘ _ [notation, in Modules.Signatures.quotientrep]
_ ø _ [notation, in Modules.Signatures.quotientrep]
_ ∙∙ _ [notation, in Modules.Signatures.quotientrep]
SET [notation, in Modules.Prelims.quotientmonad]
SET [notation, in Modules.Prelims.quotientmonadslice]
SET [notation, in Modules.Prelims.lib]
∂ [notation, in Modules.SoftEquations.Examples.LCBetaEta]
Θ [abbreviation, in Modules.SoftEquations.CatOfTwoSignatures]
Θ [abbreviation, in Modules.Signatures.ModelCat]
Θ [abbreviation, in Modules.Signatures.ModelCat]
Θ [abbreviation, in Modules.Prelims.deriveadj]
Θ [abbreviation, in Modules.Prelims.deriveadj]
Θ [abbreviation, in Modules.Prelims.deriveadj]
Θ [abbreviation, in Modules.Prelims.deriveadj]
Θ [abbreviation, in Modules.SoftEquations.SignatureOverAsFiber]
Θ [abbreviation, in Modules.SoftEquations.Summary]
Θ [abbreviation, in Modules.Signatures.Signature]
Θ [abbreviation, in Modules.Signatures.Signature]
Θ [abbreviation, in Modules.SoftEquations.quotientrepslice]
Θ [abbreviation, in Modules.SoftEquations.quotientequation]
Θ [abbreviation, in Modules.Signatures.quotientrep]
ΣΘ [abbreviation, in Modules.SoftEquations.Summary]
α' [abbreviation, in Modules.Signatures.SignatureCoproduct]
θ [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]
θ [abbreviation, in Modules.SoftEquations.BindingSig]
θ [abbreviation, in Modules.SoftEquations.quotientequation]
θ_nat_1_pw [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
θ_nat_2_pw [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
θ_nat_1_pw [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
θ_nat_2_pw [abbreviation, in Modules.Signatures.SigWithStrengthToSignature]
ι [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]
ι [abbreviation, in Modules.SoftEquations.Modularity]
ι [abbreviation, in Modules.SoftEquations.BindingSig]
ι [abbreviation, in Modules.SoftEquations.SignatureOver]
ι [abbreviation, in Modules.Signatures.Modularity]
ι [abbreviation, in Modules.SoftEquations.SignatureOverBinproducts]
ι1 [abbreviation, in Modules.Signatures.ModelCat]
ι2 [abbreviation, in Modules.Signatures.ModelCat]
π [abbreviation, in Modules.SoftEquations.quotientrepslice]
π [abbreviation, in Modules.SoftEquations.quotientequation]
π [abbreviation, in Modules.Signatures.quotientrep]
π_rep_laws [lemma, in Modules.SoftEquations.quotientrepslice]
σ [abbreviation, in Modules.Prelims.deriveadj]
σ [abbreviation, in Modules.Prelims.deriveadj]
σ [abbreviation, in Modules.Prelims.LModulesBinProducts]
σ [abbreviation, in Modules.SoftEquations.Equation]
σ [abbreviation, in Modules.SoftEquations.quotientequation]
σ [abbreviation, in Modules.Signatures.quotientrep]
σ' [abbreviation, in Modules.SoftEquations.quotientequation]
τ [abbreviation, in Modules.SoftEquations.Examples.LCBetaEta]
τ [abbreviation, in Modules.SoftEquations.Equation]
τ [abbreviation, in Modules.SoftEquations.quotientequation]
τ' [abbreviation, in Modules.SoftEquations.quotientequation]
τ' [abbreviation, in Modules.Signatures.quotientrep]
τ'_law_eq2 [lemma, in Modules.Signatures.quotientrep]
τ'_law_eq1 [lemma, in Modules.Signatures.quotientrep]
Notation Index
B
_ ×× _ [in Modules.SoftEquations.Examples.LCBetaEta]∂ [in Modules.SoftEquations.Examples.LCBetaEta]
D
∂ [in Modules.Signatures.SignatureDerivation]∂ [in Modules.SoftEquations.SignatureOverDerivation]
∂ [in Modules.SoftEquations.SignatureOverDerivation]
_ × _ (set_scope) [in Modules.Prelims.deriveadj]
_ + _ (set_scope) [in Modules.Prelims.deriveadj]
∂ [in Modules.Prelims.deriveadj]
×ℜ [in Modules.Prelims.deriveadj]
_ ×× _ [in Modules.Prelims.deriveadj]
∂ [in Modules.Prelims.deriveadj]
×ℜ [in Modules.Prelims.deriveadj]
_ ' [in Modules.Prelims.DerivationIsFunctorial]
∂ [in Modules.Prelims.DerivationIsFunctorial]
F
_ ×a _ [in Modules.Prelims.deriveadj]∂ [in Modules.Prelims.deriveadj]
I
_ ++f _ [in Modules.Signatures.ModelCat]_ + _ [in Modules.Signatures.ModelCat]
[[ _ , _ ]] [in Modules.Signatures.ModelCat]
L
## _ [in Modules.Signatures.EpiSigRepresentability]SET [in Modules.Signatures.EpiSigRepresentability]
p _ [in Modules.Signatures.SigWithStrengthToSignature]
O
_ ⟹ _ (signature_over_scope) [in Modules.SoftEquations.SignatureOver]# _ (signature_over_scope) [in Modules.SoftEquations.SignatureOver]
_ →→s _ [in Modules.SoftEquations.SignatureOver]
_ ;; _ [in Modules.SoftEquations.SignatureOver]
_ →→ _ [in Modules.SoftEquations.SignatureOver]
P
## [in Modules.Prelims.FibrationInitialPushout]Q
_ ^( _ ) [in Modules.SoftEquations.quotientequation]S
# _ (signature_over_scope) [in Modules.SoftEquations.SignatureOverAsFiber]_ ⟹ _ (signature_scope) [in Modules.Signatures.Signature]
# _ (signature_scope) [in Modules.Signatures.Signature]
_ ;; _ [in Modules.SoftEquations.SignatureOverAsFiber]
_ →→ _ [in Modules.SoftEquations.SignatureOverAsFiber]
p _ [in Modules.Signatures.SigWithStrengthToSignature]
_ × _ (set_scope) [in Modules.Prelims.deriveadj]
_ + _ (set_scope) [in Modules.Prelims.deriveadj]
∂ [in Modules.Prelims.deriveadj]
×ℜ [in Modules.Prelims.deriveadj]
T
_ →→ _ [in Modules.SoftEquations.CatOfTwoSignatures]other
# _ (signature_over_scope) [in Modules.SoftEquations.SignatureOver]# _ (signature_scope) [in Modules.Signatures.Signature]
_ ××M _ [in Modules.SoftEquations.Examples.LCBetaEta]
_ ×× _ [in Modules.SoftEquations.Examples.LCBetaEta]
_ →→s _ [in Modules.SoftEquations.Examples.LCBetaEta]
_ ;;; _ [in Modules.Prelims.quotientmonad]
_ ∙∙ _ [in Modules.Prelims.quotientmonad]
_ ;;; _ [in Modules.Prelims.quotientmonadslice]
_ ∙∙ _ [in Modules.Prelims.quotientmonadslice]
_ ⟹ _ [in Modules.SoftEquations.Summary]
_ ^( _ ) [in Modules.SoftEquations.Summary]
_ →→ _ [in Modules.SoftEquations.Summary]
_ ′ [in Modules.SoftEquations.Summary]
_ ::= _ [in Modules.SoftEquations.Summary]
_ →→ _ [in Modules.SoftEquations.quotientrepslice]
_ →→ _ [in Modules.SoftEquations.AdjunctionEquationRep]
_ ∙∙ _ [in Modules.Prelims.lib]
_ ⟶ _ [in Modules.Prelims.lib]
_ □ _ [in Modules.Prelims.lib]
_ →→ _ [in Modules.SoftEquations.Equation]
_ →→ _ [in Modules.SoftEquations.quotientequation]
_ ∘ _ [in Modules.Signatures.quotientrep]
_ ø _ [in Modules.Signatures.quotientrep]
_ ∙∙ _ [in Modules.Signatures.quotientrep]
SET [in Modules.Prelims.quotientmonad]
SET [in Modules.Prelims.quotientmonadslice]
SET [in Modules.Prelims.lib]
∂ [in Modules.SoftEquations.Examples.LCBetaEta]
Variable Index
B
Binprod.ab [in Modules.Signatures.SignatureBinproducts]Binprod.ab [in Modules.SoftEquations.SignatureOverBinproducts]
Binprod.cpFunc [in Modules.Signatures.SignatureBinproducts]
Binprod.cpFunc [in Modules.SoftEquations.SignatureOverBinproducts]
Binprod.cpLM [in Modules.Signatures.SignatureBinproducts]
Binprod.cpLM [in Modules.SoftEquations.SignatureOverBinproducts]
C
ColimsModule.d [in Modules.Prelims.LModulesColims]ColimsModule.d [in Modules.Prelims.LModulesCoproducts]
ColimsSig.coMod [in Modules.Signatures.SignaturesColims]
ColimsSig.d [in Modules.Signatures.SignaturesColims]
ColimsSig.d' [in Modules.Signatures.SignaturesColims]
ColimsSig.F [in Modules.Signatures.SignaturesColims]
ColimsSig.FORGET [in Modules.Signatures.SignaturesColims]
ColimsSig.F' [in Modules.Signatures.SignaturesColims]
ColimsSig.hsC [in Modules.Signatures.SignaturesColims]
ColimsSig.limMod [in Modules.Signatures.SignaturesColims]
commuteBinProdSig.a [in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.ar_b [in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.ar_a [in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.b [in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.bpSig [in Modules.Signatures.HssSignatureCommutation]
commuteBinProdSig.hss_bpSig [in Modules.Signatures.HssSignatureCommutation]
CoprodAr.ars [in Modules.Signatures.HssSignatureCommutation]
CoprodAr.b [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.Ba [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.bpFunct [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.bpMOD [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.bpSig [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.cpFunct [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.cpMOD [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.cpSig [in Modules.Signatures.HssSignatureCommutation]
CoprodAr.cpSig [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.epiBinProd [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.epiFa [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.Fa [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.FuncBP [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.FuncCP [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.hss_cpSig [in Modules.Signatures.HssSignatureCommutation]
CoprodAr.I [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.isDistC [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.MOD [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.p_alg_ar' [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.Sa' [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.sigs [in Modules.Signatures.HssSignatureCommutation]
CoprodAr.Sig_cp [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.Sig_bp [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodAr.toSig [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodBindingSig.ArToSig [in Modules.Signatures.BindingSig]
CoprodBindingSig.cpSig [in Modules.Signatures.BindingSig]
CoprodBindingSig.CP_from_BindingSig [in Modules.Signatures.BindingSig]
CoprodBindingSig.hsSig [in Modules.Signatures.BindingSig]
CoprodBindingSig.toSig [in Modules.Signatures.BindingSig]
CoprodPresentable.bind_α [in Modules.Signatures.PresentableSignatureCoproducts]
CoprodPresentable.cpSig [in Modules.Signatures.PresentableSignatureCoproducts]
CoprodPresentable.toSig [in Modules.Signatures.PresentableSignatureCoproducts]
CoprodPwIso.cpB'2 [in Modules.Prelims.CoproductsComplements]
CoprodSigma.BS [in Modules.Prelims.CoproductsComplements]
Coprod.cpFunc [in Modules.Signatures.SignatureCoproduct]
Coprod.cpLM [in Modules.Signatures.SignatureCoproduct]
D
DAr.a [in Modules.Signatures.SignatureDerivation]DAr.a [in Modules.SoftEquations.SignatureOverDerivation]
DAr.a [in Modules.SoftEquations.SignatureOverDerivation]
E
EpiSignatureSig.isEpiEpiFunc [in Modules.Signatures.BindingSig]EpiSignatureSig.isEpiSig [in Modules.Signatures.BindingSig]
G
GenericStrat.M1 [in Modules.Signatures.HssSignatureCommutation]GenericStrat.M2 [in Modules.Signatures.HssSignatureCommutation]
GenericStrat.Sf12_eq [in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S1 [in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S1 [in Modules.SoftEquations.SignatureOverBinproducts]
GenericStrat.S1_S2_R_iso [in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S1_data [in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S2 [in Modules.Signatures.HssSignatureCommutation]
GenericStrat.S2 [in Modules.SoftEquations.SignatureOverBinproducts]
GenericStrat.S2_data [in Modules.Signatures.HssSignatureCommutation]
L
leftadjoint.FF [in Modules.Signatures.EpiSigRepresentability]leftadjoint.fix_rep_of_a.ff [in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.dd [in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.J [in Modules.Signatures.EpiSigRepresentability]
leftadjoint.Rep_b [in Modules.Signatures.EpiSigRepresentability]
leftadjoint.Rep_a [in Modules.Signatures.EpiSigRepresentability]
O
oppr.faithful_opfibration [in Modules.Prelims.FaithfulFibrationEqualizer]OverSignatures.comp [in Modules.SoftEquations.SignatureOver]
P
PresentableDefinition.toSig [in Modules.Signatures.PresentableSignature]PresentableProjections.toSig [in Modules.Signatures.PresentableSignature]
pr.faithful_fibration [in Modules.Prelims.FaithfulFibrationEqualizer]
pr.ff1 [in Modules.Prelims.FibrationInitialPushout]
pr.ff2 [in Modules.Prelims.FibrationInitialPushout]
pr.gg1 [in Modules.Prelims.FibrationInitialPushout]
pr.gg2 [in Modules.Prelims.FibrationInitialPushout]
pullback_lims.lR [in Modules.Prelims.LModulesColims]
pullback_lims.cR [in Modules.Prelims.LModulesColims]
pullback_lims.lS [in Modules.Prelims.LModulesColims]
pullback_lims.cS [in Modules.Prelims.LModulesColims]
pullback_lims.dR [in Modules.Prelims.LModulesColims]
pullback_lims.dS [in Modules.Prelims.LModulesColims]
pullback_lims.lMod [in Modules.Prelims.LModulesColims]
pullback_lims.cMod [in Modules.Prelims.LModulesColims]
pullback_lims.MOD [in Modules.Prelims.LModulesColims]
pullback_binprod.cpFunc [in Modules.Prelims.LModulesBinProducts]
pullback_binprod.cpLM [in Modules.Prelims.LModulesBinProducts]
pullback_coprod.pbm_α [in Modules.Prelims.LModulesCoproducts]
pullback_coprod.αF [in Modules.Prelims.LModulesCoproducts]
pullback_coprod.cpFunc [in Modules.Prelims.LModulesCoproducts]
pullback_coprod.cpLM [in Modules.Prelims.LModulesCoproducts]
pwEpiAr.pushout_FF [in Modules.Signatures.EpiArePointwise]
Q
QuotientMonad.compatm [in Modules.Prelims.quotientmonad]QuotientMonad.compat_μ_projR [in Modules.Prelims.quotientmonad]
QuotientMonad.compat_m_rep [in Modules.Signatures.quotientrep]
QuotientMonad.equivc [in Modules.Prelims.quotientmonad]
QuotientMonad.equivc [in Modules.Signatures.quotientrep]
QuotientMonad.m [in Modules.Prelims.quotientmonad]
QuotientMonad.projR [in Modules.Prelims.quotientmonadslice]
QuotientMonad.projR [in Modules.Signatures.quotientrep]
QuotientMonad.projR_monad [in Modules.Signatures.quotientrep]
QuotientMonad.R' [in Modules.Prelims.quotientmonadslice]
QuotientMonad.R' [in Modules.Signatures.quotientrep]
QuotientMonad.R'_monad [in Modules.Signatures.quotientrep]
QuotientMonad.S [in Modules.Prelims.quotientmonad]
QuotientMonad.u_monad [in Modules.Signatures.quotientrep]
QuotientRep.choice [in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.d [in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.ff [in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.J [in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.projR [in Modules.SoftEquations.quotientrepslice]
QuotientRep.projR [in Modules.SoftEquations.quotientequation]
QuotientRep.projR_rep [in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.R' [in Modules.SoftEquations.quotientrepslice]
QuotientRep.R' [in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep.R' [in Modules.SoftEquations.quotientequation]
QuotientRep.u [in Modules.SoftEquations.quotientrepslice]
S
Signatures.comp [in Modules.SoftEquations.SignatureOverAsFiber]SigWithStrengthToSignatureFunctor.Sig [in Modules.Signatures.SigWithStrengthToSignature]
SigWithStrengthToSignatureMor.f [in Modules.Signatures.SigWithStrengthToSignature]
SigWithStrengthToSignatureMor.Sig [in Modules.Signatures.SigWithStrengthToSignature]
T
TautologicalPreserve.a [in Modules.Signatures.HssSignatureCommutation]TautologicalPreserve.b [in Modules.Signatures.HssSignatureCommutation]
W
WEQ.a [in Modules.Prelims.CoproductsComplements]Library Index
A
AdjunctionEquationRepB
BinCoproductComplementsBindingSig
BindingSig
BinProductComplements
C
CatOfTwoSignaturesCoproductsComplements
D
DerivationIsFunctorialderiveadj
E
EpiArePointwiseEpiComplements
EpiSigRepresentability
Equation
F
FaithfulFibrationEqualizerFibrationInitialPushout
H
HssInitialModelHssSignatureCommutation
L
LCBetaEtalib
LModulesBinProducts
LModulesColims
LModulesComplements
LModulesCoproducts
LModulesFibration
M
ModelCatModularity
Modularity
O
OpfibrationP
PresentableSignaturePresentableSignatureBinProdR
PresentableSignatureCoproducts
PreservesEpi
PushoutsFromCoeqBinCoproducts
Q
quotientequationquotientmonad
quotientmonadslice
quotientrep
quotientrepslice
S
SetCatComplementsSignature
SignatureBinproducts
SignatureCoproduct
SignatureDerivation
SignatureOver
SignatureOverAsFiber
SignatureOverBinproducts
SignatureOverDerivation
SignatureOverDerivation
SignaturesColims
SigWithStrengthToSignature
Summary
Lemma Index
A
abs_app_halfeq [in Modules.SoftEquations.Examples.LCBetaEta]ab_epi2 [in Modules.Signatures.EpiSigRepresentability]
adj_law2 [in Modules.Prelims.deriveadj]
adj_law1 [in Modules.Prelims.deriveadj]
algebraic_model_Epi [in Modules.Signatures.BindingSig]
algebraic_sig_effective [in Modules.Signatures.BindingSig]
algSig_NatEpi [in Modules.Signatures.PreservesEpi]
ArAreEpiEpiSig [in Modules.Signatures.BindingSig]
ArAreEpiSig [in Modules.Signatures.BindingSig]
arity_abs_eq [in Modules.SoftEquations.Examples.LCBetaEta]
arity_abs_mod_eq_mult [in Modules.SoftEquations.Examples.LCBetaEta]
assoc_ppprojR [in Modules.Prelims.quotientmonad]
B
bincoproduct_Epis [in Modules.Prelims.EpiComplements]BindingSigAreEpiEpiSig [in Modules.Signatures.BindingSig]
BindingSigAreEpiSig [in Modules.Signatures.BindingSig]
BindingSig_on_model_isEpi [in Modules.Signatures.BindingSig]
BinProductWith1_is_inverse [in Modules.Prelims.BinProductComplements]
BinProduct_pw_eq_id [in Modules.Prelims.BinProductComplements]
BinProduct_commutative_id_commute [in Modules.Prelims.BinProductComplements]
binprod_sigs_har_eq [in Modules.Signatures.HssSignatureCommutation]
binprod_sigs_har_mod_eq_mult [in Modules.Signatures.HssSignatureCommutation]
binprod_pbm_to_pbm_eq_mult [in Modules.Prelims.LModulesBinProducts]
binProd_epiSig [in Modules.Signatures.PreservesEpi]
bmod_axioms [in Modules.Prelims.LModulesFibration]
bmod_transport [in Modules.Prelims.LModulesFibration]
C
cancel_ar_on [in Modules.Signatures.EpiSigRepresentability]catiso_initial [in Modules.Prelims.lib]
changef_path_pw [in Modules.Prelims.lib]
changef_path [in Modules.Prelims.lib]
colimOfArrows_Epi [in Modules.Prelims.EpiComplements]
Colim_Functor_Preserves_Epi [in Modules.Prelims.EpiComplements]
commutes_binproduct_derivation_laws [in Modules.Prelims.deriveadj]
compat_μ_slice [in Modules.Prelims.quotientmonadslice]
compat_slice [in Modules.Prelims.quotientmonadslice]
compat_model_τ_projR [in Modules.Signatures.EpiSigRepresentability]
comp_cat_comp [in Modules.Prelims.lib]
congr_equivc [in Modules.Prelims.quotientmonadslice]
Const1Sig_isTerminal [in Modules.Signatures.PresentableSignatureBinProdR]
CoproductOfArrows_isEpi [in Modules.Prelims.CoproductsComplements]
coproduct_Epis [in Modules.Prelims.EpiComplements]
coprod_sigs_har_eq [in Modules.Signatures.HssSignatureCommutation]
coprod_sigs_har_mod_eq_mult [in Modules.Signatures.HssSignatureCommutation]
coprod_pbm_to_pbm_coprod_aux [in Modules.Prelims.LModulesCoproducts]
coprod_epi_p_mor [in Modules.Signatures.PresentableSignatureCoproducts]
counit_subst_adjunction [in Modules.Prelims.deriveadj]
D
deriv_adj [in Modules.Prelims.deriveadj]deriv_counit_is_nat_trans [in Modules.Prelims.deriveadj]
deriv_epiSig [in Modules.Signatures.PreservesEpi]
disp_InitialArrowUnique [in Modules.Prelims.FibrationInitialPushout]
disp_mor_unique_disc_opfib [in Modules.Prelims.Opfibration]
E
elementary_equations_preserve_initiality_choice [in Modules.SoftEquations.AdjunctionEquationRep]elementary_equations_preserve_initiality [in Modules.SoftEquations.AdjunctionEquationRep]
epiSigR' [in Modules.SoftEquations.quotientrepslice]
epiSig_equiv_pwEpi_SET [in Modules.Signatures.EpiArePointwise]
epiSig_is_pwEpi [in Modules.Signatures.EpiArePointwise]
epiSig_NatEpi [in Modules.Signatures.PreservesEpi]
epi_nt_preserves_Epi [in Modules.Prelims.EpiComplements]
epi_nt_SET_pw [in Modules.Prelims.EpiComplements]
eq_projR_rel [in Modules.Prelims.quotientmonad]
eq_mr [in Modules.Signatures.EpiSigRepresentability]
F
faithful_opfibration_coequalizer [in Modules.Prelims.FaithfulFibrationEqualizer]faithful_fibration_equalizer [in Modules.Prelims.FaithfulFibrationEqualizer]
faithful_reformulated [in Modules.Prelims.FaithfulFibrationEqualizer]
fib_to_dir_is_functor [in Modules.SoftEquations.CatOfTwoSignatures]
fib_to_dir_is_functor [in Modules.Signatures.ModelCat]
functorial_counit_derivadj [in Modules.Prelims.deriveadj]
functor_cat_isDistributive [in Modules.Signatures.PresentableSignatureBinProdR]
H
hab_alt [in Modules.Signatures.EpiSigRepresentability]har_binprodR_epi_p_mor [in Modules.Signatures.PresentableSignatureBinProdR]
helper [in Modules.Signatures.ModelCat]
helper [in Modules.Signatures.EpiSigRepresentability]
horcomp_assoc [in Modules.Prelims.lib]
hset_category_isDistributive [in Modules.Prelims.SetCatComplements]
hss_sig_effective [in Modules.Signatures.HssInitialModel]
hss_initial_arrow_unique [in Modules.Signatures.HssInitialModel]
hss_initial_model [in Modules.Signatures.HssInitialModel]
I
initial_cl_lift_square_eq [in Modules.Prelims.FibrationInitialPushout]initial_universal_to_lift_initial [in Modules.Prelims.lib]
isaprop_rep_fiber_mor_law [in Modules.Signatures.ModelCat]
isaprop_is_signature_over_Mor [in Modules.SoftEquations.SignatureOver]
isaprop_is_signature_over [in Modules.SoftEquations.SignatureOver]
isaprop_is_signature_over [in Modules.SoftEquations.SignatureOverAsFiber]
isaprop_equivc_xy [in Modules.Prelims.quotientmonadslice]
isaprop_disc_opfib_hom [in Modules.Prelims.Opfibration]
isaprop_is_cocartesian [in Modules.Prelims.Opfibration]
isaprop_model_mor_law [in Modules.Signatures.Signature]
isaprop_is_signature_Mor [in Modules.Signatures.Signature]
isaprop_is_signature [in Modules.Signatures.Signature]
isaset_rep_fiber_mor [in Modules.Signatures.ModelCat]
isaset_signature_over_Mor [in Modules.SoftEquations.SignatureOver]
isaset_model_mor_mor [in Modules.Signatures.Signature]
isaset_signature_Mor [in Modules.Signatures.Signature]
isEpiBinProdHSET [in Modules.Prelims.SetCatComplements]
isEpi_beta_sig_source [in Modules.SoftEquations.Examples.LCBetaEta]
isEpi_projR_monad [in Modules.Prelims.quotientmonad]
isEpi_projR_projR_projR_pw [in Modules.Prelims.quotientmonad]
isEpi_projR_projR [in Modules.Prelims.quotientmonad]
isEpi_R_projR_projR_pw [in Modules.Prelims.quotientmonad]
isEpi_projR_projR_pw [in Modules.Prelims.quotientmonad]
isEpi_projR [in Modules.Prelims.quotientmonad]
isEpi_RprojR_pw [in Modules.Prelims.quotientmonad]
isEpi_projR_pw [in Modules.Prelims.quotientmonad]
isEpi_horcomp_pw2 [in Modules.Prelims.EpiComplements]
isEpi_horcomp_pw [in Modules.Prelims.EpiComplements]
isEpi_projR_rep [in Modules.SoftEquations.quotientrepslice]
isEpi_binProdSig [in Modules.Signatures.BindingSig]
isEpi_def_R'_model_τ [in Modules.Signatures.EpiSigRepresentability]
iseqrel_equivc [in Modules.Prelims.quotientmonadslice]
isoRIdM [in Modules.Signatures.ModelCat]
isounit_coreflection [in Modules.Prelims.lib]
iso_mod_id_model [in Modules.Signatures.ModelCat]
isSoft_finite_deriv_tauto [in Modules.SoftEquations.quotientequation]
isSoft_derivative [in Modules.SoftEquations.quotientequation]
isSoft_tauto [in Modules.SoftEquations.quotientequation]
is_precategory_rep_fiber_precategory_data [in Modules.Signatures.ModelCat]
is_rep_fiber_comp [in Modules.Signatures.ModelCat]
is_rep_fiber_id [in Modules.Signatures.ModelCat]
is_precategory_signature_over_precategory_data [in Modules.SoftEquations.SignatureOver]
is_signature_over_Mor_comp [in Modules.SoftEquations.SignatureOver]
is_signature_over_Mor_id [in Modules.SoftEquations.SignatureOver]
is_sig_over_from_sig [in Modules.SoftEquations.SignatureOver]
is_precategory_signature_precategory_data [in Modules.Signatures.Signature]
is_signature_Mor_id [in Modules.Signatures.Signature]
is_signature_Mor_comp [in Modules.Signatures.Signature]
is_iso_from_Coproduct_to_Coproduct [in Modules.Prelims.CoproductsComplements]
is_right_adjoint_functor_of_reps_from_pw_epi_choice [in Modules.Signatures.EpiSigRepresentability]
is_right_adjoint_functor_of_reps_from_pw_epi [in Modules.Signatures.EpiSigRepresentability]
L
lift_pb_LModule_iso [in Modules.Signatures.SigWithStrengthToSignature]lift_pb_LModule_eq_mult [in Modules.Signatures.SigWithStrengthToSignature]
lift_lmodule_mor_law [in Modules.Signatures.SigWithStrengthToSignature]
LModule_to_deriv_is_nt [in Modules.Prelims.DerivationIsFunctorial]
LModule_to_deriv_laws [in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_is_functor [in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_Mor_laws [in Modules.Prelims.DerivationIsFunctorial]
LModule_isLimCone [in Modules.Prelims.LModulesColims]
LModule_isColimCocone [in Modules.Prelims.LModulesColims]
LModule_coneOut_commutes [in Modules.Prelims.LModulesColims]
LModule_coconeIn_commutes [in Modules.Prelims.LModulesColims]
LModule_coneOut_laws [in Modules.Prelims.LModulesColims]
LModule_coconeIn_laws [in Modules.Prelims.LModulesColims]
LModule_lim_laws [in Modules.Prelims.LModulesColims]
LModule_colim_laws [in Modules.Prelims.LModulesColims]
LModule_lim_mult_is_nat_trans [in Modules.Prelims.LModulesColims]
LModule_colim_mult_is_nat_trans [in Modules.Prelims.LModulesColims]
LModule_isBinProductCone [in Modules.Prelims.LModulesBinProducts]
LModule_BinProductPr2Commutes [in Modules.Prelims.LModulesBinProducts]
LModule_BinProductPr1Commutes [in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr2_laws [in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr1_laws [in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_laws [in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_mult_is_nat_trans [in Modules.Prelims.LModulesBinProducts]
LModule_isCoproduct [in Modules.Prelims.LModulesCoproducts]
LModule_coproductIn_laws [in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_laws [in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_mult_is_nat_trans [in Modules.Prelims.LModulesCoproducts]
LMod_isDistributive [in Modules.Signatures.PresentableSignatureBinProdR]
LMod_isDistributive_is_inverse [in Modules.Signatures.PresentableSignatureBinProdR]
LMod_isDistributive_inv_laws [in Modules.Signatures.PresentableSignatureBinProdR]
M
model_mor_mor_equiv [in Modules.Signatures.Signature]mod_M_idM_mod_laws [in Modules.Signatures.ModelCat]
mod_id_monad_mor_laws [in Modules.Signatures.ModelCat]
mod_id_monad_laws [in Modules.Signatures.ModelCat]
mod_id_M_mod_law2 [in Modules.Signatures.ModelCat]
mod_id_M_mod_law1 [in Modules.Signatures.ModelCat]
monad_mor_to_lmodule_law [in Modules.Prelims.LModulesComplements]
O
OneMod_to_TwoMod_fully_faithful [in Modules.SoftEquations.CatOfTwoSignatures]OneSig_to_TwoSig_fully_faithful [in Modules.SoftEquations.CatOfTwoSignatures]
P
pb_rep_comp [in Modules.SoftEquations.CatOfTwoSignatures]pb_rep_id [in Modules.SoftEquations.CatOfTwoSignatures]
pb_rep_mor_id [in Modules.Signatures.ModelCat]
pb_rep_mor_comp [in Modules.Signatures.ModelCat]
pb_rep_mor_law [in Modules.Signatures.ModelCat]
pb_lims_eq_mult [in Modules.Prelims.LModulesColims]
pb_colims_eq_mult [in Modules.Prelims.LModulesColims]
pb_rep_to_law [in Modules.Signatures.Signature]
po_is_signature_over [in Modules.SoftEquations.SignatureOver]
PO_eqdiag [in Modules.Signatures.EpiArePointwise]
precompEpiEpiFunc [in Modules.Signatures.BindingSig]
precompEpiEpiFuncSn [in Modules.Signatures.BindingSig]
precompEpiFunc [in Modules.Signatures.BindingSig]
precomp_func_preserveEpi [in Modules.Signatures.BindingSig]
PresentableisEffective [in Modules.Signatures.PresentableSignature]
preserveEpi_precomp [in Modules.Prelims.EpiComplements]
preserveEpi_binCoprodFunc [in Modules.Prelims.EpiComplements]
preserveEpi_sumFuncs [in Modules.Prelims.EpiComplements]
preserveEpi_binProdFunc [in Modules.Prelims.EpiComplements]
preserves_Epi_option [in Modules.Prelims.EpiComplements]
preserves_to_HSET_isEpi [in Modules.Prelims.EpiComplements]
pre_subst_is_nat_trans [in Modules.Prelims.deriveadj]
productEpisFunc [in Modules.Prelims.EpiComplements]
productEpisSET [in Modules.Prelims.EpiComplements]
projR_monad_laws [in Modules.Prelims.quotientmonad]
projR_rep_laws [in Modules.Signatures.EpiSigRepresentability]
pushout_total_initial [in Modules.Prelims.FibrationInitialPushout]
pushout_total [in Modules.Prelims.FibrationInitialPushout]
push_initiality_weaker_choice [in Modules.Signatures.EpiSigRepresentability]
push_initiality [in Modules.Signatures.EpiSigRepresentability]
push_initiality_weaker [in Modules.Signatures.EpiSigRepresentability]
pwEpiSig_isEpi [in Modules.Signatures.EpiArePointwise]
R
rel_eq_projR [in Modules.Prelims.quotientmonad]rep_mor_to_alg_is_alg_mor [in Modules.Signatures.HssInitialModel]
rep_fiber_category_has_homsets [in Modules.Signatures.ModelCat]
rep_fiber_mor_eq [in Modules.Signatures.ModelCat]
rep_fiber_mor_eq_nt [in Modules.Signatures.ModelCat]
rep_cleaving [in Modules.Signatures.Signature]
rep_mor_pb [in Modules.Signatures.Signature]
rep_mor_law_pb [in Modules.Signatures.Signature]
rep_axioms [in Modules.Signatures.Signature]
rep_comp_law [in Modules.Signatures.Signature]
rep_id_law [in Modules.Signatures.Signature]
Rep_mor_is_composition [in Modules.Signatures.EpiSigRepresentability]
R'_preserves_Epi [in Modules.Prelims.quotientmonad]
R'_Monad_laws [in Modules.Prelims.quotientmonad]
R'_Monad_law_μ [in Modules.Prelims.quotientmonad]
R'_Monad_law_η2 [in Modules.Prelims.quotientmonad]
R'_Monad_law_η1 [in Modules.Prelims.quotientmonad]
R'_μ_def [in Modules.Prelims.quotientmonad]
R'_action_compat [in Modules.SoftEquations.quotientrepslice]
R'_satisfies_eq [in Modules.SoftEquations.quotientequation]
R'_model_τ_module_laws [in Modules.Signatures.quotientrep]
S
signature_S1_S2_is_inverse [in Modules.Signatures.HssSignatureCommutation]signature_to_deriv_laws [in Modules.Signatures.SignatureDerivation]
signature_deriv_is_signature [in Modules.Signatures.SignatureDerivation]
signature_over_category_has_homsets [in Modules.SoftEquations.SignatureOver]
signature_over_Mor_eq [in Modules.SoftEquations.SignatureOver]
signature_over_Mor_ax_pw [in Modules.SoftEquations.SignatureOver]
signature_over_deriv_is_signature_over [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_is_signature_over [in Modules.SoftEquations.SignatureOverDerivation]
signature_isBinProduct [in Modules.Signatures.SignatureBinproducts]
signature_binProductPr2_laws [in Modules.Signatures.SignatureBinproducts]
signature_binProductPr1_laws [in Modules.Signatures.SignatureBinproducts]
signature_binProd_is_signature [in Modules.Signatures.SignatureBinproducts]
signature_isCoproduct [in Modules.Signatures.SignatureCoproduct]
signature_coproductIn_laws [in Modules.Signatures.SignatureCoproduct]
signature_coprod_is_signature [in Modules.Signatures.SignatureCoproduct]
signature_category_has_homsets [in Modules.Signatures.Signature]
signature_Mor_eq [in Modules.Signatures.Signature]
signature_Mor_ax_pw [in Modules.Signatures.Signature]
Signature_to_signature_cons_iso [in Modules.Signatures.PresentableSignatureBinProdR]
signature_over_S1_S2_is_inverse [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S2_S1_laws [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S1_S2_laws [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_isBinProduct [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductPr2_laws [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductPr1_laws [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProd_is_signature_over [in Modules.SoftEquations.SignatureOverBinproducts]
sigWithStrength_to_sig_is_functor [in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_is_signature_Mor [in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_mod_mor_laws [in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_is_signature [in Modules.Signatures.SigWithStrengthToSignature]
Sig_isLimCone [in Modules.Signatures.SignaturesColims]
Sig_isColimCocone [in Modules.Signatures.SignaturesColims]
Sig_limArrow_laws [in Modules.Signatures.SignaturesColims]
Sig_colimArrow_laws [in Modules.Signatures.SignaturesColims]
Sig_coneOut_commutes [in Modules.Signatures.SignaturesColims]
Sig_coconeIn_commutes [in Modules.Signatures.SignaturesColims]
Sig_coneOut_laws [in Modules.Signatures.SignaturesColims]
Sig_coconeIn_laws [in Modules.Signatures.SignaturesColims]
Sig_lim_is_signature [in Modules.Signatures.SignaturesColims]
Sig_colim_is_signature [in Modules.Signatures.SignaturesColims]
sig_to_sig_over_is_functor [in Modules.SoftEquations.SignatureOver]
sig_preservesNatEpiMonad_reduce_pw_SET [in Modules.Signatures.PreservesEpi]
Sig_isDistributive [in Modules.Signatures.PresentableSignatureBinProdR]
Sig_isDistributive_is_inverse [in Modules.Signatures.PresentableSignatureBinProdR]
Sig_isDistributive_inv_law [in Modules.Signatures.PresentableSignatureBinProdR]
soft_equations_preserve_initiality_choice [in Modules.SoftEquations.AdjunctionEquationRep]
soft_equations_preserve_initiality [in Modules.SoftEquations.AdjunctionEquationRep]
source_app_iso [in Modules.SoftEquations.Examples.LCBetaEta]
substitution_laws [in Modules.Prelims.deriveadj]
subst_is_nat_trans [in Modules.Prelims.deriveadj]
T
tautological_signature_over_is_signature_over [in Modules.SoftEquations.SignatureOverAsFiber]tautological_signature_is_signature [in Modules.Signatures.Signature]
toR'_laws [in Modules.Prelims.deriveadj]
transportf_bind [in Modules.Prelims.Opfibration]
transportf_postcompose_disp [in Modules.Prelims.Opfibration]
transport_signature_mor [in Modules.SoftEquations.CatOfTwoSignatures]
transport_signature_mor [in Modules.Signatures.Signature]
TwoSignature_Mor_eq [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_Pushouts [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_Coproducts [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_Coequalizers [in Modules.SoftEquations.CatOfTwoSignatures]
two_mod_cleaving [in Modules.SoftEquations.CatOfTwoSignatures]
two_mod_axioms [in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_is_coproduct [in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_axioms [in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_comp_Mor [in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_identity_Mor [in Modules.SoftEquations.CatOfTwoSignatures]
U
universal_OneMod_to_TwoMod [in Modules.SoftEquations.CatOfTwoSignatures]universal_OneSig_to_TwoSig [in Modules.SoftEquations.CatOfTwoSignatures]
univ_surj_pb_lmod_laws [in Modules.SoftEquations.quotientrepslice]
univ_surj_lmod_laws [in Modules.SoftEquations.quotientrepslice]
u_monad_def [in Modules.Prelims.quotientmonad]
u_monad_laws [in Modules.Prelims.quotientmonad]
u_monad_mor_law2 [in Modules.Prelims.quotientmonad]
u_monad_mor_law1 [in Modules.Prelims.quotientmonad]
u_def_nt [in Modules.Prelims.quotientmonad]
u_def [in Modules.Prelims.quotientmonad]
u_monad_def [in Modules.Prelims.quotientmonadslice]
u_def_nt [in Modules.Prelims.quotientmonadslice]
u_def [in Modules.Prelims.quotientmonadslice]
u_rep_def [in Modules.SoftEquations.quotientrepslice]
u_rep_laws [in Modules.SoftEquations.quotientrepslice]
u_rep_universal [in Modules.SoftEquations.AdjunctionEquationRep]
u_rep_universal [in Modules.Signatures.EpiSigRepresentability]
u_rep_unique [in Modules.Signatures.EpiSigRepresentability]
u_rep_laws [in Modules.Signatures.EpiSigRepresentability]
u_def [in Modules.Signatures.EpiSigRepresentability]
u_rep_laws [in Modules.Signatures.quotientrep]
other
π_rep_laws [in Modules.SoftEquations.quotientrepslice]τ'_law_eq2 [in Modules.Signatures.quotientrep]
τ'_law_eq1 [in Modules.Signatures.quotientrep]
Section Index
A
all_purpose [in Modules.Signatures.EpiSigRepresentability]B
BindingSigOp [in Modules.SoftEquations.Examples.LCBetaEta]Binprod [in Modules.Signatures.SignatureBinproducts]
Binprod [in Modules.SoftEquations.SignatureOverBinproducts]
BinProdComplements [in Modules.Prelims.BinProductComplements]
BinProductsLModule [in Modules.Prelims.LModulesBinProducts]
C
ColimsModule [in Modules.Prelims.LModulesColims]ColimsModule [in Modules.Prelims.LModulesCoproducts]
ColimsSig [in Modules.Signatures.SignaturesColims]
commuteBinProdSig [in Modules.Signatures.HssSignatureCommutation]
Coprod [in Modules.Signatures.SignatureCoproduct]
CoprodAr [in Modules.Signatures.HssSignatureCommutation]
CoprodAr [in Modules.Signatures.PresentableSignatureBinProdR]
CoprodBindingSig [in Modules.Signatures.BindingSig]
CoprodBinprod [in Modules.Prelims.CoproductsComplements]
CoprodEpis [in Modules.Prelims.CoproductsComplements]
CoprodPresentable [in Modules.Signatures.PresentableSignatureCoproducts]
CoprodPwIso [in Modules.Prelims.CoproductsComplements]
CoprodSigma [in Modules.Prelims.CoproductsComplements]
coproduct_unique [in Modules.Prelims.CoproductsComplements]
D
d [in Modules.Prelims.PushoutsFromCoeqBinCoproducts]DAr [in Modules.Signatures.SignatureDerivation]
DAr [in Modules.SoftEquations.SignatureOverDerivation]
DAr [in Modules.SoftEquations.SignatureOverDerivation]
derivadj [in Modules.Prelims.deriveadj]
DerivCounit [in Modules.Prelims.deriveadj]
DerivFunctor [in Modules.Prelims.DerivationIsFunctorial]
Discrete_OpFibrations [in Modules.Prelims.Opfibration]
E
EpiSignatureSig [in Modules.Signatures.HssInitialModel]EpiSignatureSig [in Modules.Signatures.BindingSig]
Equation [in Modules.SoftEquations.Equation]
F
ForgetSigFunctor [in Modules.Signatures.Signature]Functoriality [in Modules.Prelims.deriveadj]
G
GenericStrat [in Modules.Signatures.HssSignatureCommutation]GenericStrat [in Modules.SoftEquations.SignatureOverBinproducts]
I
InitAlg [in Modules.Signatures.ModelCat]InitAlg2 [in Modules.Signatures.ModelCat]
L
LargeCatMod [in Modules.Prelims.LModulesFibration]LargeCatRep [in Modules.Signatures.Signature]
leftadjoint [in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.uModel [in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.R'Model [in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a.Instantiating_Quotient_Constructions [in Modules.Signatures.EpiSigRepresentability]
leftadjoint.fix_rep_of_a [in Modules.Signatures.EpiSigRepresentability]
LiftLModuleMor [in Modules.Signatures.SigWithStrengthToSignature]
M
ModelCat [in Modules.Signatures.ModelCat]O
Opfibrations [in Modules.Prelims.Opfibration]oppr [in Modules.Prelims.FaithfulFibrationEqualizer]
OverSignatures [in Modules.SoftEquations.SignatureOver]
P
pr [in Modules.Prelims.FibrationInitialPushout]pr [in Modules.Prelims.FaithfulFibrationEqualizer]
PresentableDefinition [in Modules.Signatures.PresentableSignature]
PresentableProjections [in Modules.Signatures.PresentableSignature]
ProductModule [in Modules.Prelims.LModulesBinProducts]
pullback_lims [in Modules.Prelims.LModulesColims]
pullback_binprod [in Modules.Prelims.LModulesBinProducts]
pullback_coprod [in Modules.Prelims.LModulesCoproducts]
PushoutOverSig [in Modules.SoftEquations.SignatureOver]
pwEpiAr [in Modules.Signatures.EpiArePointwise]
Q
QuotientMonad [in Modules.Prelims.quotientmonad]QuotientMonad [in Modules.Prelims.quotientmonadslice]
QuotientMonad [in Modules.Signatures.quotientrep]
QuotientRep [in Modules.SoftEquations.quotientrepslice]
QuotientRep [in Modules.SoftEquations.AdjunctionEquationRep]
QuotientRep [in Modules.SoftEquations.quotientequation]
QuotientRepInit [in Modules.SoftEquations.AdjunctionEquationRep]
S
Signatures [in Modules.SoftEquations.SignatureOverAsFiber]Signatures [in Modules.Signatures.Signature]
SigWithStrengthToSignature [in Modules.Signatures.SigWithStrengthToSignature]
SigWithStrengthToSignatureFunctor [in Modules.Signatures.SigWithStrengthToSignature]
SigWithStrengthToSignatureMor [in Modules.Signatures.SigWithStrengthToSignature]
substitution [in Modules.Prelims.deriveadj]
T
TautologicalPreserve [in Modules.Signatures.HssSignatureCommutation]TwoSig [in Modules.SoftEquations.CatOfTwoSignatures]
U
univ_pb_mod [in Modules.SoftEquations.quotientrepslice]univ_mod [in Modules.SoftEquations.quotientrepslice]
W
WEQ [in Modules.Prelims.CoproductsComplements]Abbreviation Index
A
ArToSig [in Modules.Signatures.BindingSig]B
BC [in Modules.Signatures.ModelCat]BC [in Modules.SoftEquations.Summary]
BC [in Modules.SoftEquations.quotientequation]
bcO [in Modules.Signatures.ModelCat]
BCP [in Modules.SoftEquations.Examples.LCBetaEta]
bcpS [in Modules.Prelims.deriveadj]
bcpS [in Modules.Prelims.deriveadj]
binProdFunc [in Modules.Signatures.BindingSig]
binProdSig [in Modules.Signatures.BindingSig]
BMOD [in Modules.Signatures.Signature]
BMOD [in Modules.Signatures.Signature]
BP [in Modules.SoftEquations.Examples.LCBetaEta]
BP [in Modules.Prelims.LModulesBinProducts]
bpCC [in Modules.Prelims.deriveadj]
bpFunc [in Modules.Prelims.deriveadj]
bpFunct [in Modules.Prelims.LModulesBinProducts]
BPO [in Modules.SoftEquations.Examples.LCBetaEta]
BPO [in Modules.Prelims.BinProductComplements]
BPO [in Modules.Signatures.HssSignatureCommutation]
BPO [in Modules.Signatures.SignatureBinproducts]
BPO [in Modules.Prelims.LModulesBinProducts]
BPO [in Modules.Prelims.CoproductsComplements]
BPO [in Modules.SoftEquations.SignatureOverBinproducts]
bpS [in Modules.Prelims.deriveadj]
bpS [in Modules.Prelims.deriveadj]
C
CAT_SIGNATURE [in Modules.Signatures.EpiSigRepresentability]coFunc [in Modules.Prelims.LModulesColims]
counit [in Modules.Prelims.deriveadj]
CP [in Modules.SoftEquations.Examples.LCBetaEta]
cpFunc [in Modules.Prelims.LModulesCoproducts]
CPO [in Modules.SoftEquations.Examples.LCBetaEta]
CPO [in Modules.Signatures.HssSignatureCommutation]
CPO [in Modules.Prelims.CoproductsComplements]
CPO [in Modules.Prelims.CoproductsComplements]
CPO [in Modules.Prelims.CoproductsComplements]
CPO [in Modules.Signatures.PresentableSignatureBinProdR]
CPO [in Modules.Signatures.PresentableSignatureCoproducts]
Cset [in Modules.Signatures.BindingSig]
D
d' [in Modules.Prelims.LModulesColims]d' [in Modules.Prelims.LModulesCoproducts]
E
EndAlg [in Modules.Signatures.HssInitialModel]EndSet [in Modules.Signatures.HssInitialModel]
EndSet [in Modules.Signatures.BindingSig]
EndSet [in Modules.Signatures.PresentableSignature]
EQS [in Modules.SoftEquations.CatOfTwoSignatures]
F
F [in Modules.Prelims.LModulesColims]F [in Modules.Prelims.LModulesBinProducts]
F [in Modules.Signatures.SigWithStrengthToSignature]
F [in Modules.Signatures.SigWithStrengthToSignature]
F [in Modules.Prelims.LModulesCoproducts]
faithful_reformulated [in Modules.Prelims.FaithfulFibrationEqualizer]
FIBER_CAT [in Modules.SoftEquations.CatOfTwoSignatures]
FIBER_CAT [in Modules.Signatures.ModelCat]
FORGET [in Modules.Prelims.LModulesColims]
FS [in Modules.Signatures.ModelCat]
FSmor [in Modules.SoftEquations.CatOfTwoSignatures]
FSmor [in Modules.Signatures.ModelCat]
FSob [in Modules.Signatures.ModelCat]
F' [in Modules.Prelims.LModulesColims]
H
HAR [in Modules.Signatures.SignaturesColims]HAR [in Modules.Signatures.Signature]
hom_SET [in Modules.Signatures.HssInitialModel]
hom_SET [in Modules.Signatures.BindingSig]
hom_SET [in Modules.Signatures.PresentableSignature]
hsC [in Modules.SoftEquations.Examples.LCBetaEta]
hsC [in Modules.Prelims.deriveadj]
hsC [in Modules.Signatures.SignatureBinproducts]
hsC [in Modules.Signatures.SignatureCoproduct]
hsC [in Modules.Signatures.SigWithStrengthToSignature]
hsC [in Modules.SoftEquations.SignatureOverBinproducts]
hsS [in Modules.Prelims.deriveadj]
hsS [in Modules.Prelims.deriveadj]
I
ID [in Modules.Signatures.ModelCat]IdM [in Modules.Signatures.ModelCat]
IdM [in Modules.Signatures.ModelCat]
iniHSS [in Modules.Signatures.HssInitialModel]
L
liftlmodule [in Modules.Signatures.SigWithStrengthToSignature]liftlmodule [in Modules.Signatures.SigWithStrengthToSignature]
limFunc [in Modules.Prelims.LModulesColims]
LMOD [in Modules.Prelims.DerivationIsFunctorial]
LMOD [in Modules.Prelims.deriveadj]
LMOD [in Modules.Prelims.LModulesBinProducts]
LMOD [in Modules.Prelims.LModulesBinProducts]
LMOD_bp [in Modules.Prelims.deriveadj]
LMOD_bp [in Modules.Prelims.deriveadj]
LMOD_bp [in Modules.Prelims.deriveadj]
LMOD_bp [in Modules.Prelims.deriveadj]
M
MOD [in Modules.Signatures.SignatureDerivation]MOD [in Modules.Signatures.SignaturesColims]
MOD [in Modules.SoftEquations.SignatureOverDerivation]
MOD [in Modules.SoftEquations.SignatureOverDerivation]
MOD [in Modules.Prelims.LModulesColims]
MOD [in Modules.Signatures.SignatureBinproducts]
MOD [in Modules.Signatures.SignatureCoproduct]
MOD [in Modules.Signatures.Signature]
MOD [in Modules.SoftEquations.quotientrepslice]
MOD [in Modules.SoftEquations.quotientrepslice]
MOD [in Modules.SoftEquations.quotientrepslice]
MOD [in Modules.Signatures.EpiArePointwise]
MOD [in Modules.SoftEquations.AdjunctionEquationRep]
MOD [in Modules.SoftEquations.AdjunctionEquationRep]
MOD [in Modules.Prelims.LModulesCoproducts]
MOD [in Modules.SoftEquations.quotientequation]
MOD [in Modules.SoftEquations.SignatureOverBinproducts]
MODEL [in Modules.SoftEquations.SignatureOverDerivation]
MODEL [in Modules.SoftEquations.SignatureOverDerivation]
MODEL_CAT [in Modules.SoftEquations.CatOfTwoSignatures]
MODEL_CAT [in Modules.Signatures.ModelCat]
MODEL_MOR [in Modules.SoftEquations.SignatureOverDerivation]
MODEL_MOR [in Modules.SoftEquations.SignatureOverDerivation]
MODULE [in Modules.Prelims.LModulesFibration]
MODULE [in Modules.SoftEquations.Summary]
MOD1 [in Modules.SoftEquations.CatOfTwoSignatures]
MOD2 [in Modules.SoftEquations.CatOfTwoSignatures]
MONAD [in Modules.SoftEquations.CatOfTwoSignatures]
MONAD [in Modules.Signatures.ModelCat]
MONAD [in Modules.SoftEquations.SignatureOver]
MONAD [in Modules.SoftEquations.SignatureOverAsFiber]
MONAD [in Modules.Prelims.LModulesFibration]
MONAD [in Modules.SoftEquations.Summary]
MONAD [in Modules.Signatures.SigWithStrengthToSignature]
MONAD [in Modules.Signatures.Signature]
MONAD [in Modules.Signatures.Signature]
MONAD [in Modules.SoftEquations.quotientrepslice]
MONAD [in Modules.SoftEquations.AdjunctionEquationRep]
MONAD [in Modules.SoftEquations.AdjunctionEquationRep]
MONAD [in Modules.SoftEquations.quotientequation]
M_alg [in Modules.Signatures.HssInitialModel]
O
OSig [in Modules.SoftEquations.SignatureOver]OSIG [in Modules.SoftEquations.SignatureOverDerivation]
OSIG [in Modules.SoftEquations.SignatureOverDerivation]
P
PO [in Modules.Signatures.PresentableSignatureBinProdR]PRECAT_SIGNATURE [in Modules.SoftEquations.CatOfTwoSignatures]
PRECAT_SIGNATURE [in Modules.Signatures.Signature]
precompToFunc [in Modules.Signatures.BindingSig]
precompToSig [in Modules.Signatures.BindingSig]
precomp_functor [in Modules.Signatures.BindingSig]
PRE_MONAD [in Modules.SoftEquations.CatOfTwoSignatures]
PRE_MONAD [in Modules.SoftEquations.SignatureOver]
PRE_MONAD [in Modules.SoftEquations.SignatureOverAsFiber]
PRE_MONAD [in Modules.Signatures.SigWithStrengthToSignature]
PRE_MONAD [in Modules.Signatures.Signature]
PRE_MONAD [in Modules.Signatures.Signature]
R
REP [in Modules.SoftEquations.SignatureOver]REP [in Modules.SoftEquations.SignatureOverAsFiber]
REP [in Modules.SoftEquations.quotientrepslice]
REP [in Modules.SoftEquations.AdjunctionEquationRep]
REP [in Modules.SoftEquations.Equation]
REP [in Modules.SoftEquations.quotientequation]
REP [in Modules.Signatures.EpiSigRepresentability]
REP_CAT [in Modules.SoftEquations.SignatureOver]
REP_CAT [in Modules.SoftEquations.quotientrepslice]
REP_EQ_PRECAT [in Modules.SoftEquations.AdjunctionEquationRep]
REP_EQ [in Modules.SoftEquations.AdjunctionEquationRep]
REP_CAT [in Modules.SoftEquations.AdjunctionEquationRep]
S
SIG [in Modules.Signatures.HssSignatureCommutation]SIG [in Modules.Signatures.HssSignatureCommutation]
SIG [in Modules.Signatures.HssSignatureCommutation]
Sig [in Modules.Signatures.HssInitialModel]
SIG [in Modules.Signatures.ModelCat]
SIG [in Modules.SoftEquations.SignatureOver]
SIG [in Modules.SoftEquations.SignatureOverAsFiber]
SIG [in Modules.SoftEquations.quotientrepslice]
SIG [in Modules.Signatures.BindingSig]
Sig [in Modules.Signatures.BindingSig]
SIG [in Modules.Signatures.EpiArePointwise]
SIG [in Modules.SoftEquations.AdjunctionEquationRep]
SIG [in Modules.SoftEquations.AdjunctionEquationRep]
SIG [in Modules.Signatures.PresentableSignatureBinProdR]
Sig [in Modules.Signatures.PresentableSignature]
SIG [in Modules.SoftEquations.quotientequation]
signature [in Modules.SoftEquations.CatOfTwoSignatures]
Signature [in Modules.Signatures.SignatureDerivation]
Signature [in Modules.SoftEquations.SignatureOverDerivation]
Signature [in Modules.SoftEquations.SignatureOverDerivation]
SIGNATURE [in Modules.SoftEquations.Summary]
Signature [in Modules.Signatures.SignatureBinproducts]
Signature [in Modules.Signatures.SignatureCoproduct]
SIGNATURE [in Modules.Signatures.Signature]
signature [in Modules.Signatures.Signature]
Signature [in Modules.SoftEquations.SignatureOverBinproducts]
sumFuncs [in Modules.Signatures.BindingSig]
sumSig [in Modules.Signatures.BindingSig]
T
T [in Modules.SoftEquations.Examples.LCBetaEta]T [in Modules.Prelims.deriveadj]
T [in Modules.Prelims.deriveadj]
T [in Modules.SoftEquations.Summary]
T [in Modules.SoftEquations.quotientequation]
TFunc [in Modules.Prelims.deriveadj]
toSig [in Modules.Signatures.BindingSig]
toSig [in Modules.Signatures.PresentableSignature]
TT [in Modules.SoftEquations.Modularity]
TT [in Modules.Prelims.FibrationInitialPushout]
TT [in Modules.Signatures.Modularity]
other
Θ [in Modules.SoftEquations.CatOfTwoSignatures]Θ [in Modules.Signatures.ModelCat]
Θ [in Modules.Signatures.ModelCat]
Θ [in Modules.Prelims.deriveadj]
Θ [in Modules.Prelims.deriveadj]
Θ [in Modules.Prelims.deriveadj]
Θ [in Modules.Prelims.deriveadj]
Θ [in Modules.SoftEquations.SignatureOverAsFiber]
Θ [in Modules.SoftEquations.Summary]
Θ [in Modules.Signatures.Signature]
Θ [in Modules.Signatures.Signature]
Θ [in Modules.SoftEquations.quotientrepslice]
Θ [in Modules.SoftEquations.quotientequation]
Θ [in Modules.Signatures.quotientrep]
ΣΘ [in Modules.SoftEquations.Summary]
α' [in Modules.Signatures.SignatureCoproduct]
θ [in Modules.SoftEquations.Examples.LCBetaEta]
θ [in Modules.SoftEquations.BindingSig]
θ [in Modules.SoftEquations.quotientequation]
θ_nat_1_pw [in Modules.Signatures.SigWithStrengthToSignature]
θ_nat_2_pw [in Modules.Signatures.SigWithStrengthToSignature]
θ_nat_1_pw [in Modules.Signatures.SigWithStrengthToSignature]
θ_nat_2_pw [in Modules.Signatures.SigWithStrengthToSignature]
ι [in Modules.SoftEquations.Examples.LCBetaEta]
ι [in Modules.SoftEquations.Modularity]
ι [in Modules.SoftEquations.BindingSig]
ι [in Modules.SoftEquations.SignatureOver]
ι [in Modules.Signatures.Modularity]
ι [in Modules.SoftEquations.SignatureOverBinproducts]
ι1 [in Modules.Signatures.ModelCat]
ι2 [in Modules.Signatures.ModelCat]
π [in Modules.SoftEquations.quotientrepslice]
π [in Modules.SoftEquations.quotientequation]
π [in Modules.Signatures.quotientrep]
σ [in Modules.Prelims.deriveadj]
σ [in Modules.Prelims.deriveadj]
σ [in Modules.Prelims.LModulesBinProducts]
σ [in Modules.SoftEquations.Equation]
σ [in Modules.SoftEquations.quotientequation]
σ [in Modules.Signatures.quotientrep]
σ' [in Modules.SoftEquations.quotientequation]
τ [in Modules.SoftEquations.Examples.LCBetaEta]
τ [in Modules.SoftEquations.Equation]
τ [in Modules.SoftEquations.quotientequation]
τ' [in Modules.SoftEquations.quotientequation]
τ' [in Modules.Signatures.quotientrep]
Definition Index
A
absIdx [in Modules.SoftEquations.Examples.LCBetaEta]action_sig_over_mor [in Modules.SoftEquations.SignatureOver]
adj1 [in Modules.Prelims.deriveadj]
algebraic_sig_initial [in Modules.Signatures.BindingSig]
alg_initialR [in Modules.Signatures.BindingSig]
appIdx [in Modules.SoftEquations.Examples.LCBetaEta]
arity_abs [in Modules.SoftEquations.Examples.LCBetaEta]
arity_to_one_sigHSET [in Modules.Signatures.BindingSig]
Arity_to_SignatureHSET [in Modules.Signatures.BindingSig]
arity_to_one_sig [in Modules.Signatures.BindingSig]
B
beta_eta_equations [in Modules.SoftEquations.Examples.LCBetaEta]beta_equation [in Modules.SoftEquations.Examples.LCBetaEta]
beta_sig_source [in Modules.SoftEquations.Examples.LCBetaEta]
BinCoproducts_from_CoproductsBool [in Modules.Prelims.BinCoproductComplements]
bindingSigHSET_Initial [in Modules.SoftEquations.BindingSig]
BindingSigIndexhSet [in Modules.Signatures.BindingSig]
BindingSigIndexhSet_coprod [in Modules.Signatures.BindingSig]
bindingSig_op_to_sig_morHSET [in Modules.SoftEquations.BindingSig]
bindingSig_op_to_sig_mor [in Modules.SoftEquations.BindingSig]
binding_Sig_iso [in Modules.Signatures.BindingSig]
binding_to_one_sigHSET [in Modules.Signatures.BindingSig]
binding_to_one_sig [in Modules.Signatures.BindingSig]
BinProductWith1_iso [in Modules.Prelims.BinProductComplements]
BinProduct_pw_iso [in Modules.Prelims.BinProductComplements]
BinProduct_pw_iso_is_inverse [in Modules.Prelims.BinProductComplements]
BinProduct_pw_iso_mor [in Modules.Prelims.BinProductComplements]
BinProduct_commutative_iso [in Modules.Prelims.BinProductComplements]
BinProduct_commutative [in Modules.Prelims.BinProductComplements]
binprod_sigs_har_iso [in Modules.Signatures.HssSignatureCommutation]
binprod_pbm_to_pbm_binprod [in Modules.Prelims.LModulesBinProducts]
binprod_pbm_to_pbm_iso [in Modules.Prelims.LModulesBinProducts]
binprod_pbm [in Modules.Prelims.LModulesBinProducts]
binProd_epiSigSET [in Modules.Signatures.PreservesEpi]
bmod_disp [in Modules.Prelims.LModulesFibration]
bmod_data [in Modules.Prelims.LModulesFibration]
bmod_id_comp [in Modules.Prelims.LModulesFibration]
bmod_disp_ob_mor [in Modules.Prelims.LModulesFibration]
bp_coprod_isDistributive [in Modules.Prelims.CoproductsComplements]
bp_coprod_mor [in Modules.Prelims.CoproductsComplements]
bp_coprod_In [in Modules.Prelims.CoproductsComplements]
C
catiso_modelcat_eq [in Modules.SoftEquations.CatOfTwoSignatures]catiso_modelcat [in Modules.Signatures.ModelCat]
cleaving_bmod [in Modules.Prelims.LModulesFibration]
cocartesian_lifts_iso_commutes [in Modules.Prelims.Opfibration]
cocartesian_lifts_iso [in Modules.Prelims.Opfibration]
cocartesian_lift_is_cocartesian [in Modules.Prelims.Opfibration]
cocartesian_lift [in Modules.Prelims.Opfibration]
cocartesian_factorisation_commutes' [in Modules.Prelims.Opfibration]
cocartesian_factorisation' [in Modules.Prelims.Opfibration]
cocartesian_factorisation_unique [in Modules.Prelims.Opfibration]
cocartesian_factorisation_commutes [in Modules.Prelims.Opfibration]
cocartesian_factorisation [in Modules.Prelims.Opfibration]
commutes_binproduct_derivation [in Modules.Prelims.deriveadj]
compat_μ_projR_def [in Modules.Prelims.quotientmonad]
composite_preserves_Epi [in Modules.Prelims.EpiComplements]
cond_isEpi_hab [in Modules.Signatures.EpiSigRepresentability]
const_preserves_Epi [in Modules.Prelims.EpiComplements]
Coproducts_Unit [in Modules.Prelims.CoproductsComplements]
coprod_sigs_har_iso [in Modules.Signatures.HssSignatureCommutation]
coprod_BindingSig [in Modules.Signatures.BindingSig]
coprod_pw_iso [in Modules.Prelims.CoproductsComplements]
coprod_pw_iso_isCoproduct [in Modules.Prelims.CoproductsComplements]
coprod_pbm_to_pbm_coprod [in Modules.Prelims.LModulesCoproducts]
coprod_pbm [in Modules.Prelims.LModulesCoproducts]
coprod_isPresentable [in Modules.Signatures.PresentableSignatureCoproducts]
coprod_ρ_mor [in Modules.Signatures.PresentableSignatureCoproducts]
D
deriv_counit [in Modules.Prelims.deriveadj]deriv_counit_data [in Modules.Prelims.deriveadj]
discrete_opfibration [in Modules.Prelims.Opfibration]
disp_InitialArrow [in Modules.Prelims.FibrationInitialPushout]
disp_mor_to_total_mor [in Modules.Prelims.FibrationInitialPushout]
E
elementary_equations_on_alg_preserve_initiality [in Modules.SoftEquations.AdjunctionEquationRep]elementary_equation [in Modules.SoftEquations.quotientequation]
EpiSignatureThetaTheta [in Modules.Signatures.EpiSigRepresentability]
epis_are_pointwise [in Modules.Prelims.EpiComplements]
epi_p_mor [in Modules.Signatures.PresentableSignature]
eqrel_equivc [in Modules.Prelims.quotientmonadslice]
equation [in Modules.SoftEquations.Equation]
equivc [in Modules.Prelims.quotientmonadslice]
equivc_xy_prop [in Modules.Prelims.quotientmonadslice]
eta_equation [in Modules.SoftEquations.Examples.LCBetaEta]
F
fib_to_dir_functor_data [in Modules.SoftEquations.CatOfTwoSignatures]fib_to_dir_mor_weq [in Modules.SoftEquations.CatOfTwoSignatures]
fib_to_dir_functor [in Modules.Signatures.ModelCat]
fib_to_dir_functor_data [in Modules.Signatures.ModelCat]
fib_to_dir_mor_weq [in Modules.Signatures.ModelCat]
fib_to_dir_weq [in Modules.Signatures.ModelCat]
forget_Sig [in Modules.Signatures.Signature]
forget_Sig_is_functor [in Modules.Signatures.Signature]
forget_Sig_data [in Modules.Signatures.Signature]
forget_2model_is_right_adjoint [in Modules.SoftEquations.AdjunctionEquationRep]
forget_2model_fully_faithful [in Modules.SoftEquations.Equation]
forget_2model [in Modules.SoftEquations.Equation]
from_Coproduct_to_Coproduct [in Modules.Prelims.CoproductsComplements]
from_Coproducts_weq [in Modules.Prelims.CoproductsComplements]
H
hab [in Modules.Signatures.EpiSigRepresentability]halfeq1 [in Modules.SoftEquations.Equation]
halfeq2 [in Modules.SoftEquations.Equation]
half_beta_subst [in Modules.SoftEquations.Examples.LCBetaEta]
half_equation [in Modules.SoftEquations.Equation]
half_elem_eqs [in Modules.SoftEquations.quotientequation]
har_binprodR_isPresentable [in Modules.Signatures.PresentableSignatureBinProdR]
har_binprodR_p_mor [in Modules.Signatures.PresentableSignatureBinProdR]
har_binprodR_commute_mor_mod [in Modules.Signatures.PresentableSignatureBinProdR]
har_binprodR_p_sig [in Modules.Signatures.PresentableSignatureBinProdR]
hrel_equivc [in Modules.Prelims.quotientmonadslice]
hss_sig_initial [in Modules.Signatures.HssInitialModel]
hss_initial_arrow [in Modules.Signatures.HssInitialModel]
hss_initial_arrow_law [in Modules.Signatures.HssInitialModel]
hss_initial_arrow_mon [in Modules.Signatures.HssInitialModel]
I
id_preserves_Epi [in Modules.Prelims.EpiComplements]in_abs_halfeq [in Modules.SoftEquations.Examples.LCBetaEta]
isaprop_cocartesian_lifts [in Modules.Prelims.Opfibration]
isaset_fiber_discrete_opfibration [in Modules.Prelims.Opfibration]
isEpiBinProd [in Modules.Signatures.PresentableSignatureBinProdR]
isEpi_sig_isEpi_overSig [in Modules.SoftEquations.quotientequation]
isEpi_overSig [in Modules.SoftEquations.quotientequation]
iso_from_isDistributive [in Modules.Prelims.CoproductsComplements]
iso_from_Coproduct_to_Coproduct [in Modules.Prelims.CoproductsComplements]
isPresentable [in Modules.Signatures.PresentableSignature]
isSoft [in Modules.SoftEquations.quotientequation]
isSoft_eq [in Modules.SoftEquations.quotientequation]
is_signature_over_Mor [in Modules.SoftEquations.SignatureOver]
is_signature_over [in Modules.SoftEquations.SignatureOver]
is_signature_over [in Modules.SoftEquations.SignatureOverAsFiber]
is_discrete_opfibration [in Modules.Prelims.Opfibration]
is_opcleaving [in Modules.Prelims.Opfibration]
is_cocartesian_disp_functor [in Modules.Prelims.Opfibration]
is_cocartesian [in Modules.Prelims.Opfibration]
is_signature_Mor [in Modules.Signatures.Signature]
is_signature [in Modules.Signatures.Signature]
is_right_adjoint_functor_of_reps [in Modules.Signatures.EpiSigRepresentability]
L
LamOneSig [in Modules.SoftEquations.Examples.LCBetaEta]LamOneSigHSET [in Modules.SoftEquations.Examples.LCBetaEta]
LamOneSigHSET_Initial [in Modules.SoftEquations.Examples.LCBetaEta]
LamOneSigHSET_epiSig [in Modules.SoftEquations.Examples.LCBetaEta]
LCBetaEta [in Modules.SoftEquations.Examples.LCBetaEta]
lift_pb_LModule [in Modules.Signatures.SigWithStrengthToSignature]
lift_lmodule_mor [in Modules.Signatures.SigWithStrengthToSignature]
LModule_to_deriv_functor [in Modules.Prelims.DerivationIsFunctorial]
LModule_to_deriv [in Modules.Prelims.DerivationIsFunctorial]
LModule_to_deriv_nt [in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_functor [in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_functor_data [in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_Mor [in Modules.Prelims.DerivationIsFunctorial]
LModule_deriv_Mor_nt [in Modules.Prelims.DerivationIsFunctorial]
LModule_Lims_of_shape [in Modules.Prelims.LModulesColims]
LModule_Colims_of_shape [in Modules.Prelims.LModulesColims]
LModule_LimCone [in Modules.Prelims.LModulesColims]
LModule_ColimCocone [in Modules.Prelims.LModulesColims]
LModule_limArrow [in Modules.Prelims.LModulesColims]
LModule_colimArrow [in Modules.Prelims.LModulesColims]
LModule_limArrow_laws [in Modules.Prelims.LModulesColims]
LModule_colimArrow_laws [in Modules.Prelims.LModulesColims]
LModule_lim_cone [in Modules.Prelims.LModulesColims]
LModule_colim_cocone [in Modules.Prelims.LModulesColims]
LModule_coneOut [in Modules.Prelims.LModulesColims]
LModule_coconeIn [in Modules.Prelims.LModulesColims]
LModule_lim [in Modules.Prelims.LModulesColims]
LModule_colim [in Modules.Prelims.LModulesColims]
LModule_lim_data [in Modules.Prelims.LModulesColims]
LModule_colim_data [in Modules.Prelims.LModulesColims]
LModule_lim_mult [in Modules.Prelims.LModulesColims]
LModule_colim_mult [in Modules.Prelims.LModulesColims]
LModule_lim_mult_data [in Modules.Prelims.LModulesColims]
LModule_colim_mult_data [in Modules.Prelims.LModulesColims]
LModule_BinProducts [in Modules.Prelims.LModulesBinProducts]
LModule_ProductCone [in Modules.Prelims.LModulesBinProducts]
LModule_BinProductArrow [in Modules.Prelims.LModulesBinProducts]
LModule_BinProductArrow_laws [in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr2 [in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr1 [in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr2_nt [in Modules.Prelims.LModulesBinProducts]
LModule_binproductPr1_nt [in Modules.Prelims.LModulesBinProducts]
LModule_binproduct [in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_data [in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_mult [in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_mult_data [in Modules.Prelims.LModulesBinProducts]
LModule_binproduct_functor [in Modules.Prelims.LModulesBinProducts]
LModule_Coproducts [in Modules.Prelims.LModulesCoproducts]
LModule_Coproduct [in Modules.Prelims.LModulesCoproducts]
LModule_coproductArrow [in Modules.Prelims.LModulesCoproducts]
LModule_coproductArrow_laws [in Modules.Prelims.LModulesCoproducts]
LModule_coproductIn [in Modules.Prelims.LModulesCoproducts]
LModule_coproduct [in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_data [in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_mult [in Modules.Prelims.LModulesCoproducts]
LModule_coproduct_mult_data [in Modules.Prelims.LModulesCoproducts]
LMod_isDistributive_inv [in Modules.Signatures.PresentableSignatureBinProdR]
M
mkSignature_over_Mor [in Modules.SoftEquations.SignatureOver]mk_soft_equation [in Modules.SoftEquations.quotientequation]
model [in Modules.Signatures.Signature]
model_mor_ax [in Modules.Signatures.Signature]
model_mor_mor [in Modules.Signatures.Signature]
model_mor_law [in Modules.Signatures.Signature]
model_τ [in Modules.Signatures.Signature]
model_equations_eq [in Modules.SoftEquations.Equation]
model_equations [in Modules.SoftEquations.Equation]
mod_id_model_mor [in Modules.Signatures.ModelCat]
mod_id_model_mor_laws [in Modules.Signatures.ModelCat]
mod_id_model [in Modules.Signatures.ModelCat]
mod_id_model_action [in Modules.Signatures.ModelCat]
mod_id_model_monad [in Modules.Signatures.ModelCat]
mod_M_idM_mod_Mor [in Modules.Signatures.ModelCat]
mod_id_monad_mor [in Modules.Signatures.ModelCat]
mod_id_monad [in Modules.Signatures.ModelCat]
mod_id_monad_data [in Modules.Signatures.ModelCat]
mod_id_μ [in Modules.Signatures.ModelCat]
mod_id_M_mod [in Modules.Signatures.ModelCat]
mod_M_idM [in Modules.Signatures.ModelCat]
mod_id_η [in Modules.Signatures.ModelCat]
mod_id_nt [in Modules.Signatures.ModelCat]
mod_id_functor [in Modules.Signatures.ModelCat]
monad_mor_to_lmodule [in Modules.Prelims.LModulesComplements]
mor_disp_of_cocartesian_lift [in Modules.Prelims.Opfibration]
M_IdM_mod [in Modules.Signatures.ModelCat]
N
nat_trans_comp_pointwise' [in Modules.Prelims.lib]O
object_of_cocartesian_lift [in Modules.Prelims.Opfibration]OneMod_to_TwoMod [in Modules.SoftEquations.CatOfTwoSignatures]
OneSig_to_TwoSig [in Modules.SoftEquations.CatOfTwoSignatures]
opcleaving [in Modules.Prelims.Opfibration]
opcleaving_mor [in Modules.Prelims.Opfibration]
opcleaving_ob [in Modules.Prelims.Opfibration]
opfibration [in Modules.Prelims.Opfibration]
opfibration_from_discrete_opfibration [in Modules.Prelims.Opfibration]
opfib_two_sig [in Modules.SoftEquations.CatOfTwoSignatures]
P
pbm_binprod [in Modules.Prelims.LModulesBinProducts]pbm_coprod [in Modules.Prelims.LModulesCoproducts]
pb_modeq [in Modules.SoftEquations.CatOfTwoSignatures]
pb_rep_mor [in Modules.Signatures.ModelCat]
pb_LModule_lim_iso [in Modules.Prelims.LModulesColims]
pb_LModule_colim_iso [in Modules.Prelims.LModulesColims]
pb_rep_to_cartesian [in Modules.Signatures.Signature]
pb_rep_to [in Modules.Signatures.Signature]
pb_rep [in Modules.Signatures.Signature]
postcomp_nt [in Modules.Signatures.ModelCat]
postcomp_with_iso_disp_is_inj [in Modules.Prelims.Opfibration]
po_signature_over_mor [in Modules.SoftEquations.SignatureOver]
po_signature_over [in Modules.SoftEquations.SignatureOver]
po_signature_over_data [in Modules.SoftEquations.SignatureOver]
po_satisfies_equation [in Modules.SoftEquations.Equation]
po_equation [in Modules.SoftEquations.Equation]
precategory_model_equations [in Modules.SoftEquations.Equation]
preserveEpi_binProdFuncSET [in Modules.Prelims.EpiComplements]
preserves_Epi [in Modules.Prelims.EpiComplements]
pre_subst_nt [in Modules.Prelims.deriveadj]
pre_subst_nt_data [in Modules.Prelims.deriveadj]
products_preserves_Epis [in Modules.Prelims.EpiComplements]
projR [in Modules.Prelims.quotientmonad]
projR [in Modules.Signatures.EpiSigRepresentability]
projR_monad [in Modules.Prelims.quotientmonad]
projR_monad [in Modules.Prelims.quotientmonadslice]
projR_rep [in Modules.SoftEquations.quotientrepslice]
projR_rep [in Modules.Signatures.EpiSigRepresentability]
ptd_mor_from_Monad_mor [in Modules.Signatures.SigWithStrengthToSignature]
pushouts_from_coeq_bincoprod [in Modules.Prelims.PushoutsFromCoeqBinCoproducts]
pushout_in_big_rep [in Modules.SoftEquations.Modularity]
pushout_in_big_rep [in Modules.Signatures.Modularity]
pushout_FFpw [in Modules.Signatures.EpiArePointwise]
push_initiality [in Modules.SoftEquations.AdjunctionEquationRep]
p_mor [in Modules.Signatures.PresentableSignature]
p_alg_ar [in Modules.Signatures.PresentableSignature]
p_sig [in Modules.Signatures.PresentableSignature]
R
rep_mor_to_alg_mor [in Modules.Signatures.HssInitialModel]rep_fiber_category [in Modules.Signatures.ModelCat]
rep_fiber_precategory [in Modules.Signatures.ModelCat]
rep_fiber_precategory_data [in Modules.Signatures.ModelCat]
rep_fiber_precategory_ob_mor [in Modules.Signatures.ModelCat]
rep_fiber_comp [in Modules.Signatures.ModelCat]
rep_fiber_id [in Modules.Signatures.ModelCat]
rep_fiber_mor_ax [in Modules.Signatures.ModelCat]
rep_fiber_mor [in Modules.Signatures.ModelCat]
rep_fiber_mor_law [in Modules.Signatures.ModelCat]
rep_disp [in Modules.Signatures.Signature]
rep_data [in Modules.Signatures.Signature]
rep_id_comp [in Modules.Signatures.Signature]
rep_comp [in Modules.Signatures.Signature]
rep_id [in Modules.Signatures.Signature]
rep_disp_ob_mor [in Modules.Signatures.Signature]
rep_of_b_in_R' [in Modules.Signatures.EpiSigRepresentability]
R' [in Modules.Prelims.quotientmonad]
R' [in Modules.Signatures.EpiSigRepresentability]
R'_monad [in Modules.Prelims.quotientmonad]
R'_Monad_data [in Modules.Prelims.quotientmonad]
R'_μ [in Modules.Prelims.quotientmonad]
R'_η [in Modules.Prelims.quotientmonad]
R'_monad [in Modules.Prelims.quotientmonadslice]
R'_model [in Modules.SoftEquations.quotientrepslice]
R'_action [in Modules.SoftEquations.quotientrepslice]
R'_model_equations [in Modules.SoftEquations.quotientequation]
R'_satisfies_all_equations [in Modules.SoftEquations.quotientequation]
R'_model_τ_def [in Modules.Signatures.EpiSigRepresentability]
R'_model_τ_module [in Modules.Signatures.EpiSigRepresentability]
R'_model_τ_module [in Modules.Signatures.quotientrep]
R'_model_τ_def [in Modules.Signatures.quotientrep]
R'_model_τ [in Modules.Signatures.quotientrep]
S
satisfies_all_equations_hp [in Modules.SoftEquations.Equation]satisfies_equation_hp [in Modules.SoftEquations.Equation]
satisfies_equation_isaprop [in Modules.SoftEquations.Equation]
satisfies_equation [in Modules.SoftEquations.Equation]
sigma_coprod_iso [in Modules.Prelims.CoproductsComplements]
sigma_Coproduct [in Modules.Prelims.CoproductsComplements]
sigma_coprod_isCoproduct [in Modules.Prelims.CoproductsComplements]
sigma_coprod_In [in Modules.Prelims.CoproductsComplements]
signature [in Modules.Signatures.Signature]
signature_S1_S2_iso [in Modules.Signatures.HssSignatureCommutation]
signature_S2_S1 [in Modules.Signatures.HssSignatureCommutation]
signature_S1_S2 [in Modules.Signatures.HssSignatureCommutation]
signature_S2_S1_laws [in Modules.Signatures.HssSignatureCommutation]
signature_S1_S2_laws [in Modules.Signatures.HssSignatureCommutation]
signature_deriv_n [in Modules.Signatures.SignatureDerivation]
signature_to_deriv [in Modules.Signatures.SignatureDerivation]
signature_deriv [in Modules.Signatures.SignatureDerivation]
signature_deriv_data [in Modules.Signatures.SignatureDerivation]
signature_deriv_on_morphisms [in Modules.Signatures.SignatureDerivation]
signature_deriv_on_objects [in Modules.Signatures.SignatureDerivation]
signature_over_category [in Modules.SoftEquations.SignatureOver]
signature_over_precategory [in Modules.SoftEquations.SignatureOver]
signature_over_precategory_data [in Modules.SoftEquations.SignatureOver]
signature_over_Mor_comp [in Modules.SoftEquations.SignatureOver]
signature_over_Mor_id [in Modules.SoftEquations.SignatureOver]
signature_over_precategory_ob_mor [in Modules.SoftEquations.SignatureOver]
signature_over_Mor_ax [in Modules.SoftEquations.SignatureOver]
signature_over_Mor_data [in Modules.SoftEquations.SignatureOver]
signature_over_Mor [in Modules.SoftEquations.SignatureOver]
signature_over_comp [in Modules.SoftEquations.SignatureOver]
signature_over_id [in Modules.SoftEquations.SignatureOver]
signature_over_data_from_signature_over [in Modules.SoftEquations.SignatureOver]
signature_over [in Modules.SoftEquations.SignatureOver]
signature_over_compax [in Modules.SoftEquations.SignatureOver]
signature_over_idax [in Modules.SoftEquations.SignatureOver]
signature_over_on_morphisms_cancel_pw [in Modules.SoftEquations.SignatureOver]
signature_over_on_morphisms [in Modules.SoftEquations.SignatureOver]
signature_over_on_objects [in Modules.SoftEquations.SignatureOver]
signature_over_data [in Modules.SoftEquations.SignatureOver]
signature_over_comp [in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_id [in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_data_from_signature_over [in Modules.SoftEquations.SignatureOverAsFiber]
signature_over [in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_compax [in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_idax [in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_on_morphisms [in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_on_objects [in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_data [in Modules.SoftEquations.SignatureOverAsFiber]
signature_over_deriv_n [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_data [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_on_morphisms [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_on_objects [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_n [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_data [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_on_morphisms [in Modules.SoftEquations.SignatureOverDerivation]
signature_over_deriv_on_objects [in Modules.SoftEquations.SignatureOverDerivation]
signature_BinProducts [in Modules.Signatures.SignatureBinproducts]
signature_BinProduct [in Modules.Signatures.SignatureBinproducts]
signature_binProductArrow [in Modules.Signatures.SignatureBinproducts]
signature_binProductArrow_laws [in Modules.Signatures.SignatureBinproducts]
signature_binProductPr2 [in Modules.Signatures.SignatureBinproducts]
signature_binProductPr1 [in Modules.Signatures.SignatureBinproducts]
signature_binProd [in Modules.Signatures.SignatureBinproducts]
signature_binProd_data [in Modules.Signatures.SignatureBinproducts]
signature_BinProduct_on_morphisms [in Modules.Signatures.SignatureBinproducts]
signature_BinProduct_on_objects [in Modules.Signatures.SignatureBinproducts]
signature_Coproducts [in Modules.Signatures.SignatureCoproduct]
signature_Coproduct [in Modules.Signatures.SignatureCoproduct]
signature_coproductArrow [in Modules.Signatures.SignatureCoproduct]
signature_coproductArrow_laws [in Modules.Signatures.SignatureCoproduct]
signature_coproductIn [in Modules.Signatures.SignatureCoproduct]
signature_coprod [in Modules.Signatures.SignatureCoproduct]
signature_coprod_data [in Modules.Signatures.SignatureCoproduct]
signature_coprod_on_morphisms [in Modules.Signatures.SignatureCoproduct]
signature_coprod_on_objects [in Modules.Signatures.SignatureCoproduct]
signature_category [in Modules.Signatures.Signature]
signature_precategory [in Modules.Signatures.Signature]
signature_precategory_data [in Modules.Signatures.Signature]
signature_Mor_comp [in Modules.Signatures.Signature]
signature_Mor_id [in Modules.Signatures.Signature]
signature_precategory_ob_mor [in Modules.Signatures.Signature]
signature_Mor_ax [in Modules.Signatures.Signature]
signature_Mor_data [in Modules.Signatures.Signature]
signature_Mor [in Modules.Signatures.Signature]
signature_comp [in Modules.Signatures.Signature]
signature_id [in Modules.Signatures.Signature]
signature_data_from_signature [in Modules.Signatures.Signature]
signature_compax [in Modules.Signatures.Signature]
signature_idax [in Modules.Signatures.Signature]
signature_on_morphisms [in Modules.Signatures.Signature]
signature_on_objects [in Modules.Signatures.Signature]
signature_data [in Modules.Signatures.Signature]
signature_over_BinProducts_commutes_sig [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_BinProducts [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S1_S2_iso [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S2_S1 [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_S1_S2 [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_BinProduct [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductArrow [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductArrow_laws [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductPr2 [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProductPr1 [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProd [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_binProd_data [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_BinProduct_on_morphisms [in Modules.SoftEquations.SignatureOverBinproducts]
signature_over_BinProduct_on_objects [in Modules.SoftEquations.SignatureOverBinproducts]
sigWithStrength_to_sig_functor [in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_functor_data [in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_mor [in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_mod_mor [in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig [in Modules.Signatures.SigWithStrengthToSignature]
sigWithStrength_to_sig_data [in Modules.Signatures.SigWithStrengthToSignature]
Sig_Lims_of_shape [in Modules.Signatures.SignaturesColims]
Sig_Colims_of_shape [in Modules.Signatures.SignaturesColims]
Sig_LimCone [in Modules.Signatures.SignaturesColims]
Sig_ColimCocone [in Modules.Signatures.SignaturesColims]
Sig_limArrow [in Modules.Signatures.SignaturesColims]
Sig_colimArrow [in Modules.Signatures.SignaturesColims]
Sig_lim_cone [in Modules.Signatures.SignaturesColims]
Sig_colim_cocone [in Modules.Signatures.SignaturesColims]
Sig_coneOut [in Modules.Signatures.SignaturesColims]
Sig_coconeIn [in Modules.Signatures.SignaturesColims]
Sig_lim [in Modules.Signatures.SignaturesColims]
Sig_colim [in Modules.Signatures.SignaturesColims]
Sig_lim_signature_data [in Modules.Signatures.SignaturesColims]
Sig_colim_signature_data [in Modules.Signatures.SignaturesColims]
Sig_lim_on_mor [in Modules.Signatures.SignaturesColims]
Sig_colim_on_mor [in Modules.Signatures.SignaturesColims]
sig_to_sig_over_functor [in Modules.SoftEquations.SignatureOver]
sig_sig_over_mor [in Modules.SoftEquations.SignatureOver]
sig_over_data_from_sig [in Modules.SoftEquations.SignatureOver]
sig_preservesNatEpiMonad_pw [in Modules.Signatures.PreservesEpi]
sig_preservesNatEpiMonad [in Modules.Signatures.PreservesEpi]
Sig_isDistributive_inv [in Modules.Signatures.PresentableSignatureBinProdR]
soft_equation_choice [in Modules.SoftEquations.quotientequation]
soft_equation_isEpi [in Modules.SoftEquations.quotientequation]
soft_equation_isSoft [in Modules.SoftEquations.quotientequation]
soft_equation [in Modules.SoftEquations.quotientequation]
source_abs_iso [in Modules.SoftEquations.Examples.LCBetaEta]
source_equation [in Modules.SoftEquations.Equation]
source_elem_epiSig [in Modules.SoftEquations.quotientequation]
source_elem_eq [in Modules.SoftEquations.quotientequation]
substitution [in Modules.Prelims.deriveadj]
substitution_nat_trans [in Modules.Prelims.deriveadj]
substitution_nt [in Modules.Prelims.deriveadj]
T
target_equation [in Modules.SoftEquations.Equation]target_elem_eq [in Modules.SoftEquations.quotientequation]
tautological_signature_over [in Modules.SoftEquations.SignatureOver]
tautological_signature_over [in Modules.SoftEquations.SignatureOverAsFiber]
tautological_signature_over_data [in Modules.SoftEquations.SignatureOverAsFiber]
tautological_signature_over_on_morphisms [in Modules.SoftEquations.SignatureOverAsFiber]
tautological_signature_over_on_objects [in Modules.SoftEquations.SignatureOverAsFiber]
tautological_signature [in Modules.Signatures.Signature]
tautological_signature_data [in Modules.Signatures.Signature]
tautological_signature_on_morphisms [in Modules.Signatures.Signature]
tautological_signature_on_objects [in Modules.Signatures.Signature]
tautological_epiSig [in Modules.Signatures.PreservesEpi]
tauto_sigs_har_iso [in Modules.Signatures.HssSignatureCommutation]
TerminalSignature [in Modules.Signatures.PresentableSignatureBinProdR]
Terminal_EndC_constant_terminal [in Modules.Prelims.deriveadj]
toR' [in Modules.Prelims.deriveadj]
toR'_MOD [in Modules.Prelims.deriveadj]
TwoMod_To_One_right_adjoint [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_PushoutsSET [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_CoproductsSET [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_CoequalizersSET [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_To_One_right_adjoint [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_eqs [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_index [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_Mor [in Modules.SoftEquations.CatOfTwoSignatures]
TwoSignature_category [in Modules.SoftEquations.CatOfTwoSignatures]
Two_to_OneMod_functor [in Modules.SoftEquations.CatOfTwoSignatures]
Two_to_OneMod_is_functor [in Modules.SoftEquations.CatOfTwoSignatures]
Two_to_OneMod_functor_data [in Modules.SoftEquations.CatOfTwoSignatures]
two_model_disp [in Modules.SoftEquations.CatOfTwoSignatures]
two_mod_data [in Modules.SoftEquations.CatOfTwoSignatures]
two_model_disp_ob_mor [in Modules.SoftEquations.CatOfTwoSignatures]
two_model [in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_coproduct_in [in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_coproduct [in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_disp [in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_data [in Modules.SoftEquations.CatOfTwoSignatures]
two_signature_disp_ob_mor [in Modules.SoftEquations.CatOfTwoSignatures]
U
u [in Modules.Prelims.quotientmonad]u [in Modules.Prelims.quotientmonadslice]
u [in Modules.Signatures.EpiSigRepresentability]
unique_lift_op [in Modules.Prelims.Opfibration]
univalent_opfibration_is_cloven [in Modules.Prelims.Opfibration]
univ_surj_pb_lmod_nt_epi [in Modules.SoftEquations.quotientrepslice]
univ_surj_lmod_nt_epi [in Modules.SoftEquations.quotientrepslice]
u_monad [in Modules.Prelims.quotientmonad]
u_monad [in Modules.Prelims.quotientmonadslice]
u_rep [in Modules.SoftEquations.quotientrepslice]
u_rep_arrow [in Modules.SoftEquations.AdjunctionEquationRep]
u_rep [in Modules.Signatures.EpiSigRepresentability]
W
weak_opfibration [in Modules.Prelims.Opfibration]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1380 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (68 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (137 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (51 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (311 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (77 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (241 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (495 entries) |
This page has been generated by coqdoc