Function large binary relations

Content created by Louis Wasserman.

Created on 2026-02-21.
Last modified on 2026-02-21.

module foundation.function-large-binary-relations where
Imports 
open import foundation.dependent-products-large-binary-relations
open import foundation.large-binary-relations
open import foundation.universe-levels

Idea

Given a large binary relation on a family of types X stratified by universe levels, there is an induced large binary relation on functions I → X.

Definition

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  {l0 : Level}
  (I : UU l0)
  {X : (l : Level) → UU (α l)}
  where

  function-Large-Relation :
    Large-Relation β X → Large-Relation (λ l1 l2 → l0 ⊔ β l1 l2) (λ l → I → X l)
  function-Large-Relation R = Π-Large-Relation I (λ _ → X) (λ _ → R)

  function-Large-Relation-Prop :
    Large-Relation-Prop β X →
    Large-Relation-Prop (λ l1 l2 → l0 ⊔ β l1 l2) (λ l → I → X l)
  function-Large-Relation-Prop R =
    Π-Large-Relation-Prop I (λ _ → X) (λ _ → R)

Recent changes