Binary dependent identifications

Content created by Egbert Rijke.

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

module foundation.binary-dependent-identifications where
Imports 
open import foundation.binary-transport
open import foundation.identity-types
open import foundation.universe-levels

Idea

Consider a family of types C x y indexed by x : A and y : B, and consider identifications p : x ＝ x' and q : y ＝ y' in A and B, respectively. A binary dependent identification from c : C x y to c' : C x' y' over p and q is a dependent identification

  r : dependent-identification (C x') p (tr (λ t → C t y) p c) c'.

Definitions

Binary dependent identifications

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

  binary-dependent-identification :
    {x x' : A} (p : x ＝ x') {y y' : B} (q : y ＝ y') →
    C x y → C x' y' → UU l3
  binary-dependent-identification p q c c' = binary-tr C p q c ＝ c'

Recent changes