-- The Agda standard library
-- Turn a relation into a record definition so as to remember the things
-- being related.
-- This module has a readme file: README.Data.Wrap

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Wrap where

open import Data.Product.Nary.NonDependent
open import Function.Nary.NonDependent
open import Level using (Level)
open import Relation.Nary

     : Level

record Wrap′ {n} {ls} {A : Sets n ls} (F : A  Set ) (xs : Product n A)
                  : Set  where
  constructor [_]
    get : uncurryₙ n F xs

open Wrap′ public

Wrap :  {n ls} {A : Sets n ls}  A  Set   A  Set 
Wrap {n = n} F = curryₙ n (Wrap′ F)