1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85

-- https://github.com/BartoszMilewski/DaoFP

-- import Mathlib

-- universe u
def absurd' {C : Sort u} : Empty → C := Empty.rec

#check absurd'

#check id

-- Universes sad
-- #eval id id

-- Naturality condition

inductive Bool'
  | true' (a : Unit) : Bool'
  | false' (a : Unit) : Bool'

#check Bool'.true' = Bool'.false'


def f
  | 0 => 1
  | x + 1 => (x + 1) * f x

#eval f 69

def third {α β γ} (x : α × β × γ) :=
  let (_, _, c) := x
  c


universe v

-- class Natural (f : (Type u → Type v) → Type u → Type v) : Type (max (u + 1) v) where
-- Oops it's not a typeclass


def id' {α} (x : α) := x

#check id'

def yoneda {α} (m : Type u → Type v) [Functor m] (g : {β : Type u} → (α → β) → m β) : m α := g id

def yoneda' {α} (m : Type u → Type v) [Functor m] (y : m α) : {β : Type u} → (α → β) → m β := λ h ↦ h <$> y


-- def map_to_T (x : String) : Type :=
-- if x = "0" then
--   Nat
-- else
--   String

-- def natOrStringThree (b : Bool) : if b then Nat else String :=
--   match b with
--   | true => (3 : Nat)
--   | false => "three"

-- abbrev map_to_T (x : String) : Type :=
--   if x = "0" then Nat else String

-- def map_to (x : String) : map_to_T x :=
--   match decide (x = "0") with
--   | true => (42 : Nat)
--   | false => x

-- def map_to (x : String) : map_to_T x :=
--   if h : x = "0" then by
--     simp [map_to_T, h]
--     exact 42
--   else by
--     simp [map_to_T, h]
--     exact x


def ap [Monad m] (fs : m (α → β)) (as : m α) : m β := do
  -- fs >>= λ f ↦ as >>= λ a ↦ pure (f a)
  -- fs >>= (· <$> as)
  return (← fs) (← as)

class Monad' (m : Type → Type) where
  fish : (β → m γ) → (α → m β) → (α → m γ)
  join : (a : m (m α)) → m α := fish id id