Показывает, что Конат Коалгебра Терминал - PullRequest
Новая
       37

Показывает, что Конат Коалгебра Терминал

0 голосов
/ 19 февраля 2019

У меня есть определение Коната в Агде (на самом деле это определение в кубической библиотеке ).Я пытаюсь показать, что связанная F-коалгебра является (Homotopy-) терминальной.

Мне удалось доказать существование F-коалгебры Homomorphsim в коалгебре Коната, но я борюсь с аспектом уникальности.it.

Для конкретности функтор F имеет вид: 

F : Set → Set
F X = Unit ⊎ X

Conat / Base.agda 

{-# OPTIONS --cubical --safe --guardedness #-}
module Cubical.Codata.Conat.Base where

open import Cubical.Data.Unit
open import Cubical.Data.Sum

open import Cubical.Core.Everything

record Conat : Set
Conat′ = Unit ⊎ Conat
record Conat where
  coinductive
  constructor conat′
  field force : Conat′
open Conat public

pattern zero  = inl tt
pattern suc n = inr n

conat : Conat′ → Conat
force (conat a) = a

succ : Conat → Conat
force (succ a) = suc a

succ′ : Conat′ → Conat′
succ′ n = suc λ where .force → n

pred′ : Conat′ → Conat′
pred′  zero   = zero
pred′ (suc x) = force x

pred′′ : Conat′ → Conat
force (pred′′ zero) = zero
pred′′ (suc x) = x

pred : Conat → Conat
force (pred x) = pred′ (force x)

Conat / Properties.agda (изменен, чтобы удалить irreleventвот где мой код) 

{-# OPTIONS --cubical --safe --guardedness #-}
module Cubical.Codata.Conat.Properties where

open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Empty
import Cubical.Data.DecreasingBinarySequence
import Cubical.Data.Nat
import Cubical.Data.Bool

open import Cubical.Core.Everything
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Path
open import Cubical.Foundations.Function

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq
open import Cubical.Codata.Conat.Base

module F-Coalgebra where

  -- definition of our functor F and Coalgebra stuff

  F : Set → Set
  F X = Unit ⊎ X

  F-map : {A B : Set} → (A → B) → (F A → F B)
  F-map f (inl tt) = inl tt
  F-map f (inr x) = inr (f x)

  F-Coalgebra : Set₁
  F-Coalgebra = Σ[ C ∈ Set ] (C → F C)

  coalgebraHomomorphism : (X Y : F-Coalgebra) → Set
  coalgebraHomomorphism (C , sc) (D , sd) = Σ[ f ∈ (C → D) ] F-map f ∘ sc ≡ sd ∘ f

  isTerminalCoalgebra : F-Coalgebra → Set₁
  isTerminalCoalgebra X = (Y : F-Coalgebra) → (isContr (coalgebraHomomorphism Y X))

  -- operations on Conat that might be useful

  module coit {S : Set} where
    coit : (S → F S) → S → Conat
    coit′ : (S → F S) → F S →  Conat′
    coit f s .force = coit′ f (f s)

    coit′ f (inl tt) = zero
    coit′ f (inr x) = suc (coit f x)

    -- this needs a proper name
    yesy : (sc : S → F S) → F-map (coit sc) ≡ coit′ sc
    yesy sc i (inl tt) = zero
    yesy sc i (suc x) = suc (coit sc x)

    coitSpec : (sc : S → F S) → (s : S) → F-map (coit sc) (sc s) ≡ force (coit sc s)
    coitSpec sc s i = yesy sc i (sc s)   

  inF : F Conat → Conat
  inF x .force = x

  ioF : (x : Conat) → inF (force x) ≡ x
  ioF x i .force = refl {x = force x} i

  caseF : (P : Conat → Set) → ((t : F Conat) → P (inF t)) → (x : Conat) → P x
  caseF P p x = subst P (ioF x) (p (force x))

  -- The specific Conat F-Coalgebra

  ConatCoalgebra : F-Coalgebra
  ConatCoalgebra = Conat , force 

  ConatCoalgebraTerminal : isTerminalCoalgebra ConatCoalgebra
  ConatCoalgebraTerminal (C , sc) = (coit.coit sc , λ i s → coit.coitSpec sc s i)
    , {!!}  -- notice the hole here, this is where I'm having trouble 
            -- proving the type of morphsisms is contractible

Конкретное место, в котором у меня возникли проблемы, отмечено дырой в конце второго файла.Определение isContr: 

isContr : Set ℓ → Set ℓ
isContr A = Σ[ x ∈ A ] (∀ y → x ≡ y)

Поскольку я использую кубический режим, можно показать, что равенство (фактически пути) совпадает с бисимуляцией.Я думаю, что это как-то дает мне коиндукцию, но я не знаю, как.

Также есть доказательства того, что Conat является hSet, который может или не может быть полезен для доказательства.

...