| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.PropositionalEquality
Documentation
d__'8594''45'setoid__26 ∷ T_Level_18 → T_Level_18 → () → () → T_Setoid_44 Source #
d__'8791'__36 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → () Source #
d_'58''8594''45'to'45'Π_48 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_IndexedSetoid_18 → (AgdaAny → AgdaAny) → T_Π_16 Source #
d_'46'extendedlambda0_62 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_IndexedSetoid_18 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8801'__12 → AgdaAny Source #
d_'8594''45'to'45''10230'_68 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_Setoid_44 → (AgdaAny → AgdaAny) → T_Π_16 Source #
d_Reveal_'183'_is__86 ∷ p → p → p → p → p → p → p → () Source #
data T_Reveal_'183'_is__86 Source #
Constructors
| C_'91'_'93'_102 |
d_inspect_114 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → T_Reveal_'183'_is__86 Source #
d_isPropositional_120 ∷ T_Level_18 → () → () Source #
d_naturality_142 ∷ T_Level_18 → () → T_Level_18 → () → AgdaAny → AgdaAny → T__'8801'__12 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_cong'45''8801'id_160 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_fx'8801'x_172 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_f'178'x'8801'x_174 ∷ T_Level_18 → () → (AgdaAny → AgdaAny) → AgdaAny → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_'8801''45''8799''45'identity_194 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T__'8801'__12 → T__'8801'__12 Source #
d_'8802''45''8799''45'identity_200 ∷ T_Level_18 → () → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → (T__'8801'__12 → T_'8869'_4) → T_Σ_14 Source #
du_'8802''45''8799''45'identity_200 ∷ (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Σ_14 Source #
d_Extensionality_204 ∷ T_Level_18 → T_Level_18 → () Source #
d_extensionality'45'for'45'lower'45'levels_206 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → (() → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → () → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #
d_'8704''45'extensionality_208 ∷ T_Level_18 → T_Level_18 → (() → (AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → T__'8801'__12) → T__'8801'__12) → () → (AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → T__'8801'__12) → T__'8801'__12 Source #