module extraexercises where

open import Data.Nat
open import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning

J : {A : Set}
  → (C : (x y : A) → x ≡ y → Set)
  → (c : (x : A) → C x x refl)
  → (x y : A) → (p : x ≡ y) → C x y p
J C c x x refl = c x

-- Translation to PMLTT concepts

id : {A : Set} (a : A) → a ≡ a
id a = refl

idpeel : {A : Set} {a b : A}
  → (c : a ≡ b)
  → {C : (x y : A) → (z : x ≡ y) → Set}
  → (d : (x : A) → C x x (id x))
  → C a b c
idpeel {A} {a} {b} c {C} d = J C d a b c

-- Problem 2

inv : {A : Set} {a b : A}
  → (d : a ≡ b)
  → sym (sym d) ≡ d
inv {A} {a} {b} d = 
    J (λ x y p → sym (sym p) ≡ p) (λ x → refl) a b d

-- assoc : {A : Set} {a b c d : A}
--   → (e : a ≡ b)
--   → (f : b ≡ c)
--   → (g : c ≡ d)
--   → trans (trans e f) g ≡ trans e (trans f g)
-- assoc {a} {b} {c} {d} e f g =
--   let whatever = (λ f → J (λ x y p → trans (trans x f) y ≡ trans x (trans f y)) (λ x → {! !}) {!   !} {!   !} {!   !}) in
--   {!   !}

-- Problem 3

unitl : {A : Set}
  → (a : A)
  → {b : A}
  → (d : a ≡ b)
  → trans (id a) d ≡ d
unitl a d = id d

-- Problem 4

unitr : {A : Set}
  → {a : A}
  → (b : A)
  → (d : a ≡ b)
  → trans d (id b) ≡ d
unitr {A} {a} b d = J (λ x y p → trans p (id y) ≡ p) (λ x → id (id x)) a b d

-- Problem 5

-- ap : {A : Set}

-- Problem 6

-- id : {A : Set} → (a : A) → a ≡ a
-- id a = refl

-- interchange : {A : Set}
--   → (a : A)
--   → (d : id a ≡ id a)
--   → (e : id a ≡ id a)
--   → trans d e ≡ trans e d
-- interchange a d e =
--   let transde = trans d e in
--   let transed = trans e d in
--   let tmpl = J (λ x y p → {!   !}) (λ x → {!   !}) (id a) (id a) transde in
--   {!   !}