The binary action on identifications of binary dependent functions

Content created by Egbert Rijke.

Created on 2024-12-03.
Last modified on 2024-12-03.

module foundation.action-on-identifications-binary-dependent-functions where
Imports 
open import foundation.action-on-identifications-dependent-functions
open import foundation.binary-dependent-identifications
open import foundation.universe-levels

open import foundation-core.identity-types

Idea

Given a binary dependent function f : (x : A) (y : B) → C x y and identifications p : x ＝ x' in A and q : y ＝ y' in B, we obtain a binary dependent identification

  apd-binary f p q : binary-dependent-identification p q (f x y) (f x' y')

we call this the binary action on identifications of dependent binary functions.

Definitions

The binary action on identifications of binary dependent functions

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : A → B → UU l3}
  (f : (x : A) (y : B) → C x y)
  where

  apd-binary :
    {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
    binary-dependent-identification C p q (f x y) (f x' y')
  apd-binary refl refl = refl

See also

Recent changes