{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

-- Rename this file to "mysolutions.agda"

module mysolutions where

open import Universes
open import HoTT-UF-Agda

-- Exercises for beginners. We'll do them together

_∔_ : ℕ → ℕ → ℕ
zero ∔ y = y
succ x ∔ y = succ (x ∔ y)  -- (1 + x) + y = 1 + (x + y)


-- x is odd := there is some y such that x = 2 * y + 1

_*_ : ℕ → ℕ → ℕ
zero * y = zero
succ x * y = y ∔ x * y -- (1 + x) * y = y + x * y

distr : (x y z : ℕ) → x * (y ∔ z) ≡ x * y ∔ x * z
distr x y z = {!!}

comm : (x y : ℕ) → x ∔ y ≡ y ∔ x
comm x y = {!!}

infixl 20 _∔_
infixl 21 _*_

-- \Sigma y \:4 , x \== 2 * y \dotplus 1
-- \MCU\_0 \^.

is-odd' : ℕ → 𝓤₀ ̇
is-odd' x = Σ y ꞉ ℕ , x ≡ 2 * y ∔ 1

deepest-theorem : is-odd' 5
deepest-theorem = 2 , refl 5

is-odd : ℕ → 𝓤₀ ̇
is-odd zero = 𝟘
is-odd (succ n) = ¬ (is-odd n)

deepest-theorem' : is-odd 5
deepest-theorem' = {!!}

{- inductive definition of being odd:

    * 1 is odd (base case)
    * for any given x, if x is odd, then x + 2 is odd

-}

data is-odd₃ : ℕ → 𝓤₀ ̇ where
 base-case : is-odd₃ 1
 inductive-step : {x : ℕ} → is-odd₃ x
                          → is-odd₃ (2 ∔ x)
convert₃ : (x : ℕ) → is-odd' x → is-odd₃ x
convert₃ .(2 * y ∔ 1) (y , refl .(2 * y ∔ 1)) = {!!}

convert' : (x : ℕ) → is-odd₃ x → is-odd' x
convert' .1 base-case = {!!}
convert' .(2 ∔ x) (inductive-step {x} o) = goal
 where
  IH : is-odd' x
  IH = convert' x o
  y : ℕ
  y = pr₁ IH
  p : x ≡ 2 * y ∔ 1
  p = pr₂ IH
  y' : ℕ
  y' = 1 ∔ y
  r : 2 ∔ x ≡ 2 ∔ (2 * y ∔ 1)
  r = ap (2 ∔_) p
  s : 2 ∔ (2 * y ∔ 1) ≡ 2 ∔ (1 ∔ 2 * y)
  s = ap (2 ∔_) (comm (2 * y) 1)
  t : 2 ∔ x ≡ 2 ∔ (1 ∔ 2 * y)
  t = r ∙ s
  -- 2 * (y + 1) = 2 * y + 2 * 1 = 2 * y + 2
  q : 2 * (1 ∔ y) ≡ 2 ∔ 2 * y
  q = distr 2 1 y
  p' : 2 ∔ x ≡ 2 * y' ∔ 1
  p' = distr 2 {!y!} {!!}
  goal : is-odd' (2 ∔ x)
  goal = y' , p'

deepest-theorem₃ : is-odd₃ 5
deepest-theorem₃ = inductive-step
                     (inductive-step
                       base-case)


ℕ-induction' : (A : ℕ → 𝓤 ̇ )
             → A 0
             → ((n : ℕ) → A n → A (succ n))
             → (n : ℕ) → A n

ℕ-induction' A a₀ f = h
 where
  h : (n : ℕ) → A n
  h = {!!}

-- More to be added during the lecture


{- "Advanced exercises". They are already solved in the notes. So
rename them to e.g. subsingleton-criterion' to attempt them.

subsingleton-criterion : {X : 𝓤 ̇ }
                       → (X → is-singleton X)
                       → is-subsingleton X

subsingleton-criterion' : {X : 𝓤 ̇ }
                        → (X → is-subsingleton X)
                        → is-subsingleton X

retract-of-subsingleton : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                        → Y ◁ X → is-subsingleton X → is-subsingleton Y

left-cancellable : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
left-cancellable f = {x x' : domain f} → f x ≡ f x' → x ≡ x'

lc-maps-reflect-subsingletons : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                              → left-cancellable f
                              → is-subsingleton Y
                              → is-subsingleton X

has-retraction : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
has-retraction s = Σ r ꞉ (codomain s → domain s), r ∘ s ∼ id

sections-are-lc : {X : 𝓤 ̇ } {A : 𝓥 ̇ } (s : X → A)
                → has-retraction s → left-cancellable s

equivs-have-retractions : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                        → is-equiv f → has-retraction f

equivs-have-sections : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                     → is-equiv f → has-section f

equivs-are-lc : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
              → is-equiv f → left-cancellable f

equiv-to-subsingleton : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                      → X ≃ Y
                      → is-subsingleton Y
                      → is-subsingleton X

comp-inverses : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
                (f : X → Y) (g : Y → Z)
                (i : is-equiv f) (j : is-equiv g)
                (f' : Y → X) (g' : Z → Y)
              → f' ∼ inverse f i
              → g' ∼ inverse g j
              → f' ∘ g' ∼ inverse (g ∘ f) (∘-is-equiv j i)

equiv-to-set : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
             → X ≃ Y
             → is-set Y
             → is-set X

sections-closed-under-∼ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f g : X → Y)
                        → has-retraction f
                        → g ∼ f
                        → has-retraction g

retractions-closed-under-∼ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f g : X → Y)
                           → has-section f
                           → g ∼ f
                           → has-section g

is-joyal-equiv : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → (X → Y) → 𝓤 ⊔ 𝓥 ̇
is-joyal-equiv f = has-section f × has-retraction f

one-inverse : (X : 𝓤 ̇ ) (Y : 𝓥 ̇ )
              (f : X → Y) (r s : Y → X)
            → (r ∘ f ∼ id)
            → (f ∘ s ∼ id)
            → r ∼ s

joyal-equivs-are-invertible : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                            → is-joyal-equiv f → invertible f

joyal-equivs-are-equivs : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                        → is-joyal-equiv f → is-equiv f

invertibles-are-joyal-equivs : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                             → invertible f → is-joyal-equiv f

equivs-are-joyal-equivs : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                        → is-equiv f → is-joyal-equiv f

equivs-closed-under-∼ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {f g : X → Y}
                      → is-equiv f
                      → g ∼ f
                      → is-equiv g

equiv-to-singleton' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                    → X ≃ Y → is-singleton X → is-singleton Y

subtypes-of-sets-are-sets : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (m : X → Y)
                          → left-cancellable m → is-set Y → is-set X

pr₁-lc : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
       → ((x : X) → is-subsingleton (A x))
       → left-cancellable (λ (t : Σ A) → pr₁ t)

subsets-of-sets-are-sets : (X : 𝓤 ̇ ) (A : X → 𝓥 ̇ )
                         → is-set X
                         → ((x : X) → is-subsingleton (A x))
                         → is-set (Σ x ꞉ X , A x)

to-subtype-≡ : {X : 𝓦 ̇ } {A : X → 𝓥 ̇ }
               {x y : X} {a : A x} {b : A y}
             → ((x : X) → is-subsingleton (A x))
             → x ≡ y
             → (x , a) ≡ (y , b)

pr₁-is-equiv : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
             → ((x : X) → is-singleton (A x))
             → is-equiv (λ (t : Σ A) → pr₁ t)

pr₁-≃ : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
      → ((x : X) → is-singleton (A x))
      → Σ A ≃ X

pr₁-≃ i = pr₁ , pr₁-is-equiv i

ΠΣ-distr-≃ : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {P : (x : X) → A x → 𝓦 ̇ }
           → (Π x ꞉ X , Σ a ꞉ A x , P x a)
           ≃ (Σ f ꞉ Π A , Π x ꞉ X , P x (f x))

Σ-assoc : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {Z : Σ Y → 𝓦 ̇ }
        → Σ Z ≃ (Σ x ꞉ X , Σ y ꞉ Y x , Z (x , y))

⁻¹-≃ : {X : 𝓤 ̇ } (x y : X) → (x ≡ y) ≃ (y ≡ x)

singleton-types-≃ : {X : 𝓤 ̇ } (x : X) → singleton-type' x ≃ singleton-type x

singletons-≃ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
             → is-singleton X → is-singleton Y → X ≃ Y

maps-of-singletons-are-equivs : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y)
                              → is-singleton X → is-singleton Y → is-equiv f

