3

我在 Agda 中有一个 Conats 的定义（实际上它是立方体库中的那个）。我试图证明相关的 F 代数是（同伦）终端。

我已经设法将 F-Coalgebra Homomorphsim 的存在证明到 Conat 余代数中，但我正在努力解决它的独特性方面。

具体而言，函子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（修改为删除不相关的东西。这是我的代码所在的位置）

{-# 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 的证明，它可能对证明有用，也可能没用。

4

0 回答 0