Kata

Prove that coinduction (on coinductive stream) is equivalent to path.

Please do this Kata in advance to ensure that you know what is bisimulation. Preloaded codes are basically identical, but this time it's based on Cubical Path instead of Propositional Equality:

{-# OPTIONS --copattern --cubical --safe --no-sized-types --guardedness #-}
module StreamDef where

open import Cubical.Core.Everything

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream public

-- | Bisimulation as equality
record _==_ {A : Set} (x : Stream A) (y : Stream A) : Set where
  coinductive
  field
    refl-head : head x ≡ head y
    refl-tail : tail x == tail y
open _==_ public

You need to know what is the univalence axiom to do this.