/-
Copyright (c) 2023 Antoine Labelle. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Antoine Labelle

! This file was ported from Lean 3 source module combinatorics.quiver.single_obj
! leanprover-community/mathlib commit 509de852e1de55e1efa8eacfa11df0823f26f226
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Combinatorics.Quiver.Cast
import Mathlib.Combinatorics.Quiver.Symmetric

/-!
# Single-object quiver

Single object quiver with a given arrows type.

## Main definitions

Given a type `α`, `SingleObj α` is the `Unit` type, whose single object is called `star α`, with
`Quiver` structure such that `star α ⟶ star α` is the type `α`.
An element `x : α` can be reinterpreted as an element of `star α ⟶ star α` using
`toHom`.
More generally, a list of elements of `a` can be reinterpreted as a path from `star α` to
itself using `pathEquivList`.
-/


namespace Quiver

/-- Type tag on `Unit` used to define single-object quivers. -/
-- Porting note: Removed `deriving Unique`.
@[nolint 
unusedArguments: Std.Tactic.Lint.Linter
unusedArguments]
def 
SingleObj: Type ?u.2 → Type
SingleObj (
_: Type ?u.2
_ : 
Type _: Type (?u.2+1)
Type _) : 
Type: Type 1
Type :=
  
Unit: Type
Unit
#align quiver.single_obj 
Quiver.SingleObj: Type u_1 → Type
Quiver.SingleObj

-- Porting note: `deriving` from above has been moved to below.
instance: {α : Type u_1} → Unique (SingleObj α)
instance : 
Unique: Sort ?u.16 → Sort (max1?u.16)
Unique (
SingleObj: Type ?u.17 → Type
SingleObj 
α: ?m.13
α) where
  default := 
⟨⟩: PUnit
⟨⟩
  uniq := fun 
_: ?m.28
_ => 
rfl: ∀ {α : Sort ?u.30} {a : α}, a = a
rfl

namespace SingleObj

variable (
α: Type ?u.1704
α 
β: Type ?u.4805
β 
γ: Type ?u.267
γ : 
Type _: Type (?u.1502+1)
Type _)

instance: (α : Type u_1) → Quiver (SingleObj α)
instance : 
Quiver: Type ?u.103 → Type (max?u.103?u.104)
Quiver (
SingleObj: Type ?u.105 → Type
SingleObj 
α: Type ?u.94
α) :=
  ⟨fun 
_: ?m.114
_ 
_: ?m.117
_ => 
α: Type ?u.94
α⟩

/-- The single object in `SingleObj α`. -/
def 
star: SingleObj α
star : 
SingleObj: Type ?u.178 → Type
SingleObj 
α: Type ?u.169
α :=
  
Unit.unit: Unit
Unit.unit
#align quiver.single_obj.star 
Quiver.SingleObj.star: (α : Type u_1) → SingleObj α
Quiver.SingleObj.star

instance: (α : Type u_1) → Inhabited (SingleObj α)
instance : 
Inhabited: Sort ?u.205 → Sort (max1?u.205)
Inhabited (
SingleObj: Type ?u.206 → Type
SingleObj 
α: Type ?u.196
α) :=
  ⟨
star: (α : Type ?u.213) → SingleObj α
star 
α: Type ?u.196
α⟩

variable {
α: ?m.252
α 
β: ?m.255
β 
γ: ?m.258
γ}

lemma 
ext: ∀ {x y : SingleObj α}, x = y
ext {
x: SingleObj α
x 
y: SingleObj α
y : 
SingleObj: Type ?u.273 → Type
SingleObj 
α: Type ?u.261
α} : 
x: SingleObj α
x = 
y: SingleObj α
y := 
Unit.ext: ∀ (x y : Unit), x = y
Unit.ext 
x: SingleObj α
x 
y: SingleObj α
y

-- See note [reducible non-instances]
/-- Equip `SingleObj α` with a reverse operation. -/
@[reducible]
def 
hasReverse: (α → α) → HasReverse (SingleObj α)
hasReverse (
rev: α → α
rev : 
α: Type ?u.289
α → 
α: Type ?u.289
α) : 
HasReverse: (V : Type ?u.302) → [inst : Quiver V] → Type (max?u.302?u.303)
HasReverse (
SingleObj: Type ?u.304 → Type
SingleObj 
α: Type ?u.289
α) := ⟨
rev: α → α
rev⟩
#align quiver.single_obj.has_reverse 
Quiver.SingleObj.hasReverse: {α : Type u_1} → (α → α) → HasReverse (SingleObj α)
Quiver.SingleObj.hasReverse

