Sigma.v

(* -*- mode: coq; mode: visual-line -*-  *)

Require Import Basics.Overture Basics.Tactics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import WildCat.Core.

(** ** Indexed sum of categories *)

Section Sigma.

  Context (A : Type) (B : A -> Type)
    `{forall a, IsGraph (B a)}
    `{forall a, Is01Cat (B a)}
    `{forall a, Is0Gpd (B a)}.

Global Instance isgraph_sigma : IsGraph (sig B).A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
IsGraph {x : _ & B x}
Proof.A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
IsGraph {x : _ & B x}
  srapply Build_IsGraph.A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
{x : _ & B x} -> {x : _ & B x} -> Type
  intros [x u] [y v].A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
x: A
u: B x
y: A
v: B y
Type
  exact {p : x = y & p # u $-> v}.
Defined.

Global Instance is01cat_sigma : Is01Cat (sig B).A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
Is01Cat {x : _ & B x}
Proof.A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
Is01Cat {x : _ & B x}
  srapply Build_Is01Cat.A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
forall a : {x : _ & B x}, a $-> a
A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
forall a b c : {x : _ & B x},
(b $-> c) -> (a $-> b) -> a $-> c
  +A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
forall a : {x : _ & B x}, a $-> a intros [x u].A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
x: A
u: B x
(x; u) $-> (x; u)
    exists idpath.A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
x: A
u: B x
transport B 1 u $-> u exact (Id u).
  +A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
forall a b c : {x : _ & B x},
(b $-> c) -> (a $-> b) -> a $-> c intros [x u] [y v] [z w] [q g] [p f].A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
x: A
u: B x
y: A
v: B y
z: A
w: B z
q: y = z
g: transport B q v $-> w
p: x = y
f: transport B p u $-> v
(x; u) $-> (z; w)
    exists (p @ q).A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
x: A
u: B x
y: A
v: B y
z: A
w: B z
q: y = z
g: transport B q v $-> w
p: x = y
f: transport B p u $-> v
transport B (p @ q) u $-> w
    destruct p, q; cbn in *.A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
x: A
u, v, w: B x
g: v $-> w
f: u $-> v
u $-> w 
    exact (g $o f).
Defined.

Global Instance is0gpd_sigma : Is0Gpd (sig B).A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
Is0Gpd {x : _ & B x}
Proof.A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
Is0Gpd {x : _ & B x}
  constructor.A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
forall a b : {x : _ & B x}, (a $-> b) -> b $-> a
  intros [x u] [y v] [p f].A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
x: A
u: B x
y: A
v: B y
p: x = y
f: transport B p u $-> v
(y; v) $-> (x; u)
  exists (p^).A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
x: A
u: B x
y: A
v: B y
p: x = y
f: transport B p u $-> v
transport B p^ v $-> u
  destruct p; cbn in *.A: Type
B: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, Is01Cat (B a)
H1: forall a : A, Is0Gpd (B a)
x: A
u, v: B x
f: u $-> v
v $-> u
  exact (f^$).
Defined.

End Sigma.

Global Instance is0functor_sigma {A : Type} (B C : A -> Type)
       `{forall a, IsGraph (B a)} `{forall a, IsGraph (C a)}
       `{forall a, Is01Cat (B a)} `{forall a, Is01Cat (C a)}
       (F : forall a, B a -> C a) {ff : forall a, Is0Functor (F a)}
  : Is0Functor (fun (x:sig B) => (x.1 ; F x.1 x.2)).A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, IsGraph (C a)
H1: forall a : A, Is01Cat (B a)
H2: forall a : A, Is01Cat (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
Is0Functor (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
Proof.A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, IsGraph (C a)
H1: forall a : A, Is01Cat (B a)
H2: forall a : A, Is01Cat (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
Is0Functor (fun x : {x : _ & B x} => (x.1; F x.1 x.2))
  constructor; intros [a1 b1] [a2 b2] [p f]; cbn.A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, IsGraph (C a)
H1: forall a : A, Is01Cat (B a)
H2: forall a : A, Is01Cat (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
a1: A
b1: B a1
a2: A
b2: B a2
p: a1 = a2
f: transport B p b1 $-> b2
{p : a1 = a2 & transport C p (F a1 b1) $-> F a2 b2}
  exists p.A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, IsGraph (C a)
H1: forall a : A, Is01Cat (B a)
H2: forall a : A, Is01Cat (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
a1: A
b1: B a1
a2: A
b2: B a2
p: a1 = a2
f: transport B p b1 $-> b2
transport C p (F a1 b1) $-> F a2 b2
  destruct p; cbn in *.A: Type
B, C: A -> Type
H: forall a : A, IsGraph (B a)
H0: forall a : A, IsGraph (C a)
H1: forall a : A, Is01Cat (B a)
H2: forall a : A, Is01Cat (C a)
F: forall a : A, B a -> C a
ff: forall a : A, Is0Functor (F a)
a1: A
b1, b2: B a1
f: b1 $-> b2
F a1 b1 $-> F a1 b2
  exact (fmap (F a1) f).
Defined.