Trait identity::Identity

pub trait Identity<A: ?Sized, B: ?Sized>: Sized {
    type Inverse: Identity<B, A, Inverse = Self>;
    fn conv(&self, x: A) -> B
    where
        A: Sized,
        B: Sized;
    fn conv_ref<'a>(&self, x: &'a A) -> &'a B;
    fn conv_mut<'a>(&self, x: &'a mut A) -> &'a mut B;
    fn conv_box(&self, x: Box<A>) -> Box<B>;
    fn conv_under<TF: TyFun<A> + TyFun<B>>(
        &self, 
        x: <TF as TyFun<A>>::Result
    ) -> <TF as TyFun<B>>::Result
    where
        <TF as TyFun<A>>::Result: Sized,
        <TF as TyFun<B>>::Result: Sized;
    fn inv(&self) -> &Self::Inverse;
    fn elim<Prop: TysFun<TyPair<A, Refl<A>>> + TysFun<TyPair<B, Self>>>(
        &self, 
        refl_case: <Prop as TysFun<TyPair<A, Refl<A>>>>::Result
    ) -> <Prop as TysFun<TyPair<B, Self>>>::Result
    where
        <Prop as TysFun<TyPair<A, Refl<A>>>>::Result: Sized,
        <Prop as TysFun<TyPair<B, Self>>>::Result: Sized;
    fn elim_alt<Prop: TysFun<TyTriple<A, B, Self>>, ReflCase: Forall<AndThen<MLReflCase, Uncurry<Prop>>>>(
        &self, 
        refl_case: ReflCase
    ) -> <Prop as TysFun<TyTriple<A, B, Self>>>::Result
    where
        <Prop as TysFun<TyTriple<A, B, Self>>>::Result: Sized;
}

An identity type; that is, the type bound of “equality witnesses.”

Associated Types

type Inverse: Identity<B, A, Inverse = Self>

Required Methods

fn conv(&self, x: A) -> B where
    A: Sized,
    B: Sized, 

fn conv_ref<'a>(&self, x: &'a A) -> &'a B

fn conv_mut<'a>(&self, x: &'a mut A) -> &'a mut B

fn conv_box(&self, x: Box<A>) -> Box<B>

fn conv_under<TF: TyFun<A> + TyFun<B>>(
    &self,
    x: <TF as TyFun<A>>::Result
) -> <TF as TyFun<B>>::Result where
    <TF as TyFun<A>>::Result: Sized,
    <TF as TyFun<B>>::Result: Sized, 

Leibniz's identity rule, approximately.

fn inv(&self) -> &Self::Inverse

fn elim<Prop: TysFun<TyPair<A, Refl<A>>> + TysFun<TyPair<B, Self>>>(
    &self,
    refl_case: <Prop as TysFun<TyPair<A, Refl<A>>>>::Result
) -> <Prop as TysFun<TyPair<B, Self>>>::Result where
    <Prop as TysFun<TyPair<A, Refl<A>>>>::Result: Sized,
    <Prop as TysFun<TyPair<B, Self>>>::Result: Sized, 

Paulin-Mohring's J rule, approximately.

fn elim_alt<Prop: TysFun<TyTriple<A, B, Self>>, ReflCase: Forall<AndThen<MLReflCase, Uncurry<Prop>>>>(
    &self,
    refl_case: ReflCase
) -> <Prop as TysFun<TyTriple<A, B, Self>>>::Result where
    <Prop as TysFun<TyTriple<A, B, Self>>>::Result: Sized, 

Martin-Löf's J rule, approximately.

Implementors

• impl<A: ?Sized> Identity<A, A> for Refl<A>