Documentation

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

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

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

data T_LeftInverse_82 Source #

d_to_102 :: T_LeftInverse_82 -> T_Π_16 Source #

d_from_104 :: T_LeftInverse_82 -> T_Π_16 Source #

d_left'45'inverse'45'of_106 :: T_LeftInverse_82 -> AgdaAny -> AgdaAny Source #

d__'8776'__110 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> () Source #

d__'8776'__132 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> () Source #

d_injective_176 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_injective_176 :: T_Setoid_44 -> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_injection_184 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88 Source #

du_injection_184 :: T_Setoid_44 -> T_LeftInverse_82 -> T_Injection_88 Source #

d_equivalence_186 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_82 -> T_Equivalence_16 Source #

du_equivalence_186 :: T_LeftInverse_82 -> T_Equivalence_16 Source #

d_to'45'from_192 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_to'45'from_192 :: T_Setoid_44 -> T_Setoid_44 -> T_LeftInverse_82 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_RightInverse_212 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_Setoid_44 -> () Source #

d__'8606'__222 :: T_Level_14 -> T_Level_14 -> () -> () -> () Source #

d_leftInverse_242 :: T_Level_14 -> T_Level_14 -> () -> () -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T_LeftInverse_82 Source #

du_leftInverse_242 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> (AgdaAny -> T__'8801'__12) -> T_LeftInverse_82 Source #

d_id_256 :: T_Level_14 -> T_Level_14 -> T_Setoid_44 -> T_LeftInverse_82 Source #

du_id_256 :: T_Setoid_44 -> T_LeftInverse_82 Source #

d__'8728'__280 :: 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_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82 Source #

du__'8728'__280 :: T_Setoid_44 -> T_LeftInverse_82 -> T_LeftInverse_82 -> T_LeftInverse_82 Source #