structure Data.Functor.Identity (α : Type u) : Type u

The identity functor. Identity α is isomorphic to α.

• runIdentity : α

def Data.Functor.instBEqIdentity.beq {α✝ : Type u_1} [BEq α✝] : Identity α✝ → Identity α✝ → Bool

Equations

• Data.Functor.instBEqIdentity.beq { runIdentity := a } { runIdentity := b } = (a == b)
• Data.Functor.instBEqIdentity.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Data.Functor.instBEqIdentity {α✝ : Type u_1} [BEq α✝] : BEq (Identity α✝)

Equations

• Data.Functor.instBEqIdentity = { beq := Data.Functor.instBEqIdentity.beq }

def Data.Functor.instOrdIdentity.ord {α✝ : Type u_1} [Ord α✝] : Identity α✝ → Identity α✝ → Ordering

Equations

• Data.Functor.instOrdIdentity.ord { runIdentity := a } { runIdentity := b } = (compare a b).then Ordering.eq

@[implicit_reducible]

instance Data.Functor.instOrdIdentity {α✝ : Type u_1} [Ord α✝] : Ord (Identity α✝)

Equations

• Data.Functor.instOrdIdentity = { compare := Data.Functor.instOrdIdentity.ord }

def Data.Functor.instReprIdentity.repr {α✝ : Type u_1} [Repr α✝] : Identity α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Functor.instReprIdentity {α✝ : Type u_1} [Repr α✝] : Repr (Identity α✝)

Equations

• Data.Functor.instReprIdentity = { reprPrec := Data.Functor.instReprIdentity.repr }

def Data.Functor.instHashableIdentity.hash {α✝ : Type u_1} [Hashable α✝] : Identity α✝ → UInt64

Equations

• Data.Functor.instHashableIdentity.hash { runIdentity := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance Data.Functor.instHashableIdentity {α✝ : Type u_1} [Hashable α✝] : Hashable (Identity α✝)

Equations

• Data.Functor.instHashableIdentity = { hash := Data.Functor.instHashableIdentity.hash }

def Data.Functor.instInhabitedIdentity.default {a✝ : Type u_1} [Inhabited a✝] : Identity a✝

Equations

• Data.Functor.instInhabitedIdentity.default = { runIdentity := default }

@[implicit_reducible]

instance Data.Functor.instInhabitedIdentity {a✝ : Type u_1} [Inhabited a✝] : Inhabited (Identity a✝)

Equations

• Data.Functor.instInhabitedIdentity = { default := Data.Functor.instInhabitedIdentity.default }

@[implicit_reducible]

instance Data.Functor.instToStringIdentity {α : Type u_1} [ToString α] : ToString (Identity α)

Equations

• Data.Functor.instToStringIdentity = { toString := fun (i : Data.Functor.Identity α) => toString i.runIdentity }

@[implicit_reducible]

instance Data.Functor.instFunctorIdentity : Functor Identity

Equations

• Data.Functor.instFunctorIdentity = { map := fun {α β : Type ?u.13} (f : α → β) (i : Data.Functor.Identity α) => { runIdentity := f i.runIdentity } }

@[implicit_reducible]

instance Data.Functor.instPureIdentity : Pure Identity

Equations

• Data.Functor.instPureIdentity = { pure := fun {α : Type ?u.6} (a : α) => { runIdentity := a } }

@[implicit_reducible]

instance Data.Functor.instBindIdentity : Bind Identity

Equations

• Data.Functor.instBindIdentity = { bind := fun {α β : Type ?u.9} (i : Data.Functor.Identity α) (f : α → Data.Functor.Identity β) => f i.runIdentity }

@[implicit_reducible]

instance Data.Functor.instSeqIdentity : Seq Identity

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Functor.instApplicativeIdentity : Applicative Identity

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Data.Functor.instMonadIdentity : Monad Identity

Equations

• Data.Functor.instMonadIdentity = { toApplicative := Data.Functor.instApplicativeIdentity, toBind := Data.Functor.instBindIdentity }

theorem Data.Functor.Identity.map_id {α : Type u_1} (x : Identity α) : id <$> x = x

theorem Data.Functor.Identity.map_comp {β γ α : Type u_1} (f : β → γ) (g : α → β) (x : Identity α) : (f ∘ g) <$> x = f <$> g <$> x

theorem Data.Functor.Identity.pure_bind {α β : Type u_1} (a : α) (f : α → Identity β) : pure a >>= f = f a

theorem Data.Functor.Identity.bind_pure {α : Type u_1} (x : Identity α) : x >>= pure = x

theorem Data.Functor.Identity.bind_assoc {α β γ : Type u_1} (x : Identity α) (f : α → Identity β) (g : β → Identity γ) : x >>= f >>= g = x >>= fun (a : α) => f a >>= g