Struct True

pub struct True;

Logical true.

Trait Implementations

impl Clone for True

fn clone(&self) -> True

Returns a duplicate of the value.

const fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Decidable for True

fn decide() -> ExcM<True>

Get excluded middle rule.

impl Existential for True

fn e() -> E<Self>

Get existential rule.

impl<A: Prop> HomotopyEquality<A> for True

fn refl() -> Self

hom_eq(n, a, a).

impl<A: Prop, B: Prop> HomotopyEquivalence<A, B> for True

type N = Z

The associated homotopy level.

type Rel<A2: Prop, B2: Prop> = True

Relation constructor.

fn transitivity<C: Prop>(self, _: True) -> True

hom_eq(n, a, b) ⋀ hom_eq(n, b, c) => hom_eq(n, a, c).

fn symmetry(self) -> True

hom_eq(n, a, b) => hom_eq(n, b, a).

fn cast<A2: Prop, B2: Prop>(_: True) -> True

Cast to self.

fn cast_lift<A2: Prop, B2: Prop>(self) -> True

Cast to other.

impl<A: Prop, B: Prop> HomotopyLevel0<A, B> for True

type H0 = True

A type such that it proves homotopy level 0.

fn h0<X: LProp>(_ty_x: Ty<X, Self>) -> HomEq<Z, True, X>

Homotopy level 0.

impl Copy for True