Displayed large reflexive graphs

Content created by Fredrik Bakke.

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

module graph-theory.displayed-large-reflexive-graphs where
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import graph-theory.large-reflexive-graphs
open import graph-theory.reflexive-graphs


A displayed large reflexive graph H a over a base large reflexive graph G is the structure of a dependent large reflexive graph over G. It consists of

  • A family of vertices over the vertices of G.

  • A family of dependent edges over the edges of G. More concretely, for every edge e : x → y in G and x' in H over x, and y' over x, a type of edges from x' to y' over e:

      x' ·········> y'   ∋ H
      x ----------> y    ∋ G.
  • A family of reflexivity edges refl : x' → x' over every reflexivity edge in G.


Displayed large reflexive graphs

  {α' : Level  Level} {β' : Level  Level  Level}
  (α : Level  Level) (β : Level  Level  Level)
  (G : Large-Reflexive-Graph α' β') : UUω

    vertex-Displayed-Large-Reflexive-Graph :
      {l : Level} (x : vertex-Large-Reflexive-Graph G l)  UU (α l)

    edge-Displayed-Large-Reflexive-Graph :
      {l1 l2 : Level}
      {x : vertex-Large-Reflexive-Graph G l1}
      {y : vertex-Large-Reflexive-Graph G l2}
      (f : edge-Large-Reflexive-Graph G x y)
      (x' : vertex-Displayed-Large-Reflexive-Graph x)
      (y' : vertex-Displayed-Large-Reflexive-Graph y) 
      UU (β l1 l2)

    refl-Displayed-Large-Reflexive-Graph :
      {l : Level}
      {x : vertex-Large-Reflexive-Graph G l}
      (x' : vertex-Displayed-Large-Reflexive-Graph x) 
        ( refl-Large-Reflexive-Graph G x)
        ( x')
        ( x')

open Displayed-Large-Reflexive-Graph public

The total large reflexive graph of a displayed large reflexive graph

module _
  {α1 α2 : Level  Level} {β1 β2 : Level  Level  Level}
  {G : Large-Reflexive-Graph α1 β1}
  (H : Displayed-Large-Reflexive-Graph α2 β2 G)

  vertex-total-large-reflexive-graph-Displayed-Large-Reflexive-Graph :
    (l : Level)  UU (α1 l  α2 l)
  vertex-total-large-reflexive-graph-Displayed-Large-Reflexive-Graph l =
    Σ ( vertex-Large-Reflexive-Graph G l)
      ( vertex-Displayed-Large-Reflexive-Graph H)

  edge-total-large-reflexive-graph-Displayed-Large-Reflexive-Graph :
    {l1 l2 : Level} 
    vertex-total-large-reflexive-graph-Displayed-Large-Reflexive-Graph l1 
    vertex-total-large-reflexive-graph-Displayed-Large-Reflexive-Graph l2 
    UU (β1 l1 l2  β2 l1 l2)
    ( x , x') (y , y') =
    Σ ( edge-Large-Reflexive-Graph G x y)
      ( λ e  edge-Displayed-Large-Reflexive-Graph H e x' y')

  refl-total-large-reflexive-graph-Displayed-Large-Reflexive-Graph :
    {l : Level}
    (x : vertex-total-large-reflexive-graph-Displayed-Large-Reflexive-Graph l) 
    edge-total-large-reflexive-graph-Displayed-Large-Reflexive-Graph x x
  refl-total-large-reflexive-graph-Displayed-Large-Reflexive-Graph (x , x') =
    ( refl-Large-Reflexive-Graph G x ,
      refl-Displayed-Large-Reflexive-Graph H x')

  total-large-reflexive-graph-Displayed-Large-Reflexive-Graph :
    Large-Reflexive-Graph  l  α1 l  α2 l)  l1 l2  β1 l1 l2  β2 l1 l2)
    total-large-reflexive-graph-Displayed-Large-Reflexive-Graph =
    total-large-reflexive-graph-Displayed-Large-Reflexive-Graph =
    total-large-reflexive-graph-Displayed-Large-Reflexive-Graph =

The fiber reflexive graph of a displayed large reflexive graph over a vertex

module _
  {α1 α2 : Level  Level} {β1 β2 : Level  Level  Level}
  {G : Large-Reflexive-Graph α1 β1}
  (H : Displayed-Large-Reflexive-Graph α2 β2 G)
  {l : Level} (x : vertex-Large-Reflexive-Graph G l)

  fiber-vertex-reflexive-graph-Displayed-Large-Reflexive-Graph :
    Reflexive-Graph (α2 l) (β2 l l)
  pr1 fiber-vertex-reflexive-graph-Displayed-Large-Reflexive-Graph =
    vertex-Displayed-Large-Reflexive-Graph H x
  pr1 (pr2 fiber-vertex-reflexive-graph-Displayed-Large-Reflexive-Graph) =
    edge-Displayed-Large-Reflexive-Graph H (refl-Large-Reflexive-Graph G x)
  pr2 (pr2 fiber-vertex-reflexive-graph-Displayed-Large-Reflexive-Graph) =
    refl-Displayed-Large-Reflexive-Graph H

Recent changes