------------------------------------------------------------------------
-- The Agda standard library
--
-- Core definitions for Functions
------------------------------------------------------------------------
-- The contents of this file should always be accessed from `Function`.
{-# OPTIONS --cubical-compatible --safe #-}
module Function.Core where
open import Level using (_⊔_)
------------------------------------------------------------------------
-- Types
Fun₁ : ∀ {a} → Set a → Set a
Fun₁ A = A → A
Fun₂ : ∀ {a} → Set a → Set a
Fun₂ A = A → A → A
------------------------------------------------------------------------
-- Morphism
Morphism : ∀ {a} → ∀ {b} → Set a → Set b → Set (a ⊔ b)
Morphism A B = A → B
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4