From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Diagrams.Graph.
Require Import Diagrams.Diagram.

(** We define here the Graph ∫D, also denoted G·D *)

Definition integral {G : Graph} (D : Diagram G) : Graph.
G: Graph
D: Diagram G
Graph
Proof.
G: Graph
D: Diagram G
Graph
  srapply Build_Graph.
G: Graph
D: Diagram G
Type
G: Graph
D: Diagram G
?graph0 -> ?graph0 -> Type
  +
G: Graph
D: Diagram G
Type exact {i : G & D i}.
  +
G: Graph
D: Diagram G
{i : G & D i} -> {i : G & D i} -> Type intros i j.
G: Graph
D: Diagram G
i, j: {i0 : G & D i0}
Type
    exact {g : G i.1 j.1 & D _f g i.2 = j.2}.
Defined.

(** Then, a dependent diagram E over D is just a diagram over ∫D. *)

Definition DDiagram {G : Graph} (D : Diagram G)
  := Diagram (integral D).

(** Given a dependent diagram, we can recover a diagram over G by considering the Σ types. *)

  Definition diagram_sigma {G : Graph} {D : Diagram G} (E : DDiagram D)
    : Diagram G.
G: Graph
D: Diagram G
E: DDiagram D
Diagram G
  Proof.
G: Graph
D: Diagram G
E: DDiagram D
Diagram G
    srapply Build_Diagram.
G: Graph
D: Diagram G
E: DDiagram D
G -> Type
G: Graph
D: Diagram G
E: DDiagram D
forall i j : G, G i j -> ?obj i -> ?obj j
    -
G: Graph
D: Diagram G
E: DDiagram D
G -> Type intro i.
G: Graph
D: Diagram G
E: DDiagram D
i: G
Type
      exact {x : D i & E (i; x)}.
    -
G: Graph
D: Diagram G
E: DDiagram D
forall i j : G,
G i j ->
(fun i0 : G => {x : D i0 & E (i0; x)}) i ->
(fun i0 : G => {x : D i0 & E (i0; x)}) j intros i j g x.
G: Graph
D: Diagram G
E: DDiagram D
i, j: G
g: G i j
x: (fun i0 : G => {x0 : D i0 & E (i0; x0)}) i
(fun i0 : G => {x0 : D i0 & E (i0; x0)}) j simpl in *.
G: Graph
D: Diagram G
E: DDiagram D
i, j: G
g: G i j
x: {x0 : D i & E (i; x0)}
{x0 : D j & E (j; x0)}
      exists (D _f g x.1).
G: Graph
D: Diagram G
E: DDiagram D
i, j: G
g: G i j
x: {x0 : D i & E (i; x0)}
E (j; (D _f g) x.1)
      exact (@arr _ E (i; x.1) (j; D _f g x.1) (g; idpath) x.2).
  Defined.

  (** A dependent diagram is said equifibered if all its fibers are equivalences. *)

  Class Equifibered {G : Graph} {D : Diagram G} (E : DDiagram D) := {
    isequifibered i j (g : G i j) (x : D i)
      :: IsEquiv (@arr _ E (i; x) (j; D _f g x) (g; idpath));
  }.