let
  congComp : {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x == y)
          -> cong (λ a → g (f a)) p == cong g (cong f p);
  congComp f g p = refl;

let
  the : (A : Type) -> A -> A;
  the A x = x;

let
  congId : {A : Type} {x y : A} (p : x == y)
        -> cong (λ x → x) p == p;
  congId p = ();

let
  axUIP : {A : Type} {x y : A} (p q : x == y)
       -> p == q;
  axUIP p q = ();

let
  symSym : {A : Type} {x y : A} (p : x == y)
         -> sym (sym p) == p;
  symSym p = refl;

congComp