Functor Constructions

This file defines various Functor and Sequence constructions.

structure QuasiBorelSpace.Sequence.Compose (F : Type u → Type u) (S : ℕ → Type u) (n : ℕ) : Type u

• val : F (S n)

theorem QuasiBorelSpace.Sequence.Compose.ext {F : Type u → Type u} {S : ℕ → Type u} {n : ℕ} {x y : Compose F S n} (val : x.val = y.val) : x = y

theorem QuasiBorelSpace.Sequence.Compose.ext_iff {F : Type u → Type u} {S : ℕ → Type u} {n : ℕ} {x y : Compose F S n} : x = y ↔ x.val = y.val

@[instance_reducible]

instance QuasiBorelSpace.Sequence.Compose.inst {F : Type u_1 → Type u_1} {S : ℕ → Type u_1} [Functor F] [Sequence S] {n : ℕ} : QuasiBorelSpace (Compose F S n)

Equations

• QuasiBorelSpace.Sequence.Compose.inst = QuasiBorelSpace.lift QuasiBorelSpace.Sequence.Compose.val

@[simp]

theorem QuasiBorelSpace.Sequence.Compose.isHom_mk {F : Type u_1 → Type u_1} {S : ℕ → Type u_1} [Functor F] [Sequence S] {n : ℕ} : IsHom mk

@[simp]

theorem QuasiBorelSpace.Sequence.Compose.isHom_val {F : Type u_1 → Type u_1} {S : ℕ → Type u_1} [Functor F] [Sequence S] {n : ℕ} : IsHom val

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Sequence.Compose.inst_1 {F : Type u_1 → Type u_1} {S : ℕ → Type u_1} [Functor F] [Sequence S] : Sequence (Compose F S)

Equations

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