-- See note [reducible non-instances]
/-- Equip `SingleObj α` with an involutive reverse operation. -/
@[reducible]
def 
hasInvolutiveReverse: (rev : α → α) → Function.Involutive rev → HasInvolutiveReverse (SingleObj α)
hasInvolutiveReverse (
rev: α → α
rev : 
α: Type ?u.446
α → 
α: Type ?u.446
α) (
h: Function.Involutive rev
h : 
Function.Involutive: {α : Sort ?u.459} → (α → α) → Prop
Function.Involutive 
rev: α → α
rev) :
    
HasInvolutiveReverse: (V : Type ?u.466) → [inst : Quiver V] → Type (max?u.466?u.467)
HasInvolutiveReverse (
SingleObj: Type ?u.468 → Type
SingleObj 
α: Type ?u.446
α) where
  toHasReverse := 
hasReverse: {α : Type ?u.491} → (α → α) → HasReverse (SingleObj α)
hasReverse 
rev: α → α
rev
  inv' := 
h: Function.Involutive rev
h
#align quiver.single_obj.has_involutive_reverse 
Quiver.SingleObj.hasInvolutiveReverse: {α : Type u_1} → (rev : α → α) → Function.Involutive rev → HasInvolutiveReverse (SingleObj α)
Quiver.SingleObj.hasInvolutiveReverse

/-- The type of arrows from `star α` to itself is equivalent to the original type `α`. -/
@[simps!]
def 
toHom: {α : Type u_1} → α ≃ (star α ⟶ star α)
toHom : 
α: Type ?u.609
α ≃ (
star: (α : Type ?u.639) → SingleObj α
star 
α: Type ?u.609
α ⟶ 
star: (α : Type ?u.641) → SingleObj α
star 
α: Type ?u.609
α) :=
  
Equiv.refl: (α : Sort ?u.650) → α ≃ α
Equiv.refl 
_: Sort ?u.650
_
#align quiver.single_obj.to_hom 
Quiver.SingleObj.toHom: {α : Type u_1} → α ≃ (star α ⟶ star α)
Quiver.SingleObj.toHom
#align quiver.single_obj.to_hom_apply 
Quiver.SingleObj.toHom_apply: ∀ {α : Type u_1} (a : α), ↑toHom a = a
Quiver.SingleObj.toHom_apply
#align quiver.single_obj.to_hom_symm_apply 
Quiver.SingleObj.toHom_symm_apply: ∀ {α : Type u_1} (a : α), ↑toHom.symm a = a
Quiver.SingleObj.toHom_symm_apply

/-- Prefunctors between two `SingleObj` quivers correspond to functions between the corresponding
arrows types.
-/
@[
simps: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {X Y : SingleObj α} (a : α), (↑toPrefunctor f).map a = f a
simps]
def 
toPrefunctor: {α : Type u_1} → {β : Type u_2} → (α → β) ≃ SingleObj α ⥤q SingleObj β
toPrefunctor : (
α: Type ?u.745
α → 
β: Type ?u.748
β) ≃ 
SingleObj: Type ?u.763 → Type
SingleObj 
α: Type ?u.745
α ⥤q 
SingleObj: Type ?u.765 → Type
SingleObj 
β: Type ?u.748
β where
  toFun 
f: ?m.790
f := ⟨
id: {α : Sort ?u.846} → α → α
id, 
f: ?m.790
f⟩
  invFun 
f: ?m.874
f 
a: ?m.877
a := 
f: ?m.874
f.
map: {V : Type ?u.880} →
  [inst : Quiver V] →
    {W : Type ?u.879} → [inst_1 : Quiver W] → (self : V ⥤q W) → {X Y : V} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
map (
toHom: {α : Type ?u.891} → α ≃ (star α ⟶ star α)
toHom 
a: ?m.877
a)
  left_inv 
_: ?m.963
_ := 
rfl: ∀ {α : Sort ?u.966} {a : α}, a = a
rfl
  right_inv 
