| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Function.Properties.Inverse.HalfAdjointEquivalence
Documentation
d__'8771'__24 :: p -> p -> p -> p -> () #
data T__'8771'__24 #
Constructors
| C__'8771'_'46'constructor_973 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny) |
d_to_46 :: T__'8771'__24 -> AgdaAny -> AgdaAny #
d_from_48 :: T__'8771'__24 -> AgdaAny -> AgdaAny #
d_left'45'right_60 :: T__'8771'__24 -> AgdaAny -> T__'8801'__12 #
d_injective_66 :: T_Level_18 -> T_Level_18 -> () -> () -> T__'8771'__24 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_'8771''8658''8596'_78 :: T_Level_18 -> () -> T_Level_18 -> () -> T__'8771'__24 -> T_Inverse_1960 #
d_from_88 :: T__'8771'__24 -> AgdaAny -> AgdaAny #
d_injective_90 :: T_Level_18 -> () -> T_Level_18 -> () -> T__'8771'__24 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 #
d_left'45'right_94 :: T__'8771'__24 -> AgdaAny -> T__'8801'__12 #
d_to_98 :: T__'8771'__24 -> AgdaAny -> AgdaAny #
d_'8596''8658''8771'_100 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> T__'8771'__24 #
d_strictlyInverse'691'_130 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> AgdaAny -> T__'8801'__12 #
d_right'45'inverse'45'of_188 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> AgdaAny -> T__'8801'__12 #
d_left'45'right_194 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> AgdaAny -> T__'8801'__12 #
d_lemma_202 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Inverse_1960 -> AgdaAny -> T__'8801'__12 #