| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
Documentation
d_J_34 ∷ T_Level_18 → T_Level_18 → () → AgdaAny → (AgdaAny → T__'8801'__12 → ()) → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny Source #
d_dcong_54 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_dcong'8322'_78 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_dsubst'8322'_100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → AgdaAny → AgdaAny Source #
d_ddcong'8322'_132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'refl'691'_142 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'assoc_158 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'sym'737'_166 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'sym'691'_174 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'injective'737'_188 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'injective'691'_202 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_cong'45'id_212 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_cong'45''8728'_224 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 Source #
d_sym'45'cong_234 ∷ T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 Source #
d_trans'45'cong_248 ∷ T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_cong'8322''45'refl'737'_262 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_cong'8322''45'refl'691'_276 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_subst'45'injective_298 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_subst'45'subst_310 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_subst'45'subst'45'sym_316 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_subst'45'sym'45'subst_322 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_subst'45''8728'_336 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → AgdaAny → AgdaAny → (AgdaAny → ()) → (AgdaAny → AgdaAny) → T__'8801'__12 → AgdaAny → T__'8801'__12 Source #
d_subst'45'application'8242'_362 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 Source #
d_subst'45'application_394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → T__'8801'__12 → T__'8801'__12 Source #
d_isDecEquivalence_398 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecEquivalence_48 Source #
d_setoid_402 ∷ T_Level_18 → () → T_Setoid_46 Source #
d_decSetoid_406 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_20) → T_DecSetoid_90 Source #
du_decSetoid_406 ∷ (AgdaAny → AgdaAny → T_Dec_20) → T_DecSetoid_90 Source #
d_isPreorder_410 ∷ T_Level_18 → () → T_IsPreorder_76 Source #
d_preorder_414 ∷ T_Level_18 → () → T_Preorder_142 Source #
d_poset_418 ∷ T_Level_18 → () → T_Poset_492 Source #
d_begin__430 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_step'45''8801'_434 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_step'45''8801''45''8739'_436 ∷ T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_step'45''8801''45''10216'_438 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_step'45''8801''45''10217'_440 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d_step'45''8801''728'_442 ∷ T_Level_18 → () → AgdaAny → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 → T__'8801'__12 Source #
d__'8718'_446 ∷ T_Level_18 → () → AgdaAny → T__'8801'__12 Source #