Safe Haskell	Safe-Inferred
Language	Haskell2010

MAlonzo.Code.Algebra.Consequences.Setoid

Documentation

d__Absorbs__38 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver__40 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'691'__42 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__DistributesOver'737'__44 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d__MiddleFourExchange__48 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_AlmostLeftCancellative_54 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_AlmostRightCancellative_56 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Associative_60 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Commutative_64 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Congruent'8322'_68 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Identity_80 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Inverse_84 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_Involutive_88 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny) → () Source #

d_LeftCancellative_94 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftIdentity_106 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftInverse_108 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_LeftZero_114 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightCancellative_124 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightIdentity_136 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightInverse_138 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_RightZero_144 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_SelfInverse_148 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny) → () Source #

d_Zero_164 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #

d_'8729''45'cong'691'_214 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_214 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_216 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_216 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_228 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_228 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_230 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_230 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm'8743'assoc'8658'middleFour_232 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_232 ∷ T_Setoid_46 → (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_248 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_248 ∷ T_Setoid_46 → (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_268 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_268 ∷ T_Setoid_46 → (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_292 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_selfInverse'8658'involutive_292 ∷ T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_selfInverse'8658'congruent_294 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_selfInverse'8658'congruent_294 ∷ T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_selfInverse'8658'inverse'7495'_302 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_selfInverse'8658'inverse'7495'_302 ∷ T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_selfInverse'8658'surjective_304 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 Source #

du_selfInverse'8658'surjective_304 ∷ T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → T_Σ_14 Source #

d_selfInverse'8658'injective_308 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_selfInverse'8658'injective_308 ∷ T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_selfInverse'8658'bijective_316 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

du_selfInverse'8658'bijective_316 ∷ T_Setoid_46 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 Source #

d_comm'8743'cancel'737''8658'cancel'691'_326 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_326 ∷ T_Setoid_46 → (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'_338 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_338 ∷ T_Setoid_46 → (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'_360 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'8743'id'737''8658'id'691'_360 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'8743'id'691''8658'id'737'_366 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'8743'id'691''8658'id'737'_366 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'8743'id'737''8658'id_372 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #

du_comm'8743'id'737''8658'id_372 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #

d_comm'8743'id'691''8658'id_376 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #

du_comm'8743'id'691''8658'id_376 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #

d_comm'8743'ze'737''8658'ze'691'_380 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'8743'ze'737''8658'ze'691'_380 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'8743'ze'691''8658'ze'737'_386 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'8743'ze'691''8658'ze'737'_386 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'8743'ze'737''8658'ze_392 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #

du_comm'8743'ze'737''8658'ze_392 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #

d_comm'8743'ze'691''8658'ze_396 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #

du_comm'8743'ze'691''8658'ze_396 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #

d_comm'8743'almostCancel'737''8658'almostCancel'691'_400 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_400 ∷ T_Setoid_46 → (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'_414 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_414 ∷ T_Setoid_46 → (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'_440 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'8743'inv'737''8658'inv'691'_440 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'8743'inv'737''8658'inv_446 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #

du_comm'8743'inv'737''8658'inv_446 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #

d_comm'8743'inv'691''8658'inv'737'_450 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'8743'inv'691''8658'inv'737'_450 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'8743'inv'691''8658'inv_456 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #

du_comm'8743'inv'691''8658'inv_456 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #

d_'8729''45'cong'691'_474 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_474 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_476 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_476 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_assoc'8743'id'8743'inv'691''8658'inv'737''45'unique_482 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_482 ∷ T_Setoid_46 → (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_502 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_502 ∷ T_Setoid_46 → (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_'8729''45'cong'691'_532 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'691'_532 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_534 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_'8729''45'cong'737'_534 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_comm'8743'distr'737''8658'distr'691'_536 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_536 ∷ T_Setoid_46 → (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'_546 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_546 ∷ T_Setoid_46 → (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_556 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_556 ∷ T_Setoid_46 → (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_560 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_560 ∷ T_Setoid_46 → (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'_570 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_570 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_596 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_'8729''45'cong'691'_596 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_598 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_'8729''45'cong'737'_598 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_distrib'8743'absorbs'8658'distrib'737'_600 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_600 ∷ T_Setoid_46 → (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_'8729''45'cong'691'_634 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_'8729''45'cong'691'_634 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_636 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_'8729''45'cong'737'_636 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'691'_640 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_'8729''45'cong'691'_640 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_'8729''45'cong'737'_642 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_'8729''45'cong'737'_642 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_subst'8743'comm'8658'sym_686 ∷ T_Setoid_46 → 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_686 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

d_wlog_700 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → 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_700 ∷ (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_704 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_704 ∷ T_Setoid_46 → (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_706 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_706 ∷ T_Setoid_46 → (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_708 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_708 ∷ T_Setoid_46 → (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'_710 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_710 ∷ T_Setoid_46 → (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'_712 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_712 ∷ T_Setoid_46 → (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'_714 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'id'737''8658'id'691'_714 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'id'691''8658'id'737'_716 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'id'691''8658'id'737'_716 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'ze'737''8658'ze'691'_718 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'ze'737''8658'ze'691'_718 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'ze'691''8658'ze'737'_720 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'ze'691''8658'ze'737'_720 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'almostCancel'737''8658'almostCancel'691'_722 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_722 ∷ T_Setoid_46 → (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'_724 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_724 ∷ T_Setoid_46 → (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'_726 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'inv'737''8658'inv'691'_726 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'inv'691''8658'inv'737'_728 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

du_comm'43'inv'691''8658'inv'737'_728 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #

d_comm'43'inv'737''8658'inv_730 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #

du_comm'43'inv'737''8658'inv_730 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #

d_comm'43'inv'691''8658'inv_732 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #

du_comm'43'inv'691''8658'inv_732 ∷ T_Setoid_46 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 Source #

d_comm'43'distr'737''8658'distr'691'_734 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_734 ∷ T_Setoid_46 → (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'_736 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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'_736 ∷ T_Setoid_46 → (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_742 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_742 ∷ T_Setoid_46 → (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_744 ∷ T_Level_18 → T_Level_18 → T_Setoid_46 → (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_744 ∷ T_Setoid_46 → (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_subst'43'comm'8658'sym_746 ∷ T_Setoid_46 → T_Level_18 → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #

du_subst'43'comm'8658'sym_746 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #