------------------------------------------------------------------------
-- The Agda standard library
--
-- The constant function
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Function.Construct.Constant where
open import Function.Base using (const)
open import Function.Bundles using (Func)
import Function.Definitions as Definitions using (Congruent)
import Function.Structures as Structures using (IsCongruent)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures as B hiding (IsEquivalence)
private
variable
a b ℓ₁ ℓ₂ : Level
A B : Set a
------------------------------------------------------------------------
-- Properties
module _ (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) where
open Definitions
congruent : ∀ {b} → b ≈₂ b → Congruent _≈₁_ _≈₂_ (const b)
congruent refl _ = refl
------------------------------------------------------------------------
-- Structures
module _
{≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
(isEq₁ : B.IsEquivalence ≈₁)
(isEq₂ : B.IsEquivalence ≈₂) where
open Structures ≈₁ ≈₂
open B.IsEquivalence
isCongruent : ∀ b → IsCongruent (const b)
isCongruent b = record
{ cong = congruent ≈₁ ≈₂ (refl isEq₂)
; isEquivalence₁ = isEq₁
; isEquivalence₂ = isEq₂
}
------------------------------------------------------------------------
-- Setoid bundles
module _ (S : Setoid a ℓ₂) (T : Setoid b ℓ₂) where
open Setoid
function : Carrier T → Func S T
function b = record
{ to = const b
; cong = congruent (_≈_ S) (_≈_ T) (refl T)
}
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