theorem
functor.map_comp_map
{F : Type u → Type v}
{α β γ : Type u}
[functor F]
[is_lawful_functor F]
(f : α → β)
(g : β → γ) :
functor.map g ∘ functor.map f = functor.map (g ∘ f)
theorem
functor.ext
{F : Type u_1 → Type u_2}
{F1 F2 : functor F}
[is_lawful_functor F]
[is_lawful_functor F] :
Equations
- functor.const.mk x = x
Equations
- functor.const.mk' x = x
@[nolint]
def
functor.const.map
{γ : Type u_1}
{α : Type u_2}
{β : Type u_3} :
(α → β) → functor.const γ β → functor.const γ α
The map operation of the const γ functor.
Equations
- functor.const.map f x = x
@[instance]
Equations
- functor.const.functor = {map := functor.const.map γ, map_const := λ (α β : Type u_2), functor.const.map ∘ function.const β}
@[instance]
Equations
Equations
Equations
Equations
@[instance]
Equations
@[instance]
functor.comp is a wrapper around function.comp for types.
It prevents Lean's type class resolution mechanism from trying
a functor (comp F id) when functor F would do.
Equations
- functor.comp F G α = F (G α)
def
functor.comp.mk
{F : Type u → Type w}
{G : Type v → Type u}
{α : Type v} :
F (G α) → functor.comp F G α
Equations
- functor.comp.mk x = x
def
functor.comp.run
{F : Type u → Type w}
{G : Type v → Type u}
{α : Type v} :
functor.comp F G α → F (G α)
theorem
functor.comp.ext
{F : Type u → Type w}
{G : Type v → Type u}
{α : Type v}
{x y : functor.comp F G α} :
def
functor.comp.map
{F : Type u → Type w}
{G : Type v → Type u}
[functor F]
[functor G]
{α β : Type v} :
(α → β) → functor.comp F G α → functor.comp F G β
Equations
- functor.comp.map h (functor.comp.mk x) = functor.comp.mk (functor.map h <$> x)
@[instance]
def
functor.comp.functor
{F : Type u → Type w}
{G : Type v → Type u}
[functor F]
[functor G] :
functor (functor.comp F G)
Equations
- functor.comp.functor = {map := functor.comp.map _inst_2, map_const := λ (α β : Type v), functor.comp.map ∘ function.const β}
theorem
functor.comp.map_mk
{F : Type u → Type w}
{G : Type v → Type u}
[functor F]
[functor G]
{α β : Type v}
(h : α → β)
(x : F (G α)) :
h <$> functor.comp.mk x = functor.comp.mk (functor.map h <$> x)
@[simp]
theorem
functor.comp.run_map
{F : Type u → Type w}
{G : Type v → Type u}
[functor F]
[functor G]
{α β : Type v}
(h : α → β)
(x : functor.comp F G α) :
functor.comp.run (h <$> x) = functor.map h <$> x.run
theorem
functor.comp.id_map
{F : Type u → Type w}
{G : Type v → Type u}
[functor F]
[functor G]
[is_lawful_functor F]
[is_lawful_functor G]
{α : Type v}
(x : functor.comp F G α) :
functor.comp.map id x = x
theorem
functor.comp.comp_map
{F : Type u → Type w}
{G : Type v → Type u}
[functor F]
[functor G]
[is_lawful_functor F]
[is_lawful_functor G]
{α β γ : Type v}
(g' : α → β)
(h : β → γ)
(x : functor.comp F G α) :
functor.comp.map (h ∘ g') x = functor.comp.map h (functor.comp.map g' x)
@[instance]
def
functor.comp.is_lawful_functor
{F : Type u → Type w}
{G : Type v → Type u}
[functor F]
[functor G]
[is_lawful_functor F]
[is_lawful_functor G] :
Equations
theorem
functor.comp.functor_comp_id
{F : Type u_1 → Type u_2}
[AF : functor F]
[is_lawful_functor F] :
theorem
functor.comp.functor_id_comp
{F : Type u_1 → Type u_2}
[AF : functor F]
[is_lawful_functor F] :
def
functor.comp.seq
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G]
{α β : Type v} :
functor.comp F G (α → β) → functor.comp F G α → functor.comp F G β
Equations
- (functor.comp.mk f).seq (functor.comp.mk x) = functor.comp.mk (has_seq.seq <$> f <*> x)
@[instance]
def
functor.comp.has_pure
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G] :
has_pure (functor.comp F G)
Equations
- functor.comp.has_pure = {pure := λ (_x : Type v) (x : _x), functor.comp.mk (has_pure.pure (has_pure.pure x))}
@[instance]
def
functor.comp.has_seq
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G] :
has_seq (functor.comp F G)
Equations
- functor.comp.has_seq = {seq := λ (_x _x_1 : Type v) (f : functor.comp F G (_x → _x_1)) (x : functor.comp F G _x), f.seq x}
@[simp]
theorem
functor.comp.run_pure
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G]
{α : Type v}
(x : α) :
(has_pure.pure x).run = has_pure.pure (has_pure.pure x)
@[simp]
theorem
functor.comp.run_seq
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G]
{α β : Type v}
(f : functor.comp F G (α → β))
(x : functor.comp F G α) :
@[instance]
def
functor.comp.applicative
{F : Type u → Type w}
{G : Type v → Type u}
[applicative F]
[applicative G] :
applicative (functor.comp F G)
Equations
If we consider x : F α to, in some sense, contain values of type α,
predicate liftp p x holds iff, every value contained by x satisfies p
Equations
- functor.liftp p x = ∃ (u : F (subtype p)), subtype.val <$> u = x
def
functor.liftr
{F : Type u → Type u}
[functor F]
{α : Type u} :
(α → α → Prop) → F α → F α → Prop
liftr r x y relates x and y iff x and y have the same shape and that
we can pair values a from x and b from y so that r a b holds
supp x is the set of values of type α that x contains
Equations
- functor.supp x = {y : α | ∀ ⦃p : α → Prop⦄, functor.liftp p x → p y}
theorem
functor.of_mem_supp
{F : Type u → Type u}
[functor F]
{α : Type u}
{x : F α}
{p : α → Prop}
(h : functor.liftp p x)
(y : α) :
y ∈ functor.supp x → p y
@[instance]
Equations
- ulift.functor = {map := λ (α β : Type u_1) (f : α → β), ulift.up ∘ f ∘ ulift.down, map_const := λ (α β : Type u_1), (λ (f : β → α), ulift.up ∘ f ∘ ulift.down) ∘ function.const β}