noncomputable def QuasiBorelSpace.Sequence.Compose.map {F : Type u_1 → Type u_1} {S S' : ℕ → Type u_1} [Functor F] [Sequence S] [Sequence S'] {i : ℕ} (f : {i : ℕ} → S i → S' i) : Compose F S i → Compose F S' i

Equations

• QuasiBorelSpace.Sequence.Compose.map f { val := x_1 } = { val := QuasiBorelSpace.Functor.map f x_1 }

def QuasiBorelSpace.Sequence.Iterate.Internal (F : Type u → Type u) : ℕ → Type u

Equations

• QuasiBorelSpace.Sequence.Iterate.Internal F 0 = PEmpty.{?u.1 + 1}
• QuasiBorelSpace.Sequence.Iterate.Internal F n.succ = F (QuasiBorelSpace.Sequence.Iterate.Internal F n)

structure QuasiBorelSpace.Sequence.Iterate (F : Type u → Type u) (n : ℕ) : Type u

• val : Internal F n

@[instance_reducible]

instance QuasiBorelSpace.Sequence.Iterate.Internal.instQuasiBorelSpace {F : Type u_1 → Type u_1} [Functor F] (n : ℕ) : QuasiBorelSpace (Internal F n)

Equations

• QuasiBorelSpace.Sequence.Iterate.Internal.instQuasiBorelSpace 0 = inferInstance
• QuasiBorelSpace.Sequence.Iterate.Internal.instQuasiBorelSpace n.succ = inferInstance

noncomputable def QuasiBorelSpace.Sequence.Iterate.Internal.lift {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} : Internal F n → Internal F (n + 1)

Equations

• QuasiBorelSpace.Sequence.Iterate.Internal.lift = PEmpty.elim
• QuasiBorelSpace.Sequence.Iterate.Internal.lift = QuasiBorelSpace.Functor.map QuasiBorelSpace.Sequence.Iterate.Internal.lift

@[instance_reducible]

instance QuasiBorelSpace.Sequence.Iterate.inst {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} : QuasiBorelSpace (Iterate F n)

Equations

• QuasiBorelSpace.Sequence.Iterate.inst = QuasiBorelSpace.lift QuasiBorelSpace.Sequence.Iterate.val

noncomputable def QuasiBorelSpace.Sequence.Iterate.roll {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} : F (Iterate F n) → Iterate F (n + 1)

Equations

• QuasiBorelSpace.Sequence.Iterate.roll x✝ = { val := QuasiBorelSpace.Functor.map QuasiBorelSpace.Sequence.Iterate.val x✝ }

noncomputable def QuasiBorelSpace.Sequence.Iterate.unroll {F : Type u_1 → Type u_1} [Functor F] {n : ℕ} : Iterate F (n + 1) → F (Iterate F n)

Equations

• { val := x_1 }.unroll = QuasiBorelSpace.Functor.map QuasiBorelSpace.Sequence.Iterate.mk x_1

def QuasiBorelSpace.Sequence.Iterate.elim {F : Type u_2 → Type u_2} {A : Sort u_1} : Iterate F 0 → A

Equations

• QuasiBorelSpace.Sequence.Iterate.elim = PEmpty.elim ∘ QuasiBorelSpace.Sequence.Iterate.val

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Sequence.Iterate.inst_1 {F : Type u_1 → Type u_1} [Functor F] : Sequence (Iterate F)

Equations

• QuasiBorelSpace.Sequence.Iterate.inst_1 = QuasiBorelSpace.Sequence.fromStep fun (x : ℕ) (x_1 : QuasiBorelSpace.Sequence.Iterate F x) => { val := x_1.val.lift }

inductive QuasiBorelSpace.Functor.Sum (F G : Type u → Type v) (A : Type u) : Type v

• inl {F G : Type u → Type v} {A : Type u} : F A → Sum F G A
• inr {F G : Type u → Type v} {A : Type u} : G A → Sum F G A

def QuasiBorelSpace.Functor.Sum.toSum {F G : Type u_1 → Type u_2} {A : Type u_1} : Sum F G A → F A ⊕ G A

Equations

• (QuasiBorelSpace.Functor.Sum.inl x_1).toSum = Sum.inl x_1
• (QuasiBorelSpace.Functor.Sum.inr x_1).toSum = Sum.inr x_1

def QuasiBorelSpace.Functor.Sum.ofSum {F G : Type u_1 → Type u_2} {A : Type u_1} : F A ⊕ G A → Sum F G A

Equations

• QuasiBorelSpace.Functor.Sum.ofSum (Sum.inl x_1) = QuasiBorelSpace.Functor.Sum.inl x_1
• QuasiBorelSpace.Functor.Sum.ofSum (Sum.inr x_1) = QuasiBorelSpace.Functor.Sum.inr x_1

@[instance_reducible]

instance QuasiBorelSpace.Functor.Sum.inst {F G : Type u_1 → Type u_2} {A : Type u_1} [Functor F] [Functor G] [QuasiBorelSpace A] : QuasiBorelSpace (Sum F G A)

Equations

• QuasiBorelSpace.Functor.Sum.inst = QuasiBorelSpace.lift QuasiBorelSpace.Functor.Sum.toSum

@[simp]

theorem QuasiBorelSpace.Functor.Sum.toSum_ofSum {F✝ : Type u_1 → Type u_2} {a✝ : Type u_1} {G✝ : Type u_1 → Type u_2} {x : F✝ a✝ ⊕ G✝ a✝} : (ofSum x).toSum = x

@[simp]

theorem QuasiBorelSpace.Functor.Sum.isHom_toSum {F G : Type u_2 → Type u_1} {A : Type u_2} [Functor F] [Functor G] [QuasiBorelSpace A] : IsHom toSum

@[simp]

theorem QuasiBorelSpace.Functor.Sum.isHom_ofSum {F G : Type u_2 → Type u_1} {A : Type u_2} [Functor F] [Functor G] [QuasiBorelSpace A] : IsHom ofSum

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Functor.Sum.inst_1 {F G : Type u_1 → Type u_2} [Functor F] [Functor G] : Functor (Sum F G)

Equations

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

structure QuasiBorelSpace.Functor.Prod (F G : Type u → Type v) (A : Type u) : Type v

• fst : F A
• snd : G A

theorem QuasiBorelSpace.Functor.Prod.ext {F G : Type u → Type v} {A : Type u} {x y : Prod F G A} (fst : x.fst = y.fst) (snd : x.snd = y.snd) : x = y

theorem QuasiBorelSpace.Functor.Prod.ext_iff {F G : Type u → Type v} {A : Type u} {x y : Prod F G A} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

def QuasiBorelSpace.Functor.Prod.toProd {F G : Type u_1 → Type u_2} {A : Type u_1} : Prod F G A → F A × G A

Equations

• { fst := x_1, snd := y }.toProd = (x_1, y)

def QuasiBorelSpace.Functor.Prod.ofProd {F G : Type u_1 → Type u_2} {A : Type u_1} : F A × G A → Prod F G A

Equations

• QuasiBorelSpace.Functor.Prod.ofProd (x_1, y) = { fst := x_1, snd := y }

@[instance_reducible]

instance QuasiBorelSpace.Functor.Prod.inst {F G : Type u_1 → Type u_2} {A : Type u_1} [Functor F] [Functor G] [QuasiBorelSpace A] : QuasiBorelSpace (Prod F G A)

Equations

• QuasiBorelSpace.Functor.Prod.inst = QuasiBorelSpace.lift QuasiBorelSpace.Functor.Prod.toProd

@[simp]

theorem QuasiBorelSpace.Functor.Prod.toProd_ofProd {F✝ : Type u_1 → Type u_2} {a✝ : Type u_1} {G✝ : Type u_1 → Type u_2} {x : F✝ a✝ × G✝ a✝} : (ofProd x).toProd = x

@[simp]

theorem QuasiBorelSpace.Functor.Prod.isHom_toProd {F G : Type u_2 → Type u_1} {A : Type u_2} [Functor F] [Functor G] [QuasiBorelSpace A] : IsHom toProd

@[simp]

theorem QuasiBorelSpace.Functor.Prod.isHom_ofProd {F G : Type u_2 → Type u_1} {A : Type u_2} [Functor F] [Functor G] [QuasiBorelSpace A] : IsHom ofProd

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Functor.Prod.inst_1 {F G : Type u_1 → Type u_2} [Functor F] [Functor G] : Functor (Prod F G)

Equations

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

structure QuasiBorelSpace.Functor.Const (A : Type u_1) (B : Type u_2) : Type u_1

• val : A

@[instance_reducible]

instance QuasiBorelSpace.Functor.Const.inst {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} : QuasiBorelSpace (Const A B)

Equations

• QuasiBorelSpace.Functor.Const.inst = QuasiBorelSpace.lift QuasiBorelSpace.Functor.Const.val

@[simp]

theorem QuasiBorelSpace.Functor.Const.isHom_val {A : Type u_2} [QuasiBorelSpace A] {B : Type u_1} : IsHom val

@[simp]

theorem QuasiBorelSpace.Functor.Const.isHom_mk {A : Type u_2} [QuasiBorelSpace A] {B : Type u_1} : IsHom mk

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Functor.Const.inst_1 {A : Type u_1} [QuasiBorelSpace A] : Functor (Const A)

Equations

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

structure QuasiBorelSpace.Functor.Identity (A : Type u_1) : Type u_1

• val : A

@[instance_reducible]

instance QuasiBorelSpace.Functor.Identity.inst {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (Identity A)

Equations

• QuasiBorelSpace.Functor.Identity.inst = QuasiBorelSpace.lift QuasiBorelSpace.Functor.Identity.val

@[simp]

theorem QuasiBorelSpace.Functor.Identity.isHom_val {A : Type u_1} [QuasiBorelSpace A] : IsHom val

@[simp]

theorem QuasiBorelSpace.Functor.Identity.isHom_mk {A : Type u_1} [QuasiBorelSpace A] : IsHom mk

@[instance_reducible]

noncomputable instance QuasiBorelSpace.Functor.Identity.inst_1 : Functor Identity

Equations

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