_: ?m.987
_ := 
rfl: ∀ {α : Sort ?u.989} {a : α}, a = a
rfl
#align quiver.single_obj.to_prefunctor_symm_apply 
Quiver.SingleObj.toPrefunctor_symm_apply: ∀ {α : Type u_1} {β : Type u_2} (f : SingleObj α ⥤q SingleObj β) (a : α), ↑toPrefunctor.symm f a = f.map (↑toHom a)
Quiver.SingleObj.toPrefunctor_symm_apply
#align quiver.single_obj.to_prefunctor_apply_map 
Quiver.SingleObj.toPrefunctor_apply_map: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {X Y : SingleObj α} (a : α), (↑toPrefunctor f).map a = f a
Quiver.SingleObj.toPrefunctor_apply_map
#align quiver.single_obj.to_prefunctor_apply_obj 
Quiver.SingleObj.toPrefunctor_apply_obj: ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : SingleObj α), (↑toPrefunctor f).obj a = id a
Quiver.SingleObj.toPrefunctor_apply_obj

#align quiver.single_obj.to_prefunctor 
Quiver.SingleObj.toPrefunctor: {α : Type u_1} → {β : Type u_2} → (α → β) ≃ SingleObj α ⥤q SingleObj β
Quiver.SingleObj.toPrefunctor

theorem 
toPrefunctor_id: ↑toPrefunctor id = 𝟭q (SingleObj α)
toPrefunctor_id : 
toPrefunctor: {α : Type ?u.1510} → {β : Type ?u.1509} → (α → β) ≃ SingleObj α ⥤q SingleObj β
toPrefunctor 
id: {α : Sort ?u.1594} → α → α
id = 
𝟭q: (V : Type ?u.1600) → [inst : Quiver V] → V ⥤q V
𝟭q (
SingleObj: Type ?u.1603 → Type
SingleObj 
α: Type ?u.1499
α) :=
  
rfl: ∀ {α : Sort ?u.1669} {a : α}, a = a
rfl
#align quiver.single_obj.to_prefunctor_id 
Quiver.SingleObj.toPrefunctor_id: ∀ {α : Type u_1}, ↑toPrefunctor id = 𝟭q (SingleObj α)
Quiver.SingleObj.toPrefunctor_id

@[simp]
theorem 
toPrefunctor_symm_id: ∀ {α : Type u_1}, ↑toPrefunctor.symm (𝟭q (SingleObj α)) = id
toPrefunctor_symm_id : 
toPrefunctor: {α : Type ?u.1715} → {β : Type ?u.1714} → (α → β) ≃ SingleObj α ⥤q SingleObj β
toPrefunctor.
symm: {α : Sort ?u.1719} → {β : Sort ?u.1718} → α ≃ β → β ≃ α
symm (
𝟭q: (V : Type ?u.1806) → [inst : Quiver V] → V ⥤q V
𝟭q (
SingleObj: Type ?u.1809 → Type
SingleObj 
α: Type ?u.1704
α)) = 
id: {α : Sort ?u.1830} → α → α
id :=
  
rfl: ∀ {α : Sort ?u.1880} {a : α}, a = a
rfl
#align quiver.single_obj.to_prefunctor_symm_id 
Quiver.SingleObj.toPrefunctor_symm_id: ∀ {α : Type u_1}, ↑toPrefunctor.symm (𝟭q (SingleObj α)) = id
Quiver.SingleObj.toPrefunctor_symm_id

theorem 
toPrefunctor_comp: ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_2} (f : α → β) (g : β → γ),
  ↑toPrefunctor (g ∘ f) = ↑toPrefunctor f ⋙q ↑toPrefunctor g
toPrefunctor_comp (
f: α → β
f : 
α: Type ?u.1924
α → 
β: Type ?u.1927
β) (
g: β → γ
g : 
β: Type ?u.1927
β → 
γ: Type ?u.1930
γ) :
    
toPrefunctor: {α : Type ?u.1943} → {β : Type ?u.1942} → (α → β) ≃ SingleObj α ⥤q SingleObj β
toPrefunctor (
g: β → γ
g ∘ 
f: α → β
f) = 
toPrefunctor: {α : Type ?u.2057} → {β : Type ?u.2056} → (α → β) ≃ SingleObj α ⥤q SingleObj β
toPrefunctor 
f: α → β
f ⋙q 
toPrefunctor: {α : Type ?u.2155} → {β : Type ?u.2154} → (α → β) ≃ SingleObj α ⥤q SingleObj β
toPrefunctor 
g: β → γ
g :=
  
