Library UniMath.IdentitySystems.RXGraphOfRXGraphs

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.IdentitySystems.RXGraph.
Require Import UniMath.IdentitySystems.Examples.
Require Import UniMath.IdentitySystems.Lenses.

Local Open Scope rxgraph.

Reflexive graph of graphs

Definition graph_on_rxgraph
  : contra_lens (UU_rxgraph ).
Proof.
  use make_contra_lens.
  - intros A; exact (A ~> A ~> UU_rxgraph ).
  - intros x y w e; cbn in w, e.
    exact (λ x' y', e (w x') (w y')).
  - intros A edge; exact (refl edge).
Defined.

Lemma is_univalent_graph_on_rxgraph (A : UU )
  : is_univalent (graph_on_rxgraph A).
Proof. exact (∏! _ _, UU_univalent_rxgraph). Qed.

Definition graph_rxgraph : rxgraph
  := total_rxgraph
       (contra_lens_disp_rxgraph (graph_on_rxgraph )).

Lemma is_univalent_graph_rxgraph
  : is_univalent (graph_rxgraph ).
Proof.
  apply is_univalent_total_rxgraph.
  - exact UU_univalent_rxgraph.
  - apply is_univalent_contra_lens_disp_rxgraph; intro A.
    apply is_univalent_graph_on_rxgraph.
Qed.

Definition graph_univalent_rxgraph : univalent_rxgraph
  := make_univalent_rxgraph _ is_univalent_graph_rxgraph.

Definition graph_iso (C D : graph_rxgraph ) : UU := C ≈ D.
Identity Coercion Id_graph_iso : graph_iso >-> edge.

Coercion graph_iso_on_vertex {C D : graph_rxgraph}
  (w : graph_iso C D) : pr1 C ≃ pr1 D := pr1 w.
Definition graph_iso_on_edge {C D : graph_rxgraph}
  (w : graph_iso C D)
  : ∏ {a b : pr1 C }, pr2 C a b ≃ pr2 D (w a) (w b)
  := pr2 w.

Definition make_graph_iso (C D : graph_rxgraph)
  (v : pr1 C ≃ pr1 D)
  (e : ∏ (a b : pr1 C ), pr2 C a b ≃ pr2 D (v a) (v b))
  : graph_iso C D
  := v ,, e.

Reflexive graph of rxgraphs

Definition has_refl_rxgraph
  : unbiased_lens (graph_rxgraph ).
Proof.
  use make_unbiased_lens.
  - intros C D f.
    change (graph_iso C D) in f.
    exact (∏~ (a : pr1 C), Δ pr2 D (f a) (f a)).
  - intros C D f refl a.
    change (graph_iso C D) in f.
    cbn in refl.
    exact (graph_iso_on_edge f (refl a)).
  - intros C D f refl a.
    change (graph_iso C D) in f.
    cbn in refl.
    exact (refl (f a)).
  - intros C refl'; exact (refl refl').
  - intros C refl'; exact (refl refl').
Defined.

Lemma is_univalent_has_refl_rxgraph
  {C D : graph_rxgraph } (w : graph_iso C D)
  : is_univalent (has_refl_rxgraph C D w).
Proof. exact (∏! _, Δ _). Qed.

Definition rxgraph_rxgraph : rxgraph
  := total_rxgraph
       (sigma_disp_rxgraph _
          (unbiased_lens_disp_rxgraph
             (has_refl_rxgraph ))).

Example rxgraph_vertex_rxgraph_rxgraph_compute
  : rxgraph_vertex (rxgraph_rxgraph )
    = rxgraph .
Proof. reflexivity. Defined.

Lemma is_univalent_rxgraph_rxgraph
  : is_univalent (rxgraph_rxgraph ).
Proof.
  use is_univalent_total_rxgraph.
  - exact UU_univalent_rxgraph.
  - apply is_univalent_sigma_disp_rxgraph.
    + apply is_univalent_contra_lens_disp_rxgraph; intro A.
      apply is_univalent_graph_on_rxgraph.
    + apply is_univalent_unbiased_lens_disp_rxgraph.
      intros C D w.
      apply is_univalent_has_refl_rxgraph.
Qed.

Definition rxgraph_univalent_rxgraph : univalent_rxgraph
  := make_univalent_rxgraph _ is_univalent_rxgraph_rxgraph.