logically-equivalent-subsingletons-are-equivalent : (X : 𝓤 ̇ ) (Y : 𝓥 ̇ )
                                                  → is-subsingleton X
                                                  → is-subsingleton Y
                                                  → X ⇔ Y
                                                  → X ≃ Y

singletons-are-equivalent : (X : 𝓤 ̇ ) (Y : 𝓥 ̇ )
                          → is-singleton X
                          → is-singleton Y
                          → X ≃ Y

NatΣ-fiber-equiv : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (φ : Nat A B)
                   (x : X) (b : B x)
                 → fiber (φ x) b ≃ fiber (NatΣ φ) (x , b)

NatΣ-equiv-gives-fiberwise-equiv : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {B : X → 𝓦 ̇ }
                                   (φ : Nat A B)
                                 → is-equiv (NatΣ φ)
                                 → ((x : X) → is-equiv (φ x))

Σ-is-subsingleton : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
                  → is-subsingleton X
                  → ((x : X) → is-subsingleton (A x))
                  → is-subsingleton (Σ A)

×-is-singleton : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                  → is-singleton X
                  → is-singleton Y
                  → is-singleton (X × Y)

×-is-subsingleton : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                  → is-subsingleton X
                  → is-subsingleton Y
                  → is-subsingleton (X × Y)

