module Lib.Hide where

record Hide (X : Set) : Set where
  constructor hide
  field .expose : X
open Hide public

postulate
  .irrAx : {A : Set} → .A → A

.unhide : forall {A} → Hide A → A
unhide (hide a) = irrAx a