view paper/src/Equiv.agda.replaced @ 2:c7acb9211784

add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +0900
parents
children b5fffa8ae875
line wrap: on
line source

data _@$\equiv$@_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x @$\equiv$@ x