extra files

extra/extra/Lists.lagda.md

@@ -0,0 +1,18 @@
+#### Exercise `Any-∃` (practice)
+
+Show that `Any P xs` is isomorphic to `∃[ x ] (x ∈ xs × P x)`.
+
+```
+Any-∃ : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs ≃ ∃[ x ] (x ∈ xs × P x)
+Any-∃ {A} {P} {xs} = record
+  { to = to
+  ; from = {!!}
+  ; from∘to = {!!}
+  ; to∘from = {!!} }
+  where
+  to : ∀ {A : Set} {P : A → Set} {xs : List A} → Any P xs → ∃[ x ] (x ∈ xs × P x)
+  to (here {x = x} px) = ⟨ x , ⟨ here refl , px ⟩ ⟩
+  to (there anyp) with to anyp
+  ...                | ⟨ x , ⟨ x∈xs , px ⟩ ⟩ = ⟨ x , ⟨ there x∈xs , px ⟩ ⟩
+
+```

extra/extra/Rec1.agda

@@ -0,0 +1,7 @@
+module Rec1 where
+
+  import Rec2
+
+  y : ℕ
+  y = x
+

extra/extra/Rec2.agda

@@ -0,0 +1,10 @@
+module Rec2 where
+
+  open import Data.Nat
+  open import Rec1
+
+  x : ℕ
+  x = 42
+
+  z : ℕ
+  z = y