Add random daofp stuff

Changes

1 changed files (+73/-0)

• Dao.lean (new)
  • @@ -0,0 +1,73 @@
    + -- 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