| Safe Haskell | None |
|---|
MAlonzo.Code.Function.Consequences
Documentation
d_inverse'737''8658'surjective_36 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 Source #
du_inverse'737''8658'surjective_36 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 Source #
d_inverse'691''8658'surjective_42 :: T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 Source #
du_inverse'691''8658'surjective_42 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14 Source #
d__'8776'__68 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Setoid_44 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> () Source #
d_inverse'691''8658'injective_74 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Setoid_44 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_inverse'691''8658'injective_74 :: T_Setoid_44 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_inverse'7495''8658'bijective_122 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_Level_14 -> T_Setoid_44 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14 Source #