Notions from the slice category Set/P(V), 4.11

The semantics of coalgebric logics is defined by coalgebras in the simple slice category Set / P(V). This category has tuples (X, f) as objects, where X is a set and f : X P(V) is a function (which, in the semantics, gives the covaluation of propositional variables). A morphism from (X,f) to (Y,g) is function h : X Y such that g h = f.
A T-coalgebra, for a functor T, is a function X T(X). For coalgebras in the slice we need to lift the functor T to the slice category. This happens via TL(X) = (T(X) × P(V), \pi_2) and TL(f) = T(f) × id, where TL is the lifted functor on the slice.
This is a lot of categorical noice for just the following point: A model is a triple (X,f,coval) with
  • 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
(I don't know, if the last point is needed somewhere.)
In the semantics, I simply define a model to be a triple, instead of using the notions from the slice category. However, the completeness proof uses the terminal cone in the slice and a specific property (lemma 4.11) about it.
This module defines the terminal cone and proves 4.11.
For the definitions and the proof I work in the embedding of the slice in Set. That is, instead of pairs (X, f) I only consider sets or rather types (in Coq) X. The f is often not needed, and when, it is passed as additional argument. Instead of commuting triangles g h = f (as morphisms in the slice) I only consider functions h. If necessary, the commutation is proved as lemma.

Require Export functor sets cast.

Section Slice.

  Variable V : Type.
  Variable T : functor.

Lift a functor T to the slice


  Definition slice_obj_T(T : functor)(X V : Type) : Type :=
    prod (obj T X) (set V).

  Definition slice_map_T{X Y : Type}(f : XY)
                                   : slice_obj_T T X Vslice_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 : XY),
    f gslice_map_T f slice_map_T g.

  Lemma feq_slice_map_T_compose :
    (X Y Z : Type)(f : XY)(g : YZ),
      (slice_map_T g) (slice_map_T f) slice_map_T (g f).

n-fold application of T in the slice


  Fixpoint iter_obj_T(X : Type)(n : nat) : Type :=
    match n with
      | 0 ⇒ X
      | S nslice_obj_T T (iter_obj_T X n) V
    end.

  Lemma slice_obj_T_eq_lift : (X Y : Type),
    X = Yslice_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 : XY)(n : nat) :
                                      (iter_obj_T X n) → (iter_obj_T Y n) :=
    match n with
      | 0 ⇒ f
      | S nslice_map_T (iter_fmap_T f n)
    end.

final object in the slice


  Definition slice_final : Type := prod unit (set V).

  Lemma nonempty_slice_final : non_empty_type slice_final.

  Definition slice_final_map{X : Type}(coval : Xset V)
                                                          : Xslice_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 : Xset V),
      coval_1 coval_2slice_final_map coval_1 slice_final_map coval_2.

  Lemma slice_final_map_pair_prop :
    (X Y : Type)(f : XY × (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 : XY),
      slice_final_map (@snd Y (set V)) (ftimes f id)
      slice_final_map (@snd X (set V)).

terminal sequence and cone


  Definition terminal_obj_sequence(n : nat) : Type :=
    iter_obj_T slice_final n.

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 nset V :=
    match n return terminal_obj_sequence nset 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 nslice_map_T (terminal_morph_sequence n)
      end.

  Fixpoint terminal_seq_cone{X : Type}(slice_c : Xslice_obj_T T X V)
                                   (n : nat) : Xterminal_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 : Xslice_obj_T T X V)(n : nat),
      c1 c2terminal_seq_cone c1 n terminal_seq_cone c2 n.

  Lemma terminal_seq_cone_property :
    (X : Type)(slice_c : Xslice_obj_T T X V)(n : nat),
      (terminal_morph_sequence n) (terminal_seq_cone slice_c (S n))
       terminal_seq_cone slice_c n.

towards Lemma 4.11 in the slice


  Definition slice_unit_coalg : Type := slice_finalobj T slice_final.

  Definition unit_coalg_sequence(c : slice_unit_coalg)(n : nat) :
           terminal_obj_sequence nterminal_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 nterminal_obj_sequence (S n)
        with
          | 0 ⇒ pair c (snd (B := set V))
          | S nslice_map_T (unit_coalg_sequence c n)
        end.

  Definition unit_coalg_seq_cone(c : slice_unit_coalg)(i n : nat) :
                         terminal_obj_sequence iterminal_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].