{-# OPTIONS --cubical #-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function

data F (A : Set) : Set where
  * : F A
  cayley' : A → * ≡ *

module _ (A : Set) (x : A) where

  foo : F A → F A
  foo * = *
  foo (cayley' y i) =
    hcomp (λ j → λ {
      (i = i0) → cayley' x j;
      (i = i1) → cayley' x j
    }) (cayley' y i)

  bar : F A → F A
  bar = {!!}

  foobar : ∀ m → foo (bar m) ≡ m
  foobar = {!!}

  barfoo : ∀ m → bar (foo m) ≡ m
  barfoo = {!!}

  cayley : F A ≡ F A
  cayley = ua (isoToEquiv (iso foo bar foobar barfoo))