rfl: ∀ {α : Sort ?u.2275} {a : α}, a = a
rfl
#align quiver.single_obj.to_prefunctor_comp 
Quiver.SingleObj.toPrefunctor_comp: ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_2} (f : α → β) (g : β → γ),
  ↑toPrefunctor (g ∘ f) = ↑toPrefunctor f ⋙q ↑toPrefunctor g
Quiver.SingleObj.toPrefunctor_comp

@[simp]
theorem 
toPrefunctor_symm_comp: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : SingleObj α ⥤q SingleObj β) (g : SingleObj β ⥤q SingleObj γ),
  ↑toPrefunctor.symm (f ⋙q g) = ↑toPrefunctor.symm g ∘ ↑toPrefunctor.symm f
toPrefunctor_symm_comp (
f: SingleObj α ⥤q SingleObj β
f : 
SingleObj: Type ?u.2329 → Type
SingleObj 
α: Type ?u.2316
α ⥤q 
SingleObj: Type ?u.2331 → Type
SingleObj 
β: Type ?u.2319
β) (
g: SingleObj β ⥤q SingleObj γ
g : 
SingleObj: Type ?u.2353 → Type
SingleObj 
β: Type ?u.2319
β ⥤q 
SingleObj: Type ?u.2355 → Type
SingleObj 
γ: Type ?u.2322
γ) :
    
toPrefunctor: {α : Type ?u.2373} → {β : Type ?u.2372} → (α → β) ≃ SingleObj α ⥤q SingleObj β
toPrefunctor.
symm: {α : Sort ?u.2377} → {β : Sort ?u.2376} → α ≃ β → β ≃ α
symm (
f: SingleObj α ⥤q SingleObj β
f ⋙q 
g: SingleObj β ⥤q SingleObj γ
g) = 
toPrefunctor: {α : Type ?u.2571} → {β : Type ?u.2570} → (α → β) ≃ SingleObj α ⥤q SingleObj β
toPrefunctor.
symm: {α : Sort ?u.2575} → {β : Sort ?u.2574} → α ≃ β → β ≃ α
symm 
g: SingleObj β ⥤q SingleObj γ
g ∘ 
toPrefunctor: {α : Type ?u.2674} → {β : Type ?u.2673} → (α → β) ≃ SingleObj α ⥤q SingleObj β
toPrefunctor.
symm: {α : Sort ?u.2678} → {β : Sort ?u.2677} → α ≃ β → β ≃ α
symm 
f: SingleObj α ⥤q SingleObj β
f := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type u_2

γ: Type u_3

f: SingleObj α ⥤q SingleObj β

g: SingleObj β ⥤q SingleObj γ

↑toPrefunctor.symm (f ⋙q g) = ↑toPrefunctor.symm g ∘ ↑toPrefunctor.symm fsimp only [
Equiv.symm_apply_eq: ∀ {α : Sort ?u.2800} {β : Sort ?u.2801} (e : α ≃ β) {x : β} {y : (fun x => α) x}, ↑e.symm x = y ↔ x = ↑e y
Equiv.symm_apply_eq, 
toPrefunctor_comp: ∀ {α : Type ?u.2836} {β : Type ?u.2838} {γ : Type ?u.2837} (f : α → β) (g : β → γ),
  ↑toPrefunctor (g ∘ f) = ↑toPrefunctor f ⋙q ↑toPrefunctor g
toPrefunctor_comp, 
Equiv.apply_symm_apply: ∀ {α : Sort ?u.2876} {β : Sort ?u.2875} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = x
Equiv.apply_symm_apply]
Goals accomplished! 🐙
#align quiver.single_obj.to_prefunctor_symm_comp 
Quiver.SingleObj.toPrefunctor_symm_comp: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : SingleObj α ⥤q SingleObj β) (g : SingleObj β ⥤q SingleObj γ),
  ↑toPrefunctor.symm (f ⋙q g) = ↑toPrefunctor.symm g ∘ ↑toPrefunctor.symm f
Quiver.SingleObj.toPrefunctor_symm_comp

