Safe Haskell	None

MAlonzo.Code.Function.HalfAdjointEquivalence

Documentation

d__'8771'__12 :: p1 -> p2 -> p3 -> p4 -> () Source #

data T__'8771'__12 Source #

Constructors

C__'8771'_'46'constructor_541 (AgdaAny -> AgdaAny) (AgdaAny -> AgdaAny)

d_to_38 :: T__'8771'__12 -> AgdaAny -> AgdaAny Source #

d_from_40 :: T__'8771'__12 -> AgdaAny -> AgdaAny Source #

d_left'45'inverse'45'of_44 :: T__'8771'__12 -> AgdaAny -> T__'8801'__12 Source #

d_right'45'inverse'45'of_48 :: T__'8771'__12 -> AgdaAny -> T__'8801'__12 Source #

d_left'45'right_52 :: T__'8771'__12 -> AgdaAny -> T__'8801'__12 Source #

d_inverse_54 :: T_Level_14 -> T_Level_14 -> () -> () -> T__'8771'__12 -> T_Inverse_58 Source #

du_inverse_54 :: T__'8771'__12 -> T_Inverse_58 Source #

d_injective_60 :: T_Level_14 -> T_Level_14 -> () -> () -> T__'8771'__12 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12 Source #

d_'8596''8594''8771'_80 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Inverse_58 -> T__'8771'__12 Source #

du_'8596''8594''8771'_80 :: T_Inverse_58 -> T__'8771'__12 Source #

d_right'45'inverse'45'of_122 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Inverse_58 -> AgdaAny -> T__'8801'__12 Source #

d_left'45'right_132 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Inverse_58 -> AgdaAny -> T__'8801'__12 Source #

d_lemma_140 :: T_Level_14 -> T_Level_14 -> () -> () -> T_Inverse_58 -> AgdaAny -> T__'8801'__12 Source #