Require Import Diagrams.Graph. Require Import Diagrams.Diagram. (** We define here the Graph ∫D, also denoted G·D *)G: Graph
D: Diagram GGraphG: Graph
D: Diagram GGraphG: Graph
D: Diagram GTypeG: Graph
D: Diagram G?graph0 -> ?graph0 -> Typeexact {i : G & D i}.G: Graph
D: Diagram GTypeG: Graph
D: Diagram G{i : G & D i} -> {i : G & D i} -> Typeexact {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 c.an recover a diagram over G by considering the Σ types. *)G: Graph
D: Diagram G
i, j: {i : G & D i}TypeG: Graph
D: Diagram G
E: DDiagram DDiagram GG: Graph
D: Diagram G
E: DDiagram DDiagram GG: Graph
D: Diagram G
E: DDiagram DG -> TypeG: Graph
D: Diagram G
E: DDiagram Dforall i j : G, G i j -> ?obj i -> ?obj jG: Graph
D: Diagram G
E: DDiagram DG -> Typeexact {x : D i & E (i; x)}.G: Graph
D: Diagram G
E: DDiagram D
i: GTypeG: Graph
D: Diagram G
E: DDiagram Dforall 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)}) jG: Graph
D: Diagram G
E: DDiagram D
i, j: G
g: G i j
x: (fun i : G => {x : D i & E (i; x)}) i(fun i : G => {x : D i & E (i; x)}) jG: Graph
D: Diagram G
E: DDiagram D
i, j: G
g: G i j
x: {x : D i & E (i; x)}{x : D j & E (j; x)}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)); }. #[export] Existing Instance isequifibered.G: Graph
D: Diagram G
E: DDiagram D
i, j: G
g: G i j
x: {x : D i & E (i; x)}E (j; (D _f g) x.1)