Morphisms of descent data of the circle

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-08.
Last modified on 2024-04-25.

module synthetic-homotopy-theory.morphisms-descent-data-circle where
Imports 
open import foundation.commuting-squares-of-maps
open import foundation.universe-levels

open import structured-types.morphisms-types-equipped-with-automorphisms

open import synthetic-homotopy-theory.descent-circle

Idea

Given two descent data (A,e) and (B,f) over the circle, a **morphism** hof descent data between(A, e)and(B, f)is a maphfromAtoB` such that the square

      h
  A -----> B
  |        |
 e|        |f
  ∨        ∨
  A -----> B
      h

commutes.

Definitions

Morphisms of descent data for the circle

hom-descent-data-circle :
  { l1 l2 : Level}
  ( P : descent-data-circle l1) (Q : descent-data-circle l2) →
  UU (l1 ⊔ l2)
hom-descent-data-circle = hom-Type-With-Automorphism

module _
  { l1 l2 : Level} (P : descent-data-circle l1) (Q : descent-data-circle l2)
  ( h : hom-descent-data-circle P Q)
  where

  map-hom-descent-data-circle :
    type-descent-data-circle P → type-descent-data-circle Q
  map-hom-descent-data-circle =
    map-hom-Type-With-Automorphism P Q h

  coherence-square-hom-descent-data-circle :
    coherence-square-maps
      ( map-hom-descent-data-circle)
      ( map-descent-data-circle P)
      ( map-descent-data-circle Q)
      ( map-hom-descent-data-circle)
  coherence-square-hom-descent-data-circle =
    coherence-square-hom-Type-With-Automorphism P Q h

Recent changes