/-- Auxiliary definition for `quiver.SingleObj.pathEquivList`.
Converts a path in the quiver `single_obj α` into a list of elements of type `a`.
-/
def 
pathToList: {x : SingleObj α} → Path (star α) x → List α
pathToList : ∀ {
x: SingleObj α
x : 
SingleObj: Type ?u.3397 → Type
SingleObj 
α: Type ?u.3387
α}, 
Path: {V : Type ?u.3401} → [inst : Quiver V] → V → V → Sort (max(?u.3401+1)?u.3402)
Path (
star: (α : Type ?u.3420) → SingleObj α
star 
α: Type ?u.3387
α) 
x: SingleObj α
x → 
List: Type ?u.3430 → Type ?u.3430
List 
α: Type ?u.3387
α
  | _, 
Path.nil: {V : Type ?u.3440} → [inst : Quiver V] → {a : V} → Path a a
Path.nil => 
[]: List ?m.3485
[]
  | _, 
Path.cons: {V : Type ?u.3487} → [inst : Quiver V] → {a b c : V} → Path a b → (b ⟶ c) → Path a c
Path.cons 
p: Path (star α) b✝
p 
a: b✝ ⟶ x✝
a => 
a: b✝ ⟶ x✝
a :: 
pathToList: {x : SingleObj α} → Path (star α) x → List α
pathToList 
p: Path (star α) b✝
p
#align quiver.single_obj.path_to_list 
Quiver.SingleObj.pathToList: {α : Type u_1} → {x : SingleObj α} → Path (star α) x → List α
Quiver.SingleObj.pathToList

/-- Auxiliary definition for `quiver.SingleObj.pathEquivList`.
Converts a list of elements of type `α` into a path in the quiver `SingleObj α`.
-/
@[simp]
def 
listToPath: List α → Path (star α) (star α)
listToPath : 
List: Type ?u.4168 → Type ?u.4168
List 
α: Type ?u.4158
α → 
Path: {V : Type ?u.4170} → [inst : Quiver V] → V → V → Sort (max(?u.4170+1)?u.4171)
Path (
star: (α : Type ?u.4189) → SingleObj α
star 
α: Type ?u.4158
α) (
star: (α : Type ?u.4191) → SingleObj α
star 
α: Type ?u.4158
α)
  | [] => 
Path.nil: {V : Type ?u.4213} → [inst : Quiver V] → {a : V} → Path a a
Path.nil
  | 
a: α
a :: 
l: List α
l => (
listToPath: List α → Path (star α) (star α)
listToPath 
l: List α
l).
cons: {V : Type ?u.4262} → [inst : Quiver V] → {a b c : V} → Path a b → (b ⟶ c) → Path a c
cons 
a: α
a
#align quiver.single_obj.list_to_path 
Quiver.SingleObj.listToPath: {α : Type u_1} → List α → Path (star α) (star α)
Quiver.SingleObj.listToPath

theorem 
listToPath_pathToList: ∀ {x : SingleObj α} (p : Path (star α) x),
  listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : x = star α) p
listToPath_pathToList {
x: SingleObj α
x : 
SingleObj: Type ?u.4811 → Type
SingleObj 
α: Type ?u.4802
α} (
p: Path (star α) x
p : 
Path: {V : Type ?u.4814} → [inst : Quiver V] → V → V → Sort (max(?u.4814+1)?u.4815)
Path (
star: (α : Type ?u.4833) → SingleObj α
star 
α: Type ?u.4802
α) 
x: SingleObj α
x) :
    
listToPath: {α : Type ?u.4845} → List α → Path (star α) (star α)
listToPath (
pathToList: {α : Type ?u.4847} → {x : SingleObj α} → Path (star α) x → List α
pathToList 
p: Path (star α) x
p) = 
p: Path (star α) x
p.
cast: {U : Type ?u.4862} → [inst : Quiver U] → {u v u' v' : U} → u = u' → v = v' → Path u v → Path u' v'
cast 
rfl: ∀ {α : Sort ?u.4879} {a : α}, a = a
rfl 
ext: ∀ {α : Type ?u.4885} {x y : SingleObj α}, x = y
ext := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x: SingleObj α

p: Path (star α) x

listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : x = star α) pinduction' 
p: Path (star α) x
p with 
y: ?m.4962
y 
z: ?m.4962
z 
p: Path ?m.4964 y
p 
a: y ⟶ z
a 
ih: ?m.4965 y p
ih
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x: SingleObj α