Definition rxgraph_iso (C D : rxgraph) : UU := C ≈{rxgraph_rxgraph } D.
Identity Coercion Id_rxgraph_iso : graph_iso >-> edge.

Coercion rxgraph_iso_on_vertex {C D : rxgraph}
  (w : rxgraph_iso C D) : C ≃ D := pr1 w.
Definition rxgraph_iso_on_edge {C D : rxgraph}
  (w : rxgraph_iso C D)
  : ∏ {a b : C }, a ≈ b ≃ w a ≈ w b
  := pr12 w.
Definition rxgraph_iso_on_refl {C D : rxgraph}
  (w : rxgraph_iso C D)
  : ∏ (a : C ), rxgraph_iso_on_edge w (refl a) = refl (w a)
  := pr22 w.

Definition make_rxgraph_iso (C D : rxgraph)
  (verts : C ≃ D)
  (edges : ∏ {a b : C }, a ≈ b ≃ verts a ≈ verts b)
  (refls : ∏ (a : C ), edges (refl a) = refl (verts a))
  : rxgraph_iso C D
  := verts ,, @edges ,, refls.

Definition is_univalent_rxgraph_iso_f
  (C D : rxgraph) (F : rxgraph_iso C D)
  (H : is_univalent C) : is_univalent D.
Proof.
  apply is_univalent_from_isaprop_edges_from; intro a.
  apply (isofhlevelweqb 1 (Y:=(edges_from C (invmap F a)))).
  - apply (weqbandf (invweq F)); intro b.
    intermediate_weq (F (invmap F a) ≈ F (invmap F b)).
    { rewrite !(homotweqinvweq F).
      exact (idweq (a ≈ b)). }
    apply invweq, (rxgraph_iso_on_edge F).
  - apply is_univalent_to_isaprop_edges_from, H.
Qed.

Definition is_univalent_rxgraph_iso_b
  (C D : rxgraph) (F : rxgraph_iso C D)
  (H : is_univalent D) : is_univalent C.
Proof.
  apply is_univalent_from_isaprop_edges_from; intro a.
  apply (isofhlevelweqb 1 (Y:=(edges_from D (F a)))).
  - apply (weqbandf F); intro b.
    exact (rxgraph_iso_on_edge F).
  - apply is_univalent_to_isaprop_edges_from, H.
Qed.

Reflexive graph of displayed graphs

Definition disp_graph_on_rxgraph (B : rxgraph )
  : contra_lens (B ~> UU_rxgraph ).
Proof.
  use make_contra_lens.
  + intro E.
    exact (∏~ (x y : B) (e : x ≈ y ),
            E x ~> E y ~> UU_rxgraph ).
  + cbn; intros E₁ E₂ w edge x y e a b.
    exact (edge x y e (w x a) (w y b)).
  + intros E disp_edge; exact (refl disp_edge).
Defined.

Lemma is_univalent_disp_graph_on_rxgraph
  (B : rxgraph ) (E : B -> UU )
  : is_univalent (disp_graph_on_rxgraph B E).
Proof.
  do 5 (apply is_univalent_product_rxgraph; intro).
  exact UU_univalent_rxgraph.
Qed.

Definition disp_graph_rxgraph (B : rxgraph )
  : rxgraph
  := total_rxgraph
       (contra_lens_disp_rxgraph
          (disp_graph_on_rxgraph B)).

Lemma is_univalent_disp_graph_rxgraph (B : rxgraph )
  : is_univalent (disp_graph_rxgraph B).
Proof.
  apply is_univalent_total_rxgraph.
  - exact (∏! _, UU_univalent_rxgraph).
  - apply is_univalent_contra_lens_disp_rxgraph; intro.
    apply is_univalent_disp_graph_on_rxgraph.
Qed.

Reflexive graph of disp_rxgraphs

Definition has_disp_refl_rxgraph (B : rxgraph )
  : unbiased_lens (disp_graph_rxgraph B).
Proof.
  use make_unbiased_lens.
  - intros C D f.
    cbn in f.
    exact (∏~ (x : B) (a : pr1 C x ),
            Δ pr2 D x x (refl x) (pr1 f x a) (pr1 f x a)).
  - intros C D f disp_refl x a.
    cbn in f, disp_refl.
    exact (pr2 f _ _ (refl x) _ _ (disp_refl x a)).
  - intros C D f disp_refl x a.
    cbn in f, disp_refl.
    exact (disp_refl x (pr1 f x a)).
  - intros C disp_refl; exact (refl disp_refl).
  - intros C disp_refl; exact (refl disp_refl).
