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

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

-- Problem 2

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 = J {!   !} {!   !} {!   !} {!   !} {!   !} in
  {!   !}

-- 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
--   {!   !}