nil
listToPath (pathToList Path.nil) = Path.cast (_ : star α = star α) (_ : star α = star α) Path.nil
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x, y, z: SingleObj α

p: Path (star α) y

a: y ⟶ z

ih: listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : y = star α) p

cons
listToPath (pathToList (Path.cons p a)) = Path.cast (_ : star α = star α) (_ : z = star α) (Path.cons p a)
  
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x: SingleObj α

p: Path (star α) x

listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : x = star α) p·
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x: SingleObj α

nil
listToPath (pathToList Path.nil) = Path.cast (_ : star α = star α) (_ : star α = star α) Path.nil 
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x: SingleObj α

nil
listToPath (pathToList Path.nil) = Path.cast (_ : star α = star α) (_ : star α = star α) Path.nil
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x, y, z: SingleObj α

p: Path (star α) y

a: y ⟶ z

ih: listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : y = star α) p

cons
listToPath (pathToList (Path.cons p a)) = Path.cast (_ : star α = star α) (_ : z = star α) (Path.cons p a)rfl
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x: SingleObj α

p: Path (star α) x

listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : x = star α) p·
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x, y, z: SingleObj α

p: Path (star α) y

a: y ⟶ z

ih: listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : y = star α) p

cons
listToPath (pathToList (Path.cons p a)) = Path.cast (_ : star α = star α) (_ : z = star α) (Path.cons p a) 
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x, y, z: SingleObj α

p: Path (star α) y

a: y ⟶ z

ih: listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : y = star α) p

cons
listToPath (pathToList (Path.cons p a)) = Path.cast (_ : star α = star α) (_ : z = star α) (Path.cons p a)dsimp at *
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x, y, z: SingleObj α

p: Path (star α) y

a: y ⟶ z

ih: listToPath (pathToList p) = p

cons
Path.cons (listToPath (pathToList p)) a = Path.cons p a;
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x, y, z: SingleObj α

p: Path (star α) y

a: y ⟶ z

ih: listToPath (pathToList p) = p

cons
Path.cons (listToPath (pathToList p)) a = Path.cons p a 
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x, y, z: SingleObj α

p: Path (star α) y

a: y ⟶ z

ih: listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : y = star α) p

cons
listToPath (pathToList (Path.cons p a)) = Path.cast (_ : star α = star α) (_ : z = star α) (Path.cons p a)rw [
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x, y, z: SingleObj α

p: Path (star α) y

a: y ⟶ z

ih: listToPath (pathToList p) = p

cons
Path.cons (listToPath (pathToList p)) a = Path.cons p a
ih: listToPath (pathToList p) = p
ih
α: Type u_1

β: Type ?u.4805

γ: Type ?u.4808

x, y, z: SingleObj α

p: Path (star α) y

a: y ⟶ z

ih: listToPath (pathToList p) = p

cons
Path.cons p a = Path.cons p a]
Goals accomplished! 🐙
#align quiver.single_obj.path_to_list_to_path 
Quiver.SingleObj.listToPath_pathToList: ∀ {α : Type u_1} {x : SingleObj α} (p : Path (star α) x),
  listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : x = star α) p
Quiver.SingleObj.listToPath_pathToList

theorem 
pathToList_listToPath: ∀ (l : List α), pathToList (listToPath l) = l
pathToList_listToPath (
l: List α
l : 
List: Type ?u.5114 → Type ?u.5114
List 
α: Type ?u.5105
α) : 
pathToList: {α : Type ?u.5118} → {x : SingleObj α} → Path (star α) x → List α
pathToList (
listToPath: {α : Type ?u.5121} → List α → Path (star α) (star α)
listToPath 
l: List α
l) = 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

l: List α

pathToList (listToPath l) = linduction' 
l: List α
l with 
a: ?m.5159
a 
l: List ?m.5159
l 
ih: ?m.5160 l
ih
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

nil
pathToList (listToPath []) = []
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

a: α

l: List α

ih: pathToList (listToPath l) = l

cons
pathToList (listToPath (a :: l)) = a :: l
  
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

l: List α

pathToList (listToPath l) = l·
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

nil
pathToList (listToPath []) = [] 
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

nil
pathToList (listToPath []) = []
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

a: α

l: List α

ih: pathToList (listToPath l) = l

cons
pathToList (listToPath (a :: l)) = a :: lrfl
Goals accomplished! 🐙
  
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

