Safe Haskell	None

MAlonzo.Code.Relation.Binary.Construct.Subst.Equality

Documentation

d_refl_28 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

du_refl_28 :: T_Σ_14 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #

d_sym_32 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sym_32 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_trans_36 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_trans_36 :: T_Σ_14 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_isEquivalence_44 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_IsEquivalence_26 -> T_IsEquivalence_26 Source #

du_isEquivalence_44 :: T_Σ_14 -> T_IsEquivalence_26 -> T_IsEquivalence_26 Source #