×-is-subsingleton' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                   → ((Y → is-subsingleton X) × (X → is-subsingleton Y))
                   → is-subsingleton (X × Y)

×-is-subsingleton'-back : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
                        → is-subsingleton (X × Y)
                        → (Y → is-subsingleton X) × (X → is-subsingleton Y)

ap₂ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } (f : X → Y → Z) {x x' : X} {y y' : Y}
    → x ≡ x' → y ≡ y' → f x y ≡ f x'

-}

-- \Mii \Mid

-- type "∼" as "\sim"

ex1 : {X : 𝓤 ̇ } {x x' : X}
    → ap (𝑖𝑑 X) ∼ 𝑖𝑑 (x ≡ x')
ex1 {𝓤} {X} {x} {.x} (refl .x) = refl (refl x)

-- ∘ is "\comp"

app : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (x x' : X)
      (f : X → Y)
    → x ≡ x' → f x ≡ f x'
app x .x f (refl .x) = refl (f x)


ex2 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
      (f : X → Y) (g : Y → Z)
      {x x' : X}
      (p : x ≡ x')
    → ap (g ∘ f) p ≡ (ap g ∘ ap f) p
ex2 {𝓤} {𝓥} {𝓦} {X} {Y} {Z} f g {x} {.x} (refl .x) = refl (refl (g (f x)))

ex2-1 : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
      (f : X → Y) (g : Y → Z)
      {x x' : X}
    → app x x' (g ∘ f)
    ∼ (app (f x) (f x') g ∘ app x x' f)
ex2-1 f g {x} {.x} (refl .x) = refl (refl (g (f x)))

ex2-bad : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
      (f : X → Y) (g : Y → Z)
      {x x' : X}
    → ap (g ∘ f) {x} {x'}
    ∼ (ap g ∘ ap f)
ex2-bad f g {x} {.x} (refl .x) = refl (refl (g (f x)))

is-singl : 𝓤 ̇ → 𝓤 ̇
is-singl X = Σ x ꞉ X , ((y : X) → x ≡ y)

single : {X : 𝓤 ̇} → X → 𝓤 ̇
single {𝓤} {X} x = Σ y ꞉ X , x ≡ y

ex3 : {X : 𝓤 ̇} (x : X)
    → is-singl (single x)
ex3 x = (x , refl x) , {!!}