l: List α

pathToList (listToPath l) = l·
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

a: α

l: List α

ih: pathToList (listToPath l) = l

cons
pathToList (listToPath (a :: l)) = a :: l 
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

a: α

l: List α

ih: pathToList (listToPath l) = l

cons
pathToList (listToPath (a :: l)) = a :: lchange 
a: ?m.5159
a :: 
pathToList: {α : Type ?u.5204} → {x : SingleObj α} → Path (star α) x → List α
pathToList (
listToPath: {α : Type ?u.5207} → List α → Path (star α) (star α)
listToPath 
l: List ?m.5159
l) = 
a: ?m.5159
a :: 
l: List ?m.5159
l
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

a: α

l: List α

ih: pathToList (listToPath l) = l

cons
a :: pathToList (listToPath l) = a :: l;
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

a: α

l: List α

ih: pathToList (listToPath l) = l

cons
a :: pathToList (listToPath l) = a :: l 
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

a: α

l: List α

ih: pathToList (listToPath l) = l

cons
pathToList (listToPath (a :: l)) = a :: lrw [
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

a: α

l: List α

ih: pathToList (listToPath l) = l

cons
a :: pathToList (listToPath l) = a :: l
ih: ?m.5160 l
ih
α: Type u_1

β: Type ?u.5108

γ: Type ?u.5111

a: α

l: List α

ih: pathToList (listToPath l) = l

cons
a :: l = a :: l]
Goals accomplished! 🐙
#align quiver.single_obj.list_to_path_to_list 
Quiver.SingleObj.pathToList_listToPath: ∀ {α : Type u_1} (l : List α), pathToList (listToPath l) = l
Quiver.SingleObj.pathToList_listToPath

/-- Paths in `SingleObj α` quiver correspond to lists of elements of type `α`. -/
def 
pathEquivList: {α : Type u_1} → Path (star α) (star α) ≃ List α
pathEquivList : 
Path: {V : Type ?u.5284} → [inst : Quiver V] → V → V → Sort (max(?u.5284+1)?u.5285)
Path (
star: (α : Type ?u.5303) → SingleObj α
star 
α: Type ?u.5273
α) (
star: (α : Type ?u.5305) → SingleObj α
star 
α: Type ?u.5273
α) ≃ 
List: Type ?u.5313 → Type ?u.5313
List 
α: Type ?u.5273
α :=
  ⟨
pathToList: {α : Type ?u.5327} → {x : SingleObj α} → Path (star α) x → List α
pathToList, 
listToPath: {α : Type ?u.5340} → List α → Path (star α) (star α)
listToPath, fun 
p: ?m.5346
p => 
listToPath_pathToList: ∀ {α : Type ?u.5348} {x : SingleObj α} (p : Path (star α) x),
  listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : x = star α) p
listToPath_pathToList 
p: ?m.5346
p, 
pathToList_listToPath: ∀ {α : Type ?u.5361} (l : List α), pathToList (listToPath l) = l
pathToList_listToPath⟩
#align quiver.single_obj.path_equiv_list 
Quiver.SingleObj.pathEquivList: {α : Type u_1} → Path (star α) (star α) ≃ List α
Quiver.SingleObj.pathEquivList

@[simp]
theorem 
pathEquivList_nil: ∀ {α : Type u_1}, ↑pathEquivList Path.nil = []
pathEquivList_nil : 
pathEquivList: {α : Type ?u.5419} → Path (star α) (star α) ≃ List α
pathEquivList 
Path.nil: {V : Type ?u.5482} → [inst : Quiver V] → {a : V} → Path a a
Path.nil = (
[]: List ?m.5515
[] : 
List: Type ?u.5513 → Type ?u.5513
List 
α: Type ?u.5409
α) :=
  
rfl: ∀ {α : Sort ?u.5550} {a : α}, a = a
rfl
#align quiver.single_obj.path_equiv_list_nil 
Quiver.SingleObj.pathEquivList_nil: ∀ {α : Type u_1}, ↑pathEquivList Path.nil = []
Quiver.SingleObj.pathEquivList_nil

