Safe Haskell	None

MAlonzo.Code.Function.Injection

Documentation

d_Injective_16 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Π_16 -> () Source #

d_Injection_88 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> () Source #

data T_Injection_88 Source #

Constructors

C_Injection'46'constructor_2269 T_Π_16 (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)

d_to_106 :: T_Injection_88 -> T_Π_16 Source #

d_injective_108 :: T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'10216''36''10217'__112 :: T_Injection_88 -> AgdaAny -> AgdaAny Source #

d_cong_114 :: T_Injection_88 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8611'__120 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d_injection_140 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_Injection_88 Source #

du_injection_140 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12) -> T_Injection_88 Source #

d_id_152 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Injection_88 Source #

du_id_152 :: T_Injection_88 Source #

d__'8728'__172 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_Setoid_44 -> T_Injection_88 -> T_Injection_88 -> T_Injection_88 Source #

du__'8728'__172 :: T_Injection_88 -> T_Injection_88 -> T_Injection_88 Source #