Defined.

Lemma is_univalent_has_disp_refl_rxgraph (B : rxgraph )
  {E₁ E₂ : disp_graph_rxgraph B} (f : E₁ ≈ E₂)
  : is_univalent (has_disp_refl_rxgraph B _ _ f).
Proof.
  exact (∏! _ _, Δ _).
Qed.

Definition disp_rxgraph_rxgraph (B : rxgraph )
  : rxgraph
  := total_rxgraph
       (sigma_disp_rxgraph _
          (unbiased_lens_disp_rxgraph
             (has_disp_refl_rxgraph B))).

Example rxgraph_vertex_disp_rxgraph_rxgraph_compute
  (B : rxgraph )
  : rxgraph_vertex (disp_rxgraph_rxgraph B)
    = disp_rxgraph B.
Proof. reflexivity. Qed.

Lemma is_univalent_disp_rxgraph_rxgraph (B : rxgraph )
  : is_univalent (disp_rxgraph_rxgraph B).
Proof.
  apply is_univalent_total_rxgraph.
  - exact (∏! _, UU_univalent_rxgraph).
  - apply is_univalent_sigma_disp_rxgraph.
    + apply is_univalent_contra_lens_disp_rxgraph; intro.
      apply is_univalent_disp_graph_on_rxgraph.
    + apply is_univalent_unbiased_lens_disp_rxgraph; intros x y e.
      apply is_univalent_has_disp_refl_rxgraph.
Qed.

Definition disp_rxgraph_univalent_rxgraph (B : rxgraph )
  : univalent_rxgraph
  := make_univalent_rxgraph _
       (is_univalent_disp_rxgraph_rxgraph B).

Definition disp_rxgraph_iso {B : rxgraph} (E₁ E₂ : disp_rxgraph B) : UU
  := E₁ ≈{disp_rxgraph_rxgraph B } E₂.

Definition make_disp_rxgraph_iso
  {B : rxgraph} (E₁ E₂ : disp_rxgraph B)
  (verts : ∏ {x}, E₁ x ≃ E₂ x)
  (edges : ∏ {x y : B} (e : x ≈ y) {a : E₁ x} {b : E₁ y },
      a ≈[e ] b ≃ verts a ≈[e ] verts b)
  (refls : ∏ (x : B) (a : E₁ x ),
      edges (refl x) (disp_refl x a) = disp_refl x (verts a))
  : disp_rxgraph_iso E₁ E₂
  := @verts ,, @edges ,, refls.

Displayed reflexive graph of disp_rxgraphs

Definition transportb_disp_rxgraph
  {B₁ B₂ : rxgraph} (i : rxgraph_iso B₁ B₂)
  (E : disp_rxgraph B₂)
  : disp_rxgraph B₁.
Proof.
  use make_disp_rxgraph.
  - intros x'.
    exact (E (i x')).
  - cbn; intros x y e a b.
    exact (a ≈[rxgraph_iso_on_edge i e] b).
  - cbn; intros x a.
    refine (transportb (λ e , a ≈[e ] a) _ (disp_refl (i x) a)).
    exact (rxgraph_iso_on_refl i x).
Defined.

Definition disp_rxgraph_lens_structure
  : contra_lens_structure
      (B:=rxgraph_rxgraph )
      (disp_rxgraph_rxgraph ).
Proof.
  use make_contra_lens_structure.
  - intros C D i E.
    exact (transportb_disp_rxgraph i E).
  - intros B E; exact (refl E).
Defined.

Definition disp_rxgraph_disp_rxgraph
  : disp_rxgraph (rxgraph_rxgraph )
  := contra_lens_disp_rxgraph
       (disp_rxgraph_rxgraph ,, disp_rxgraph_lens_structure
         : contra_lens (rxgraph_rxgraph )).

Lemma is_univalent_disp_rxgraph_disp_rxgraph
  : is_disp_univalent disp_rxgraph_disp_rxgraph.
Proof.
  apply is_univalent_contra_lens_disp_rxgraph; intro.
  apply is_univalent_disp_rxgraph_rxgraph.
Qed.

Definition disp_rxgraph_univalent_disp_rxgraph
  : univalent_disp_rxgraph (rxgraph_rxgraph )
  := make_univalent_disp_rxgraph _ is_univalent_disp_rxgraph_disp_rxgraph.