| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Consequences.Setoid
Documentation
d__Absorbs__36 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver__38 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'691'__40 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__DistributesOver'737'__42 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__MiddleFourExchange__46 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_AlmostLeftCancellative_52 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_AlmostRightCancellative_54 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Associative_58 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Commutative_62 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Congruent'8322'_66 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Identity_78 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Inverse_82 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Involutive_86 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → () Source #
d_LeftCancellative_92 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftIdentity_104 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftInverse_106 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftZero_112 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightCancellative_122 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightIdentity_134 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightInverse_136 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightZero_142 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_SelfInverse_146 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → () Source #
d_Zero_162 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_comm'8743'assoc'8658'middleFour_212 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'8743'assoc'8658'middleFour_212 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_identity'8743'middleFour'8658'assoc_228 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_identity'8743'middleFour'8658'assoc_228 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_identity'8743'middleFour'8658'comm_248 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_identity'8743'middleFour'8658'comm_248 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_selfInverse'8658'involutive_272 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_selfInverse'8658'involutive_272 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_selfInverse'8658'congruent_274 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_selfInverse'8658'congruent_274 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_selfInverse'8658'inverse'7495'_282 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
du_selfInverse'8658'inverse'7495'_282 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_selfInverse'8658'surjective_284 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 Source #
du_selfInverse'8658'surjective_284 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 Source #
d_selfInverse'8658'injective_288 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_selfInverse'8658'injective_288 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_selfInverse'8658'bijective_296 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
du_selfInverse'8658'bijective_296 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'8743'cancel'737''8658'cancel'691'_306 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'8743'cancel'737''8658'cancel'691'_306 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'8743'cancel'691''8658'cancel'737'_318 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'8743'cancel'691''8658'cancel'737'_318 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'8743'id'737''8658'id'691'_340 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'8743'id'737''8658'id'691'_340 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'8743'id'691''8658'id'737'_346 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'8743'id'691''8658'id'737'_346 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'8743'id'737''8658'id_352 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'8743'id'737''8658'id_352 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'8743'id'691''8658'id_356 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'8743'id'691''8658'id_356 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'8743'ze'737''8658'ze'691'_360 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'8743'ze'737''8658'ze'691'_360 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'8743'ze'691''8658'ze'737'_366 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'8743'ze'691''8658'ze'737'_366 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'8743'ze'737''8658'ze_372 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'8743'ze'737''8658'ze_372 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'8743'ze'691''8658'ze_376 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'8743'ze'691''8658'ze_376 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'8743'almostCancel'737''8658'almostCancel'691'_380 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny Source #
du_comm'8743'almostCancel'737''8658'almostCancel'691'_380 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny Source #
d_comm'8743'almostCancel'691''8658'almostCancel'737'_394 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny Source #
du_comm'8743'almostCancel'691''8658'almostCancel'737'_394 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny Source #
d_comm'8743'inv'737''8658'inv'691'_420 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'8743'inv'737''8658'inv'691'_420 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'8743'inv'737''8658'inv_426 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'8743'inv'737''8658'inv_426 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'8743'inv'691''8658'inv'737'_430 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'8743'inv'691''8658'inv'737'_430 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'8743'inv'691''8658'inv_436 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'8743'inv'691''8658'inv_436 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_assoc'8743'id'8743'inv'691''8658'inv'737''45'unique_456 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_assoc'8743'id'8743'inv'691''8658'inv'737''45'unique_456 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc'8743'id'8743'inv'737''8658'inv'691''45'unique_476 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_assoc'8743'id'8743'inv'737''8658'inv'691''45'unique_476 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'8743'distr'737''8658'distr'691'_504 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'8743'distr'737''8658'distr'691'_504 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'8743'distr'691''8658'distr'737'_514 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'8743'distr'691''8658'distr'737'_514 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'8743'distr'737''8658'distr_524 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'8743'distr'737''8658'distr_524 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'8743'distr'691''8658'distr_528 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'8743'distr'691''8658'distr_528 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'8658'sym'91'distrib'737''93'_538 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'8658'sym'91'distrib'737''93'_538 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_distrib'8743'absorbs'8658'distrib'737'_562 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_distrib'8743'absorbs'8658'distrib'737'_562 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc'8743'distrib'691''8743'id'691''8743'inv'691''8658'ze'737'_594 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_assoc'8743'distrib'691''8743'id'691''8743'inv'691''8658'ze'737'_594 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_assoc'8743'distrib'737''8743'id'691''8743'inv'691''8658'ze'691'_606 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_assoc'8743'distrib'737''8743'id'691''8743'inv'691''8658'ze'691'_606 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_subst'8743'comm'8658'sym_636 ∷ T_Setoid_44 → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_subst'8743'comm'8658'sym_636 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_wlog_650 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_wlog_650 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'43'assoc'8658'middleFour_654 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'43'assoc'8658'middleFour_654 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_identity'43'middleFour'8658'assoc_656 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_identity'43'middleFour'8658'assoc_656 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_identity'43'middleFour'8658'comm_658 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_identity'43'middleFour'8658'comm_658 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'43'cancel'737''8658'cancel'691'_660 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'43'cancel'737''8658'cancel'691'_660 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'43'cancel'691''8658'cancel'737'_662 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'43'cancel'691''8658'cancel'737'_662 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'43'id'737''8658'id'691'_664 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'43'id'737''8658'id'691'_664 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'43'id'691''8658'id'737'_666 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'43'id'691''8658'id'737'_666 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'43'ze'737''8658'ze'691'_668 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'43'ze'737''8658'ze'691'_668 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'43'ze'691''8658'ze'737'_670 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'43'ze'691''8658'ze'737'_670 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'43'almostCancel'737''8658'almostCancel'691'_672 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny Source #
du_comm'43'almostCancel'737''8658'almostCancel'691'_672 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny Source #
d_comm'43'almostCancel'691''8658'almostCancel'737'_674 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny Source #
du_comm'43'almostCancel'691''8658'almostCancel'737'_674 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny Source #
d_comm'43'inv'737''8658'inv'691'_676 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'43'inv'737''8658'inv'691'_676 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'43'inv'691''8658'inv'737'_678 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_comm'43'inv'691''8658'inv'737'_678 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_comm'43'inv'737''8658'inv_680 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'43'inv'737''8658'inv_680 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'43'inv'691''8658'inv_682 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_comm'43'inv'691''8658'inv_682 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_comm'43'distr'737''8658'distr'691'_684 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'43'distr'737''8658'distr'691'_684 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_comm'43'distr'691''8658'distr'737'_686 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_comm'43'distr'691''8658'distr'737'_686 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc'43'distrib'691''43'id'691''43'inv'691''8658'ze'737'_688 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_assoc'43'distrib'691''43'id'691''43'inv'691''8658'ze'737'_688 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_assoc'43'distrib'737''43'id'691''43'inv'691''8658'ze'691'_690 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_assoc'43'distrib'737''43'id'691''43'inv'691''8658'ze'691'_690 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_assoc'43'id'43'inv'691''8658'inv'737''45'unique_692 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_assoc'43'id'43'inv'691''8658'inv'737''45'unique_692 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc'43'id'43'inv'737''8658'inv'691''45'unique_694 ∷ T_Level_18 → T_Level_18 → T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_assoc'43'id'43'inv'737''8658'inv'691''45'unique_694 ∷ T_Setoid_44 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #