Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2021 David WΓ€rn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David WΓ€rn, Scott Morrison
Ported by: Scott Morrison

! This file was ported from Lean 3 source module combinatorics.quiver.basic
! leanprover-community/mathlib commit 56adee5b5eef9e734d82272918300fca4f3e7cef
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Opposite

/-!
# Quivers

This module defines quivers. A quiver on a type `V` of vertices assigns to every
pair `a b : V` of vertices a type `a ⟢ b` of arrows from `a` to `b`. This
is a very permissive notion of directed graph.

## Implementation notes

Currently `Quiver` is defined with `arrow : V β†’ V β†’ Sort v`.
This is different from the category theory setup,
where we insist that morphisms live in some `Type`.
There's some balance here: it's nice to allow `Prop` to ensure there are no multiple arrows,
but it is also results in error-prone universe signatures when constraints require a `Type`.
-/


open Opposite

-- We use the same universe order as in category theory.
-- See note [CategoryTheory universes]
universe v v₁ vβ‚‚ u u₁ uβ‚‚

/-- A quiver `G` on a type `V` of vertices assigns to every pair `a b : V` of vertices
a type `a ⟢ b` of arrows from `a` to `b`.

For graphs with no repeated edges, one can use `Quiver.{0} V`, which ensures
`a ⟢ b : Prop`. For multigraphs, one can use `Quiver.{v+1} V`, which ensures
`a ⟢ b : Type v`.

Because `Category` will later extend this class, we call the field `hom`.
Except when constructing instances, you should rarely see this, and use the `⟢` notation instead.
-/
class 
Quiver: {V : Type u} β†’ (V β†’ V β†’ Sort v) β†’ Quiver V
Quiver (
V: Type u
V : 
Type u: Type (u+1)
Type u) where
  /-- The type of edges/arrows/morphisms between a given source and target. -/
  
Hom: {V : Type u} β†’ [self : Quiver V] β†’ V β†’ V β†’ Sort v
Hom : 
V: Type u
V β†’ 
V: Type u
V β†’ 
Sort v: Type v
Sort
Sort v: Type v
 v
#align quiver 
Quiver: Type u β†’ Type (maxuv)
Quiver
#align quiver.hom 
Quiver.Hom: {V : Type u} β†’ [self : Quiver V] β†’ V β†’ V β†’ Sort v
Quiver.Hom

/--
Notation for the type of edges/arrows/morphisms between a given source and target
in a quiver or category.
-/
infixr:10 " ⟢ " => 
Quiver.Hom: {V : Type u} β†’ [self : Quiver V] β†’ V β†’ V β†’ Sort v
Quiver.Hom

/-- A morphism of quivers. As we will later have categorical functors extend this structure,
we call it a `Prefunctor`. -/
structure 
Prefunctor: {V : Type u₁} β†’
  [inst : Quiver V] β†’
    {W : Type uβ‚‚} β†’ [inst_1 : Quiver W] β†’ (obj : V β†’ W) β†’ ({X Y : V} β†’ (X ⟢ Y) β†’ (obj X ⟢ obj Y)) β†’ Prefunctor V W
Prefunctor (
V: Type u₁
V : 
Type u₁: Type (u₁+1)
Type u₁) [
Quiver: Type ?u.7832 β†’ Type (max?u.7832v₁)
Quiver.{v₁} 
V: Type u₁
V] (
W: Type uβ‚‚
W : 
Type uβ‚‚: Type (uβ‚‚+1)
Type uβ‚‚) [
Quiver: Type ?u.7837 β†’ Type (max?u.7837vβ‚‚)
Quiver.{vβ‚‚} 
W: Type uβ‚‚
W] where
  /-- The action of a (pre)functor on vertices/objects. -/
  
obj: {V : Type u₁} β†’ [inst : Quiver V] β†’ {W : Type uβ‚‚} β†’ [inst_1 : Quiver W] β†’ Prefunctor V W β†’ V β†’ W
obj : 
V: Type u₁
V β†’ 
W: Type uβ‚‚
W
  /-- The action of a (pre)functor on edges/arrows/morphisms. -/
  
map: {V : Type u₁} β†’
  [inst : Quiver V] β†’
    {W : Type uβ‚‚} β†’
      [inst_1 : Quiver W] β†’
        (self : Prefunctor V W) β†’ {X Y : V} β†’ (X ⟢ Y) β†’ (Prefunctor.obj self X ⟢ Prefunctor.obj self Y)
map : βˆ€ {
X: V
X 
Y: V
Y : 
V: Type u₁
V}, (
X: V
X ⟢ 
Y: V
Y) β†’ (
obj: V β†’ W
obj 
X: V
X ⟢ 
obj: V β†’ W
obj 
Y: V
Y)
#align prefunctor 
Prefunctor: (V : Type u₁) β†’ [inst : Quiver V] β†’ (W : Type uβ‚‚) β†’ [inst : Quiver W] β†’ Sort (max(max(max(u₁+1)(uβ‚‚+1))v₁)vβ‚‚)
Prefunctor

pp_extended_field_notation 
Prefunctor.obj: {V : Type u₁} β†’ [inst : Quiver V] β†’ {W : Type uβ‚‚} β†’ [inst_1 : Quiver W] β†’ Prefunctor V W β†’ V β†’ W
Prefunctor.obj
pp_extended_field_notation 
Prefunctor.map: {V : Type u₁} β†’
  [inst : Quiver V] β†’
    {W : Type uβ‚‚} β†’ [inst_1 : Quiver W] β†’ (self : Prefunctor V W) β†’ {X Y : V} β†’ (X ⟢ Y) β†’ (self.obj X ⟢ self.obj Y)
Prefunctor.map

namespace Prefunctor

@[ext]
theorem 
ext: βˆ€ {V : Type u} [inst : Quiver V] {W : Type uβ‚‚} [inst_1 : Quiver W] {F G : Prefunctor V W}
  (h_obj : βˆ€ (X : V), F.obj X = G.obj X),
  (βˆ€ (X Y : V) (f : X ⟢ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))) β†’
    F = G
ext {
V: Type u
V : 
Type u: Type (u+1)
Type u} [
Quiver: Type ?u.22889 β†’ Type (max?u.22889v₁)
Quiver.{v₁} 
V: Type u
V] {
W: Type uβ‚‚
W : 
Type uβ‚‚: Type (uβ‚‚+1)
Type uβ‚‚} [
Quiver: Type ?u.22894 β†’ Type (max?u.22894vβ‚‚)
Quiver.{vβ‚‚} 
W: Type uβ‚‚
W] {
F: Prefunctor V W
F 
G: Prefunctor V W
G : 
Prefunctor: (V : Type ?u.22914) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.22913) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.22914+1)(?u.22913+1))?u.22916)?u.22915)
Prefunctor 
V: Type u
V 
W: Type uβ‚‚
W}
    (
h_obj: βˆ€ (X : V), F.obj X = G.obj X
h_obj : βˆ€ 
X: ?m.22928
X, 
F: Prefunctor V W
F.
obj: {V : Type ?u.22933} β†’ [inst : Quiver V] β†’ {W : Type ?u.22932} β†’ [inst_1 : Quiver W] β†’ Prefunctor V W β†’ V β†’ W
obj 
X: ?m.22928
X = 
G: Prefunctor V W
G.
obj: {V : Type ?u.22951} β†’ [inst : Quiver V] β†’ {W : Type ?u.22950} β†’ [inst_1 : Quiver W] β†’ Prefunctor V W β†’ V β†’ W
obj 
X: ?m.22928
X)
    (
h_map: βˆ€ (X Y : V) (f : X ⟢ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))
h_map : βˆ€ (
X: V
X 
Y: V
Y : 
V: Type u
V) (
f: X ⟢ Y
f : 
X: V
X ⟢ 
Y: V
Y),
      
F: Prefunctor V W
F.
map: {V : Type ?u.22981} β†’
  [inst : Quiver V] β†’
    {W : Type ?u.22980} β†’
      [inst_1 : Quiver W] β†’ (self : Prefunctor V W) β†’ {X Y : V} β†’ (X ⟢ Y) β†’ (self.obj X ⟢ self.obj Y)
map 
f: X ⟢ Y
f = 
Eq.recOn: {Ξ± : Sort ?u.23032} β†’
  {a : Ξ±} β†’
    {motive : (a_1 : Ξ±) β†’ a = a_1 β†’ Sort ?u.23033} β†’ {a_1 : Ξ±} β†’ (t : a = a_1) β†’ motive a (_ : a = a) β†’ motive a_1 t
Eq.recOn (
h_obj: βˆ€ (X : V), F.obj X = G.obj X
h_obj 
Y: V
Y).
symm: βˆ€ {Ξ± : Sort ?u.23058} {a b : Ξ±}, a = b β†’ b = a
symm (
Eq.recOn: {Ξ± : Sort ?u.23078} β†’
  {a : Ξ±} β†’
    {motive : (a_1 : Ξ±) β†’ a = a_1 β†’ Sort ?u.23079} β†’ {a_1 : Ξ±} β†’ (t : a = a_1) β†’ motive a (_ : a = a) β†’ motive a_1 t
Eq.recOn (
h_obj: βˆ€ (X : V), F.obj X = G.obj X
h_obj 
X: V
X).
symm: βˆ€ {Ξ± : Sort ?u.23104} {a b : Ξ±}, a = b β†’ b = a
symm (
G: Prefunctor V W
G.
map: {V : Type ?u.23121} β†’
  [inst : Quiver V] β†’
    {W : Type ?u.23120} β†’
      [inst_1 : Quiver W] β†’ (self : Prefunctor V W) β†’ {X Y : V} β†’ (X ⟢ Y) β†’ (self.obj X ⟢ self.obj Y)
map 
f: X ⟢ Y
f))) : 
F: Prefunctor V W
F = 
G: Prefunctor V W
G := 
Goals accomplished! πŸ™
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: βˆ€ (X : V), F.obj X = G.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))

F = G
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

G: Prefunctor V W

F_obj: V β†’ W

map✝: {X Y : V} β†’ (X ⟢ Y) β†’ (F_obj X ⟢ F_obj Y)

h_obj: βˆ€ (X : V), { obj := F_obj, map := map✝ }.obj X = G.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y),
  { obj := F_obj, map := map✝ }.map f =     Eq.recOn (_ : G.obj Y = { obj := F_obj, map := map✝ }.obj Y)
      (Eq.recOn (_ : G.obj X = { obj := F_obj, map := map✝ }.obj X) (G.map f))

mk
{ obj := F_obj, map := map✝ } = G
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: βˆ€ (X : V), F.obj X = G.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))

F = G
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F_obj: V β†’ W

map✝¹: {X Y : V} β†’ (X ⟢ Y) β†’ (F_obj X ⟢ F_obj Y)

G_obj: V β†’ W

map✝: {X Y : V} β†’ (X ⟢ Y) β†’ (G_obj X ⟢ G_obj Y)

h_obj: βˆ€ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y),
  { obj := F_obj, map := map✝¹ }.map f =     Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
      (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
        ({ obj := G_obj, map := map✝ }.map f))

mk.mk
{ obj := F_obj, map := map✝¹ } = { obj := G_obj, map := map✝ }
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: βˆ€ (X : V), F.obj X = G.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))

F = G
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F_obj: V β†’ W

map✝¹: {X Y : V} β†’ (X ⟢ Y) β†’ (F_obj X ⟢ F_obj Y)

G_obj: V β†’ W

map✝: {X Y : V} β†’ (X ⟢ Y) β†’ (G_obj X ⟢ G_obj Y)

h_obj: βˆ€ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y),
  { obj := F_obj, map := map✝¹ }.map f =     Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
      (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
        ({ obj := G_obj, map := map✝ }.map f))

mk.mk
{ obj := F_obj, map := map✝¹ } = { obj := G_obj, map := map✝ }
Goals accomplished! πŸ™
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F_obj: V β†’ W

map✝¹: {X Y : V} β†’ (X ⟢ Y) β†’ (F_obj X ⟢ F_obj Y)

G_obj: V β†’ W

map✝: {X Y : V} β†’ (X ⟢ Y) β†’ (G_obj X ⟢ G_obj Y)

h_obj: βˆ€ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y),
  { obj := F_obj, map := map✝¹ }.map f =     Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
      (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
        ({ obj := G_obj, map := map✝ }.map f))

F_obj = G_obj
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F_obj: V β†’ W

map✝¹: {X Y : V} β†’ (X ⟢ Y) β†’ (F_obj X ⟢ F_obj Y)

G_obj: V β†’ W

map✝: {X Y : V} β†’ (X ⟢ Y) β†’ (G_obj X ⟢ G_obj Y)

h_obj: βˆ€ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y),
  { obj := F_obj, map := map✝¹ }.map f =     Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
      (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
        ({ obj := G_obj, map := map✝ }.map f))

X: V

h
F_obj X = G_obj X
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F_obj: V β†’ W

map✝¹: {X Y : V} β†’ (X ⟢ Y) β†’ (F_obj X ⟢ F_obj Y)

G_obj: V β†’ W

map✝: {X Y : V} β†’ (X ⟢ Y) β†’ (G_obj X ⟢ G_obj Y)

h_obj: βˆ€ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := G_obj, map := map✝ }.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y),
  { obj := F_obj, map := map✝¹ }.map f =     Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
      (Eq.recOn (_ : { obj := G_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
        ({ obj := G_obj, map := map✝ }.map f))

F_obj = G_obj
Goals accomplished! πŸ™
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: βˆ€ (X : V), F.obj X = G.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))

F = G
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F_obj: V β†’ W

map✝¹, map✝: {X Y : V} β†’ (X ⟢ Y) β†’ (F_obj X ⟢ F_obj Y)

h_obj: βˆ€ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y),
  { obj := F_obj, map := map✝¹ }.map f =     Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
      (Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
        ({ obj := F_obj, map := map✝ }.map f))

mk.mk.e_map
map✝¹ = map✝
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: βˆ€ (X : V), F.obj X = G.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))

F = G
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F_obj: V β†’ W

map✝¹, map✝: {X Y : V} β†’ (X ⟢ Y) β†’ (F_obj X ⟢ F_obj Y)

h_obj: βˆ€ (X : V), { obj := F_obj, map := map✝¹ }.obj X = { obj := F_obj, map := map✝ }.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y),
  { obj := F_obj, map := map✝¹ }.map f =     Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj Y = { obj := F_obj, map := map✝¹ }.obj Y)
      (Eq.recOn (_ : { obj := F_obj, map := map✝ }.obj X = { obj := F_obj, map := map✝¹ }.obj X)
        ({ obj := F_obj, map := map✝ }.map f))

X, Y: V

f: X ⟢ Y

mk.mk.e_map.h.h.h
map✝¹ f = map✝ f
V: Type u

inst✝¹: Quiver V

W: Type uβ‚‚

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: βˆ€ (X : V), F.obj X = G.obj X

h_map: βˆ€ (X Y : V) (f : X ⟢ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))

F = G
Goals accomplished! πŸ™

#align prefunctor.ext 
Prefunctor.ext: βˆ€ {V : Type u} [inst : Quiver V] {W : Type uβ‚‚} [inst_1 : Quiver W] {F G : Prefunctor V W}
  (h_obj : βˆ€ (X : V), F.obj X = G.obj X),
  (βˆ€ (X Y : V) (f : X ⟢ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))) β†’
    F = G
Prefunctor.ext

/-- The identity morphism between quivers. -/
@[
simps: βˆ€ (V : Type u_1) [inst : Quiver V] {X Y : V} (f : X ⟢ Y), (id V).map f = f
simps]
def 
id: (V : Type u_1) β†’ [inst : Quiver V] β†’ Prefunctor V V
id (
V: Type ?u.23954
V : 
Type _: Type (?u.23954+1)
Type _) [
Quiver: Type ?u.23957 β†’ Type (max?u.23957?u.23958)
Quiver 
V: Type ?u.23954
V] : 
Prefunctor: (V : Type ?u.23962) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.23961) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.23962+1)(?u.23961+1))?u.23964)?u.23963)
Prefunctor 
V: Type ?u.23954
V 
V: Type ?u.23954
V where
  obj := fun 
X: ?m.23993
X => 
X: ?m.23993
X
  map 
f: ?m.24000
f := 
f: ?m.24000
f
#align prefunctor.id 
Prefunctor.id: (V : Type u_1) β†’ [inst : Quiver V] β†’ Prefunctor V V
Prefunctor.id
#align prefunctor.id_obj 
Prefunctor.id_obj: βˆ€ (V : Type u_1) [inst : Quiver V] (X : V), (id V).obj X = X
Prefunctor.id_obj
#align prefunctor.id_map 
Prefunctor.id_map: βˆ€ (V : Type u_1) [inst : Quiver V] {X Y : V} (f : X ⟢ Y), (id V).map f = f
Prefunctor.id_map


instance: (V : Type u_1) β†’ [inst : Quiver V] β†’ Inhabited (Prefunctor V V)
instance (
V: Type ?u.24133
V : 
Type _: Type (?u.24133+1)
Type _) [
Quiver: Type ?u.24136 β†’ Type (max?u.24136?u.24137)
Quiver 
V: Type ?u.24133
V] : 
Inhabited: Sort ?u.24140 β†’ Sort (max1?u.24140)
Inhabited (
Prefunctor: (V : Type ?u.24142) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.24141) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.24142+1)(?u.24141+1))?u.24144)?u.24143)
Prefunctor 
V: Type ?u.24133
V 
V: Type ?u.24133
V) :=
  ⟨
id: (V : Type ?u.24163) β†’ [inst : Quiver V] β†’ Prefunctor V V
id 
V: Type ?u.24133
V⟩

/-- Composition of morphisms between quivers. -/
@[
simps: βˆ€ {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst_1 : Quiver V] {W : Type u_5} [inst_2 : Quiver W]
  (F : Prefunctor U V) (G : Prefunctor V W) (X : U), (comp F G).obj X = G.obj (F.obj X)
simps]
def 
comp: {U : Type ?u.24207} β†’
  [inst : Quiver U] β†’
    {V : Type ?u.24214} β†’
      [inst_1 : Quiver V] β†’ {W : Type ?u.24221} β†’ [inst_2 : Quiver W] β†’ Prefunctor U V β†’ Prefunctor V W β†’ Prefunctor U W
comp {
U: Type ?u.24207
U : 
Type _: Type (?u.24207+1)
Type _} [
Quiver: Type ?u.24210 β†’ Type (max?u.24210?u.24211)
Quiver 
U: Type ?u.24207
U] {
V: Type ?u.24214
V : 
Type _: Type (?u.24214+1)
Type _} [
Quiver: Type ?u.24217 β†’ Type (max?u.24217?u.24218)
Quiver 
V: Type ?u.24214
V] {
W: Type ?u.24221
W : 
Type _: Type (?u.24221+1)
Type _} [
Quiver: Type ?u.24224 β†’ Type (max?u.24224?u.24225)
Quiver 
W: Type ?u.24221
W]
    (
F: Prefunctor U V
F : 
Prefunctor: (V : Type ?u.24229) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.24228) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.24229+1)(?u.24228+1))?u.24231)?u.24230)
Prefunctor 
U: Type ?u.24207
U 
V: Type ?u.24214
V) (
G: Prefunctor V W
G : 
Prefunctor: (V : Type ?u.24245) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.24244) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.24245+1)(?u.24244+1))?u.24247)?u.24246)
Prefunctor 
V: Type ?u.24214
V 
W: Type ?u.24221
W) : 
Prefunctor: (V : Type ?u.24260) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.24259) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.24260+1)(?u.24259+1))?u.24262)?u.24261)
Prefunctor 
U: Type ?u.24207
U 
W: Type ?u.24221
W where
  obj 
X: ?m.24298
X := 
G: Prefunctor V W
G.
obj: {V : Type ?u.24301} β†’ [inst : Quiver V] β†’ {W : Type ?u.24300} β†’ [inst_1 : Quiver W] β†’ Prefunctor V W β†’ V β†’ W
obj (
F: Prefunctor U V
F.
obj: {V : Type ?u.24317} β†’ [inst : Quiver V] β†’ {W : Type ?u.24316} β†’ [inst_1 : Quiver W] β†’ Prefunctor V W β†’ V β†’ W
obj 
X: ?m.24298
X)
  map 
f: ?m.24335
f := 
G: Prefunctor V W
G.
map: {V : Type ?u.24338} β†’
  [inst : Quiver V] β†’
    {W : Type ?u.24337} β†’
      [inst_1 : Quiver W] β†’ (self : Prefunctor V W) β†’ {X Y : V} β†’ (X ⟢ Y) β†’ (self.obj X ⟢ self.obj Y)
map (
F: Prefunctor U V
F.
map: {V : Type ?u.24362} β†’
  [inst : Quiver V] β†’
    {W : Type ?u.24361} β†’
      [inst_1 : Quiver W] β†’ (self : Prefunctor V W) β†’ {X Y : V} β†’ (X ⟢ Y) β†’ (self.obj X ⟢ self.obj Y)
map 
f: ?m.24335
f)
#align prefunctor.comp 
Prefunctor.comp: {U : Type u_1} β†’
  [inst : Quiver U] β†’
    {V : Type u_3} β†’
      [inst_1 : Quiver V] β†’ {W : Type u_5} β†’ [inst_2 : Quiver W] β†’ Prefunctor U V β†’ Prefunctor V W β†’ Prefunctor U W
Prefunctor.comp
#align prefunctor.comp_obj 
Prefunctor.comp_obj: βˆ€ {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst_1 : Quiver V] {W : Type u_5} [inst_2 : Quiver W]
  (F : Prefunctor U V) (G : Prefunctor V W) (X : U), (comp F G).obj X = G.obj (F.obj X)
Prefunctor.comp_obj
#align prefunctor.comp_map 
Prefunctor.comp_map: βˆ€ {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst_1 : Quiver V] {W : Type u_5} [inst_2 : Quiver W]
  (F : Prefunctor U V) (G : Prefunctor V W) {X Y : U} (f : X ⟢ Y), (comp F G).map f = G.map (F.map f)
Prefunctor.comp_map

pp_extended_field_notation 
Prefunctor.comp: {U : Type u_1} β†’
  [inst : Quiver U] β†’
    {V : Type u_3} β†’
      [inst_1 : Quiver V] β†’ {W : Type u_5} β†’ [inst_2 : Quiver W] β†’ Prefunctor U V β†’ Prefunctor V W β†’ Prefunctor U W
Prefunctor.comp

@[simp]
theorem 
comp_id: βˆ€ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : Prefunctor U V), F.comp (id V) = F
comp_id {
U: Type ?u.31803
U 
V: Type ?u.31806
V : 
Type _: Type (?u.31806+1)
Type _} [
Quiver: Type ?u.31809 β†’ Type (max?u.31809?u.31810)
Quiver 
U: Type ?u.31803
U] [
Quiver: Type ?u.31813 β†’ Type (max?u.31813?u.31814)
Quiver 
V: Type ?u.31806
V] (
F: Prefunctor U V
F : 
Prefunctor: (V : Type ?u.31818) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.31817) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.31818+1)(?u.31817+1))?u.31820)?u.31819)
Prefunctor 
U: Type ?u.31803
U 
V: Type ?u.31806
V) :
    
F: Prefunctor U V
F.
comp: {U : Type ?u.31839} β†’
  [inst : Quiver U] β†’
    {V : Type ?u.31837} β†’
      [inst_1 : Quiver V] β†’ {W : Type ?u.31835} β†’ [inst_2 : Quiver W] β†’ Prefunctor U V β†’ Prefunctor V W β†’ Prefunctor U W
comp (
id: (V : Type ?u.31861) β†’ [inst : Quiver V] β†’ Prefunctor V V
id 
_: Type ?u.31861
_) = 
F: Prefunctor U V
F := 
rfl: βˆ€ {Ξ± : Sort ?u.31887} {a : Ξ±}, a = a
rfl
#align prefunctor.comp_id 
Prefunctor.comp_id: βˆ€ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : Prefunctor U V), F.comp (id V) = F
Prefunctor.comp_id

@[simp]
theorem 
id_comp: βˆ€ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : Prefunctor U V), (id U).comp F = F
id_comp {
U: Type u_1
U 
V: Type ?u.31930
V : 
Type _: Type (?u.31930+1)
Type _} [
Quiver: Type ?u.31933 β†’ Type (max?u.31933?u.31934)
Quiver 
U: Type ?u.31927
U] [
Quiver: Type ?u.31937 β†’ Type (max?u.31937?u.31938)
Quiver 
V: Type ?u.31930
V] (
F: Prefunctor U V
F : 
Prefunctor: (V : Type ?u.31942) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.31941) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.31942+1)(?u.31941+1))?u.31944)?u.31943)
Prefunctor 
U: Type ?u.31927
U 
V: Type ?u.31930
V) :
    (
id: (V : Type ?u.31959) β†’ [inst : Quiver V] β†’ Prefunctor V V
id 
_: Type ?u.31959
_).
comp: {U : Type ?u.31969} β†’
  [inst : Quiver U] β†’
    {V : Type ?u.31967} β†’
      [inst_1 : Quiver V] β†’ {W : Type ?u.31965} β†’ [inst_2 : Quiver W] β†’ Prefunctor U V β†’ Prefunctor V W β†’ Prefunctor U W
comp 
F: Prefunctor U V
F = 
F: Prefunctor U V
F := 
rfl: βˆ€ {Ξ± : Sort ?u.32011} {a : Ξ±}, a = a
rfl
#align prefunctor.id_comp 
Prefunctor.id_comp: βˆ€ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : Prefunctor U V), (id U).comp F = F
Prefunctor.id_comp

@[simp]
theorem 
comp_assoc: βˆ€ {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [inst : Quiver U] [inst_1 : Quiver V] [inst_2 : Quiver W]
  [inst_3 : Quiver Z] (F : Prefunctor U V) (G : Prefunctor V W) (H : Prefunctor W Z),
  (F.comp G).comp H = F.comp (G.comp H)
comp_assoc {
U: Type ?u.32055
U 
V: Type ?u.32058
V 
W: Type ?u.32061
W 
Z: Type ?u.32064
Z : 
Type _: Type (?u.32055+1)
Type _} [
Quiver: Type ?u.32067 β†’ Type (max?u.32067?u.32068)
Quiver 
U: Type ?u.32055
U] [
Quiver: Type ?u.32071 β†’ Type (max?u.32071?u.32072)
Quiver 
V: Type ?u.32058
V] [
Quiver: Type ?u.32075 β†’ Type (max?u.32075?u.32076)
Quiver 
W: Type ?u.32061
W] [
Quiver: Type ?u.32079 β†’ Type (max?u.32079?u.32080)
Quiver 
Z: Type ?u.32064
Z]
    (
F: Prefunctor U V
F : 
Prefunctor: (V : Type ?u.32084) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.32083) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.32084+1)(?u.32083+1))?u.32086)?u.32085)
Prefunctor 
U: Type ?u.32055
U 
V: Type ?u.32058
V) (
G: Prefunctor V W
G : 
Prefunctor: (V : Type ?u.32100) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.32099) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.32100+1)(?u.32099+1))?u.32102)?u.32101)
Prefunctor 
V: Type ?u.32058
V 
W: Type ?u.32061
W) (
H: Prefunctor W Z
H : 
Prefunctor: (V : Type ?u.32115) β†’
  [inst : Quiver V] β†’
    (W : Type ?u.32114) β†’ [inst : Quiver W] β†’ Sort (max(max(max(?u.32115+1)(?u.32114+1))?u.32117)?u.32116)
Prefunctor 
W: Type ?u.32061
W 
Z: Type ?u.32064
Z) :
    (
F: Prefunctor U V
F.
comp: {U : Type ?u.32135} β†’
  [inst : Quiver U] β†’
    {V : Type ?u.32133} β†’
      [inst_1 : Quiver V] β†’ {W : Type ?u.32131} β†’ [inst_2 : Quiver W] β†’ Prefunctor U V β†’ Prefunctor V W β†’ Prefunctor U W
comp 
G: Prefunctor V W
G).
comp: {U : Type ?u.32176} β†’
  [inst : Quiver U] β†’
    {V : Type ?u.32174} β†’
      [inst_1 : Quiver V] β†’ {W : Type ?u.32172} β†’ [inst_2 : Quiver W] β†’ Prefunctor U V β†’ Prefunctor V W β†’ Prefunctor U W
comp 
H: Prefunctor W Z
H = 
F: Prefunctor U V
F.
comp: {U : Type ?u.32213} β†’
  [inst : Quiver U] β†’
    {V : Type ?u.32211} β†’
      [inst_1 : Quiver V] β†’ {W : Type ?u.32209} β†’ [inst_2 : Quiver W] β†’ Prefunctor U V β†’ Prefunctor V W β†’ Prefunctor U W
comp (
G: Prefunctor V W
G.
comp: {U : Type ?u.32235} β†’
  [inst : Quiver U] β†’
    {V : Type ?u.32233} β†’
      [inst_1 : Quiver V] β†’ {W : Type ?u.32231} β†’ [inst_2 : Quiver W] β†’ Prefunctor U V β†’ Prefunctor V W β†’ Prefunctor U W
comp 
H: Prefunctor W Z
H) :=
  
rfl: βˆ€ {Ξ± : Sort ?u.32285} {a : Ξ±}, a = a
rfl
#align prefunctor.comp_assoc 
Prefunctor.comp_assoc: βˆ€ {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [inst : Quiver U] [inst_1 : Quiver V] [inst_2 : Quiver W]
  [inst_3 : Quiver Z] (F : Prefunctor U V) (G : Prefunctor V W) (H : Prefunctor W Z),
  (F.comp G).comp H = F.comp (G.comp H)
Prefunctor.comp_assoc

/-- Notation for a prefunctor between quivers. -/
infixl:50 " β₯€q " => 
Prefunctor: (V : Type u₁) β†’ [inst : Quiver V] β†’ (W : Type uβ‚‚) β†’ [inst : Quiver W] β†’ Sort (max(max(max(u₁+1)(uβ‚‚+1))v₁)vβ‚‚)
Prefunctor

/-- Notation for composition of prefunctors. -/
infixl:60 " β‹™q " => 
Prefunctor.comp: {U : Type u_1} β†’
  [inst : Quiver U] β†’
    {V : Type u_3} β†’ [inst_1 : Quiver V] β†’ {W : Type u_5} β†’ [inst_2 : Quiver W] β†’ U β₯€q V β†’ V β₯€q W β†’ U β₯€q W
Prefunctor.comp

/-- Notation for the identity prefunctor on a quiver. -/
notation "𝟭q" => 
id: (V : Type u_1) β†’ [inst : Quiver V] β†’ V β₯€q V
id

end Prefunctor

namespace Quiver

/-- `Vα΅’α΅–` reverses the direction of all arrows of `V`. -/
instance 
opposite: {V : Type ?u.54166} β†’ [inst : Quiver V] β†’ Quiver Vα΅’α΅–
opposite {
V: ?m.54163
V} [
Quiver: Type ?u.54166 β†’ Type (max?u.54166?u.54167)
Quiver 
V: ?m.54163
V] : 
Quiver: Type ?u.54170 β†’ Type (max?u.54170?u.54171)
Quiver 
V: ?m.54163
Vα΅’α΅– :=
  ⟨fun 
a: ?m.54183
a 
b: ?m.54186
b => (
unop: {Ξ± : Sort ?u.54195} β†’ Ξ±α΅’α΅– β†’ Ξ±
unop 
b: ?m.54186
b ⟢ 
unop: {Ξ± : Sort ?u.54199} β†’ Ξ±α΅’α΅– β†’ Ξ±
unop 
a: ?m.54183
a)α΅’α΅–βŸ©
#align quiver.opposite 
Quiver.opposite: {V : Type u_1} β†’ [inst : Quiver V] β†’ Quiver Vα΅’α΅–
Quiver.opposite

/-- The opposite of an arrow in `V`.
-/
def 
Hom.op: {V : Type ?u.54258} β†’ [inst : Quiver V] β†’ {X Y : V} β†’ (X ⟢ Y) β†’ (Opposite.op Y ⟢ Opposite.op X)
Hom.op {
V: ?m.54255
V} [
Quiver: Type ?u.54258 β†’ Type (max?u.54258?u.54259)
Quiver 
V: ?m.54255
V] {
X: V
X 
Y: V
Y : 
V: ?m.54255
V} (
f: X ⟢ Y
f : 
X: V
X ⟢ 
Y: V
Y) : 
op: {Ξ± : Sort ?u.54288} β†’ Ξ± β†’ Ξ±α΅’α΅–
op 
Y: V
Y ⟢ 
op: {Ξ± : Sort ?u.54291} β†’ Ξ± β†’ Ξ±α΅’α΅–
op 
X: V
X := ⟨
f: X ⟢ Y
f⟩
#align quiver.hom.op 
Quiver.Hom.op: {V : Type u_1} β†’ [inst : Quiver V] β†’ {X Y : V} β†’ (X ⟢ Y) β†’ (op Y ⟢ op X)
Quiver.Hom.op

pp_extended_field_notation 
Quiver.Hom.op: {V : Type u_1} β†’ [inst : Quiver V] β†’ {X Y : V} β†’ (X ⟢ Y) β†’ (op Y ⟢ op X)
Quiver.Hom.op

/-- Given an arrow in `Vα΅’α΅–`, we can take the "unopposite" back in `V`.
-/
def 
Hom.unop: {V : Type u_1} β†’ [inst : Quiver V] β†’ {X Y : Vα΅’α΅–} β†’ (X ⟢ Y) β†’ (Y.unop ⟢ X.unop)
Hom.unop {
V: ?m.57901
V} [
Quiver: Type ?u.57904 β†’ Type (max?u.57904?u.57905)
Quiver 
V: ?m.57901
V] {
X: Vα΅’α΅–
X 
Y: Vα΅’α΅–
Y : 
V: ?m.57901
Vα΅’α΅–} (
f: X ⟢ Y
f : 
X: Vα΅’α΅–
X ⟢ 
Y: Vα΅’α΅–
Y) : 
unop: {Ξ± : Sort ?u.57946} β†’ Ξ±α΅’α΅– β†’ Ξ±
unop 
Y: Vα΅’α΅–
Y ⟢ 
unop: {Ξ± : Sort ?u.57949} β†’ Ξ±α΅’α΅– β†’ Ξ±
unop 
X: Vα΅’α΅–
X := 
Opposite.unop: {Ξ± : Sort ?u.57965} β†’ Ξ±α΅’α΅– β†’ Ξ±
Opposite.unop 
f: X ⟢ Y
f
#align quiver.hom.unop 
Quiver.Hom.unop: {V : Type u_1} β†’ [inst : Quiver V] β†’ {X Y : Vα΅’α΅–} β†’ (X ⟢ Y) β†’ (Y.unop ⟢ X.unop)
Quiver.Hom.unop

pp_extended_field_notation 
Quiver.Hom.unop: {V : Type u_1} β†’ [inst : Quiver V] β†’ {X Y : Vα΅’α΅–} β†’ (X ⟢ Y) β†’ (Y.unop ⟢ X.unop)
Quiver.Hom.unop

/-- A type synonym for a quiver with no arrows. -/
-- Porting note: no has_nonempty_instance linter yet
-- @[nolint has_nonempty_instance]
def 
Empty: Type u β†’ Type u
Empty (
V: Type u
V : 
Type u: Type (u+1)
Type u) : 
Type u: Type (u+1)
Type u := 
V: Type u
V
#align quiver.empty 
Quiver.Empty: Type u β†’ Type u
Quiver.Empty

instance 
emptyQuiver: (V : Type u) β†’ Quiver (Empty V)
emptyQuiver (
V: Type u
V : 
Type u: Type (u+1)
Type u) : 
Quiver: Type ?u.61563 β†’ Type (max?u.61563u)
Quiver.{u} (
Empty: Type ?u.61564 β†’ Type ?u.61564
Empty 
V: Type u
V) := ⟨fun 
_: ?m.61574
_ 
_: ?m.61577
_ => 
PEmpty: Sort ?u.61579
PEmpty⟩
#align quiver.empty_quiver 
Quiver.emptyQuiver: (V : Type u) β†’ Quiver (Empty V)
Quiver.emptyQuiver

@[simp]
theorem 
empty_arrow: βˆ€ {V : Type u} (a b : Empty V), (a ⟢ b) = PEmpty
empty_arrow {
V: Type u
V : 
Type u: Type (u+1)
Type u} (
a: Empty V
a 
b: Empty V
b : 
Empty: Type ?u.61630 β†’ Type ?u.61630
Empty 
V: Type u
V) : (
a: Empty V
a ⟢ 
b: Empty V
b) = 
PEmpty: Sort ?u.61646
PEmpty := 
rfl: βˆ€ {Ξ± : Sort ?u.61670} {a : Ξ±}, a = a
rfl
#align quiver.empty_arrow 
Quiver.empty_arrow: βˆ€ {V : Type u} (a b : Empty V), (a ⟢ b) = PEmpty
Quiver.empty_arrow

/-- A quiver is thin if it has no parallel arrows. -/
@[reducible]
def 
IsThin: (V : Type u) β†’ [inst : Quiver V] β†’ Prop
IsThin (
V: Type u
V : 
Type u: Type (u+1)
Type u) [
Quiver: Type ?u.61693 β†’ Type (max?u.61693?u.61694)
Quiver 
V: Type u
V] : 
Prop: Type
Prop := βˆ€ 
a: V
a 
b: V
b : 
V: Type u
V, 
Subsingleton: Sort ?u.61705 β†’ Prop
Subsingleton (
a: V
a ⟢ 
b: V
b)
#align quiver.is_thin 
Quiver.IsThin: (V : Type u) β†’ [inst : Quiver V] β†’ Prop
Quiver.IsThin

end Quiver