| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality
Documentation
d__'8776''8729'__20 :: p -> p -> p -> p -> p -> p -> () #
data T__'8776''8729'__20 #
Constructors
| C_'8729''8776''8729'_22 | |
| C_'91'_'93'_28 AgdaAny |
d_'91''8776''93''45'injective_34 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> T__'8776''8729'__20 -> AgdaAny #
d_'8776''8729''45'refl_38 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20 #
du_'8776''8729''45'refl_38 :: (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> T__'8776''8729'__20 #
d_'8776''8729''45'sym_46 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'8776''8729'__20 #
du_'8776''8729''45'sym_46 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'8776''8729'__20 #
d_'8776''8729''45'trans_54 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'8776''8729'__20 -> T__'8776''8729'__20 #
du_'8776''8729''45'trans_54 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'8776''8729'__20 -> T__'8776''8729'__20 #
d_'8776''8729''45'dec_66 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20 #
du_'8776''8729''45'dec_66 :: (AgdaAny -> AgdaAny -> T_Dec_20) -> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20 #
d_'8776''8729''45'irrelevant_84 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> T__'8776''8729'__20 -> T__'8801'__12 #
d_'8776''8729''45'substitutive_96 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> ((AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (Maybe AgdaAny -> ()) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> AgdaAny -> AgdaAny #
du_'8776''8729''45'substitutive_96 :: ((AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (Maybe AgdaAny -> ()) -> Maybe AgdaAny -> Maybe AgdaAny -> T__'8776''8729'__20 -> AgdaAny -> AgdaAny #
d_'8776''8729''45'isEquivalence_108 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsEquivalence_26 #
d_'8776''8729''45'isDecEquivalence_128 :: T_Level_18 -> T_Level_18 -> () -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 #