@[simp]
theorem 
pathEquivList_cons: ∀ {α : Type u_1} (p : Path (star α) (star α)) (a : star α ⟶ star α), ↑pathEquivList (Path.cons p a) = a :: pathToList p
pathEquivList_cons (
p: Path (star α) (star α)
p : 
Path: {V : Type ?u.5604} → [inst : Quiver V] → V → V → Sort (max(?u.5604+1)?u.5605)
Path (
star: (α : Type ?u.5623) → SingleObj α
star 
α: Type ?u.5595
α) (
star: (α : Type ?u.5625) → SingleObj α
star 
α: Type ?u.5595
α)) (
a: star α ⟶ star α
a : 
star: (α : Type ?u.5654) → SingleObj α
star 
α: Type ?u.5595
α ⟶ 
star: (α : Type ?u.5655) → SingleObj α
star 
α: Type ?u.5595
α) :
    
pathEquivList: {α : Type ?u.5664} → Path (star α) (star α) ≃ List α
pathEquivList (
Path.cons: {V : Type ?u.5727} → [inst : Quiver V] → {a b c : V} → Path a b → (b ⟶ c) → Path a c
Path.cons 
p: Path (star α) (star α)
p 
a: star α ⟶ star α
a) = 
a: star α ⟶ star α
a :: 
pathToList: {α : Type ?u.5766} → {x : SingleObj α} → Path (star α) x → List α
pathToList 
p: Path (star α) (star α)
p :=
  
rfl: ∀ {α : Sort ?u.5776} {a : α}, a = a
rfl
#align quiver.single_obj.path_equiv_list_cons 
Quiver.SingleObj.pathEquivList_cons: ∀ {α : Type u_1} (p : Path (star α) (star α)) (a : star α ⟶ star α), ↑pathEquivList (Path.cons p a) = a :: pathToList p
Quiver.SingleObj.pathEquivList_cons

@[simp]
theorem 
pathEquivList_symm_nil: ∀ {α : Type u_1}, ↑pathEquivList.symm [] = Path.nil
pathEquivList_symm_nil : 
pathEquivList: {α : Type ?u.5847} → Path (star α) (star α) ≃ List α
pathEquivList.
symm: {α : Sort ?u.5850} → {β : Sort ?u.5849} → α ≃ β → β ≃ α
symm (
[]: List ?m.5922
[] : 
List: Type ?u.5920 → Type ?u.5920
List 
α: Type ?u.5837
α) = 
Path.nil: {V : Type ?u.5924} → [inst : Quiver V] → {a : V} → Path a a
Path.nil :=
  
rfl: ∀ {α : Sort ?u.6010} {a : α}, a = a
rfl
#align quiver.single_obj.path_equiv_list_symm_nil 
Quiver.SingleObj.pathEquivList_symm_nil: ∀ {α : Type u_1}, ↑pathEquivList.symm [] = Path.nil
Quiver.SingleObj.pathEquivList_symm_nil

@[simp]
theorem 
pathEquivList_symm_cons: ∀ {α : Type u_1} (l : List α) (a : α), ↑pathEquivList.symm (a :: l) = Path.cons (↑pathEquivList.symm l) a
pathEquivList_symm_cons (
l: List α
l : 
List: Type ?u.6063 → Type ?u.6063
List 
α: Type ?u.6054
α) (
a: α
a : 
α: Type ?u.6054
α) :
    
pathEquivList: {α : Type ?u.6069} → Path (star α) (star α) ≃ List α
pathEquivList.
symm: {α : Sort ?u.6072} → {β : Sort ?u.6071} → α ≃ β → β ≃ α
symm (
a: α
a :: 
l: List α
l) = 
Path.cons: {V : Type ?u.6145} → [inst : Quiver V] → {a b c : V} → Path a b → (b ⟶ c) → Path a c
Path.cons (
pathEquivList: {α : Type ?u.6152} → Path (star α) (star α) ≃ List α
pathEquivList.
symm: {α : Sort ?u.6155} → {β : Sort ?u.6154} → α ≃ β → β ≃ α
symm 
l: List α
l) 
a: α
a :=
  
rfl: ∀ {α : Sort ?u.6272} {a : α}, a = a
rfl
#align quiver.single_obj.path_equiv_list_symm_cons 
Quiver.SingleObj.pathEquivList_symm_cons: ∀ {α : Type u_1} (l : List α) (a : α), ↑pathEquivList.symm (a :: l) = Path.cons (↑pathEquivList.symm l) a
Quiver.SingleObj.pathEquivList_symm_cons

end SingleObj

end Quiver