| Safe Haskell | None |
|---|
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
Documentation
d_J_34 :: T_Level_14 -> T_Level_14 -> () -> AgdaAny -> (AgdaAny -> T__'8801'__12 -> ()) -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny Source #
d_dcong_54 :: T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #
d_dcong'8322'_78 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> () -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 Source #
d_dsubst'8322'_100 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> AgdaAny -> AgdaAny Source #
du_dsubst'8322'_100 :: AgdaAny -> AgdaAny Source #
d_ddcong'8322'_132 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (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_14 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #
d_trans'45'assoc_158 :: T_Level_14 -> () -> 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_14 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #
d_trans'45'sym'691'_174 :: T_Level_14 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #
d_trans'45'injective'737'_188 :: T_Level_14 -> () -> 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_14 -> () -> 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_14 -> () -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #
d_cong'45''8728'_224 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 Source #
d_sym'45'cong_234 :: T_Level_14 -> () -> T_Level_14 -> () -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 Source #
d_trans'45'cong_248 :: T_Level_14 -> () -> T_Level_14 -> () -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 -> T__'8801'__12 Source #
d_cong'8322''45'refl'737'_262 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #
d_cong'8322''45'refl'691'_276 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #
d_subst'45'injective_298 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #
d_subst'45'subst_310 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 -> AgdaAny -> T__'8801'__12 Source #
d_subst'45'subst'45'sym_316 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> T__'8801'__12 Source #
d_subst'45'sym'45'subst_322 :: T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> T__'8801'__12 Source #
d_subst'45''8728'_336 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> AgdaAny -> AgdaAny -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> T__'8801'__12 -> AgdaAny -> T__'8801'__12 Source #
d_subst'45'application'8242'_362 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 Source #
d_subst'45'application_394 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> T__'8801'__12 -> T__'8801'__12 Source #
d_isEquivalence_396 :: T_Level_14 -> () -> T_IsEquivalence_26 Source #
d_isDecEquivalence_398 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44 Source #
du_isDecEquivalence_398 :: (AgdaAny -> AgdaAny -> T_Dec_32) -> T_IsDecEquivalence_44 Source #
d_isPreorder_402 :: T_Level_14 -> () -> T_IsPreorder_70 Source #
d_setoid_404 :: T_Level_14 -> () -> T_Setoid_44 Source #
d_decSetoid_408 :: T_Level_14 -> () -> (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecSetoid_84 Source #
du_decSetoid_408 :: (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecSetoid_84 Source #
d_preorder_412 :: T_Level_14 -> () -> T_Preorder_132 Source #