Notions from the slice category Set/P(V), 4.11
- X a set of states
- f : X → T(X) the transition function
- coval : X → P(V) the covaluation of propositional variables
- p holds for x iff p holds for f(x), for a variable p and a state x
Definition slice_obj_T(T : functor)(X V : Type) : Type :=
prod (obj T X) (set V).
Definition slice_map_T{X Y : Type}(f : X → Y)
: slice_obj_T T X V → slice_obj_T T Y V :=
ftimes (fmap T f) id.
Lemma slice_map_T_id : ∀(X : Type),
slice_map_T (@id X) ≡ @id (slice_obj_T T X V).
Lemma feq_slice_map_T : ∀(X Y : Type)(f g : X → Y),
f ≡ g → slice_map_T f ≡ slice_map_T g.
Lemma feq_slice_map_T_compose :
∀(X Y Z : Type)(f : X → Y)(g : Y → Z),
(slice_map_T g) ∘ (slice_map_T f) ≡ slice_map_T (g ∘ f).
Fixpoint iter_obj_T(X : Type)(n : nat) : Type :=
match n with
| 0 ⇒ X
| S n ⇒ slice_obj_T T (iter_obj_T X n) V
end.
Lemma slice_obj_T_eq_lift : ∀(X Y : Type),
X = Y → slice_obj_T T X V = slice_obj_T T Y V.
Lemma slice_obj_T_eq_lift_refl : ∀(X : Type),
slice_obj_T_eq_lift X X eq_refl = eq_refl.
Lemma iter_obj_T_S_n : ∀(X : Type)(n : nat),
iter_obj_T (slice_obj_T T X V) n = iter_obj_T X (S n).
Fixpoint iter_fmap_T{X Y : Type}(f : X → Y)(n : nat) :
(iter_obj_T X n) → (iter_obj_T Y n) :=
match n with
| 0 ⇒ f
| S n ⇒ slice_map_T (iter_fmap_T f n)
end.
Definition slice_final : Type := prod unit (set V).
Lemma nonempty_slice_final : non_empty_type slice_final.
Definition slice_final_map{X : Type}(coval : X → set V)
: X → slice_final :=
pair (final_map X) coval.
Lemma slice_final_map_id :
@slice_final_map slice_final (@snd unit (set V)) ≡ @id slice_final.
Lemma feq_slice_final_map_coval :
∀(X : Type)(coval_1 coval_2 : X → set V),
coval_1 ≡ coval_2 → slice_final_map coval_1 ≡ slice_final_map coval_2.
Lemma slice_final_map_pair_prop :
∀(X Y : Type)(f : X → Y × (set V)),
slice_final_map (@snd Y (set V)) ∘ f ≡
slice_final_map ((@snd Y (set V)) ∘ f).
Lemma slice_final_map_times_prop :
∀(X Y : Type)(f : X → Y),
slice_final_map (@snd Y (set V)) ∘ (ftimes f id) ≡
slice_final_map (@snd X (set V)).
I need to define the projections of the terminal sequence cone
by case analysis on n. Otherwise Coq is not able to recognice
that the term is a product.
The first projection has a different type for n = 0. Therefore
I only define it here for n > 0.
Definition terminal_obj_sequence_pi_1(n : nat) :
terminal_obj_sequence (S n) → obj T (terminal_obj_sequence n) :=
match n
return terminal_obj_sequence (S n) → obj T (terminal_obj_sequence n)
with
| 0 ⇒ @fst (obj T (terminal_obj_sequence 0)) _
| S n ⇒ @fst (obj T (terminal_obj_sequence (S n))) _
end.
Lemma terminal_obj_sequence_pi_1_char :
∀(n : nat)(tx : obj T (terminal_obj_sequence n))(pv : set V),
terminal_obj_sequence_pi_1 n (tx, pv) = tx.
Definition terminal_obj_sequence_pi_2(n : nat) :
terminal_obj_sequence n → set V :=
match n return terminal_obj_sequence n → set V
with
| 0 ⇒ @snd _ _
| S n ⇒ @snd (obj T (terminal_obj_sequence n)) _
end.
Lemma nonempty_terminal_obj_sequence :
∀(n : nat)(coval : set V),
non_trivial_functor T →
∃(x : terminal_obj_sequence n),
terminal_obj_sequence_pi_2 n x = coval.
Definition terminal_morph_sequence(n : nat) :
(terminal_obj_sequence (S n)) → terminal_obj_sequence n :=
fun_dom_cast (iter_obj_T_S_n slice_final n)
(iter_fmap_T
(slice_final_map (X := terminal_obj_sequence 1) (snd (B := set V)))
n).
Lemma terminal_morph_sequence_char : ∀(n : nat),
terminal_morph_sequence n =
match n return terminal_obj_sequence (S n) → terminal_obj_sequence n
with
| 0 ⇒ slice_final_map
(X := terminal_obj_sequence 1) (snd (B := set V))
| S n ⇒ slice_map_T (terminal_morph_sequence n)
end.
Fixpoint terminal_seq_cone{X : Type}(slice_c : X → slice_obj_T T X V)
(n : nat) : X → terminal_obj_sequence n :=
match n with
| 0 ⇒ slice_final_map ((snd (B := set V)) ∘ slice_c)
| S n ⇒ (slice_map_T (terminal_seq_cone slice_c n)) ∘ slice_c
end.
Lemma feq_terminal_seq_cone :
∀(X : Type)(c1 c2 : X → slice_obj_T T X V)(n : nat),
c1 ≡ c2 → terminal_seq_cone c1 n ≡ terminal_seq_cone c2 n.
Lemma terminal_seq_cone_property :
∀(X : Type)(slice_c : X → slice_obj_T T X V)(n : nat),
(terminal_morph_sequence n) ∘ (terminal_seq_cone slice_c (S n))
≡ terminal_seq_cone slice_c n.
terminal_obj_sequence (S n) → obj T (terminal_obj_sequence n) :=
match n
return terminal_obj_sequence (S n) → obj T (terminal_obj_sequence n)
with
| 0 ⇒ @fst (obj T (terminal_obj_sequence 0)) _
| S n ⇒ @fst (obj T (terminal_obj_sequence (S n))) _
end.
Lemma terminal_obj_sequence_pi_1_char :
∀(n : nat)(tx : obj T (terminal_obj_sequence n))(pv : set V),
terminal_obj_sequence_pi_1 n (tx, pv) = tx.
Definition terminal_obj_sequence_pi_2(n : nat) :
terminal_obj_sequence n → set V :=
match n return terminal_obj_sequence n → set V
with
| 0 ⇒ @snd _ _
| S n ⇒ @snd (obj T (terminal_obj_sequence n)) _
end.
Lemma nonempty_terminal_obj_sequence :
∀(n : nat)(coval : set V),
non_trivial_functor T →
∃(x : terminal_obj_sequence n),
terminal_obj_sequence_pi_2 n x = coval.
Definition terminal_morph_sequence(n : nat) :
(terminal_obj_sequence (S n)) → terminal_obj_sequence n :=
fun_dom_cast (iter_obj_T_S_n slice_final n)
(iter_fmap_T
(slice_final_map (X := terminal_obj_sequence 1) (snd (B := set V)))
n).
Lemma terminal_morph_sequence_char : ∀(n : nat),
terminal_morph_sequence n =
match n return terminal_obj_sequence (S n) → terminal_obj_sequence n
with
| 0 ⇒ slice_final_map
(X := terminal_obj_sequence 1) (snd (B := set V))
| S n ⇒ slice_map_T (terminal_morph_sequence n)
end.
Fixpoint terminal_seq_cone{X : Type}(slice_c : X → slice_obj_T T X V)
(n : nat) : X → terminal_obj_sequence n :=
match n with
| 0 ⇒ slice_final_map ((snd (B := set V)) ∘ slice_c)
| S n ⇒ (slice_map_T (terminal_seq_cone slice_c n)) ∘ slice_c
end.
Lemma feq_terminal_seq_cone :
∀(X : Type)(c1 c2 : X → slice_obj_T T X V)(n : nat),
c1 ≡ c2 → terminal_seq_cone c1 n ≡ terminal_seq_cone c2 n.
Lemma terminal_seq_cone_property :
∀(X : Type)(slice_c : X → slice_obj_T T X V)(n : nat),
(terminal_morph_sequence n) ∘ (terminal_seq_cone slice_c (S n))
≡ terminal_seq_cone slice_c n.
Definition slice_unit_coalg : Type := slice_final → obj T slice_final.
Definition unit_coalg_sequence(c : slice_unit_coalg)(n : nat) :
terminal_obj_sequence n → terminal_obj_sequence (S n) :=
fun_codom_cast (iter_obj_T_S_n slice_final n)
(iter_fmap_T (pair c (snd (B := set V))) n).
Lemma unit_coalg_sequence_char :
∀(c : slice_unit_coalg)(n : nat),
unit_coalg_sequence c n =
match n return terminal_obj_sequence n → terminal_obj_sequence (S n)
with
| 0 ⇒ pair c (snd (B := set V))
| S n ⇒ slice_map_T (unit_coalg_sequence c n)
end.
Definition unit_coalg_seq_cone(c : slice_unit_coalg)(i n : nat) :
terminal_obj_sequence i → terminal_obj_sequence n :=
terminal_seq_cone (unit_coalg_sequence c i) n.
Lemma unit_coalg_seq_cone_after_c :
∀(c : slice_unit_coalg)(i n : nat),
(unit_coalg_seq_cone c (S i) n) ∘ (unit_coalg_sequence c i)
≡ unit_coalg_seq_cone c i n.
Lemma 4.11 in the slice, page 22
Lemma unit_coalg_seq_cone_identity :
∀(c : slice_unit_coalg)(n : nat),
unit_coalg_seq_cone c n n ≡ @id (terminal_obj_sequence n).
End Slice.
Implicit Arguments terminal_obj_sequence_pi_2 [V T].
Implicit Arguments terminal_obj_sequence_pi_1 [V T].
Implicit Arguments nonempty_terminal_obj_sequence [V T].
Implicit Arguments terminal_seq_cone [V T X].
Implicit Arguments unit_coalg_sequence [V T].
∀(c : slice_unit_coalg)(n : nat),
unit_coalg_seq_cone c n n ≡ @id (terminal_obj_sequence n).
End Slice.
Implicit Arguments terminal_obj_sequence_pi_2 [V T].
Implicit Arguments terminal_obj_sequence_pi_1 [V T].
Implicit Arguments nonempty_terminal_obj_sequence [V T].
Implicit Arguments terminal_seq_cone [V T X].
Implicit Arguments unit_coalg_sequence [V T].