{-# OPTIONS --without-K --type-in-type #-}

postulate
  magic : ∀ {i} {X : Set i} → X

Type : Set
Type = Set

data _≡_ {A : Type} (x : A) : A → Type where
  refl : x ≡ x

J : ∀ {A : Type} {x : A} (B : (x' : A) → x ≡ x' → Type) (refl* : B x refl)
  {x' : A} (p : x ≡ x') → B x' p
J B refl* refl = refl*

ap : ∀ {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f {x} p = J (λ y p → f x ≡ f y) refl p

_∙_ : ∀ {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_∙_ {x = x} {z = z} p = J (λ y p → y ≡ z → x ≡ z) (λ q → q) p
infixr 80 _∙_

!_ : ∀ {A : Type} {x y : A} → x ≡ y → y ≡ x
!_ {x = x} p = J (λ y p → y ≡ x) refl p
infixr 100 !_

∙-unit-r : ∀ {A : Type} {x y : A} (q : x ≡ y) → q ∙ refl ≡ q
∙-unit-r q = J (λ y q → q ∙ refl ≡ q) refl q

-- Prove the following lemmas, using only J. (That is, do not use the "refl" pattern.)

∙-unit-l : ∀ {A : Type} {x y : A} (q : x ≡ y) → refl ∙ q ≡ q
∙-unit-l = magic

!-inv-l : ∀ {A : Type} {x y : A} (p : x ≡ y) → (! p) ∙ p ≡ refl
!-inv-l = magic

!-inv-r : ∀ {A : Type} {x y : A} (p : x ≡ y) → p ∙ (! p) ≡ refl
!-inv-r = magic

!-! : ∀ {A : Type} {x y : A} (p : x ≡ y) → ! (! p) ≡ p
!-! = magic

∙-assoc : ∀ {A : Type} {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
  → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r)
∙-assoc = magic

ap-∙ : ∀ {A B : Type} (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z)
  → ap f (p ∙ q) ≡ ap f p ∙ ap f q
ap-∙ = magic

ap-! : ∀ {A B : Type} (f : A → B) {x y : A} (p : x ≡ y) → ap f (! p) ≡ ! (ap f p)
ap-! = magic