Experiments with cubical subtypes in Agda

Experiments.agda

{-# OPTIONS --cubical #-}
module Experiments where

open import Agda.Builtin.Cubical.Path public
open import Agda.Builtin.Cubical.Sub public renaming (primSubOut to ouc)
open import Agda.Primitive.Cubical public
  renaming ( primIMin       to _∧_  -- I → I → I
           ; primIMax       to _∨_  -- I → I → I
           ; primINeg       to -_   -- I → I
           ; isOneEmpty     to empty
           ; primComp       to comp
           ; primHComp      to hcomp
           ; primTransp     to transp
           ; itIsOne        to 1=1 )
import Agda.Builtin.Cubical.Glue

open import Agda.Primitive public
  using    ( Level )
  renaming ( lzero to ℓ-zero
           ; lsuc  to ℓ-suc
           ; _⊔_   to ℓ-max
           ; Setω  to Typeω )
open import Agda.Builtin.Sigma public

_[_↦_] : ∀ {ℓ} (A : Set ℓ) (φ : I) (u : Partial φ A) → Typeω
A [ φ ↦ u ] = Sub A φ u

infix 4 _[_↦_]

f : ∀ i → Partial (i ∨ - i) Set₁
f i (i = i0) = Set₀
f i (i = i1) = Set₀ → Set₀

leg : ∀ {ℓ} (A : Set ℓ) (a : A) → Typeω
leg A a = (i : I) → A [ - i ↦ (λ _ → a) ]

post : ∀ {ℓ} (A : Set ℓ) (a : A) → Typeω
post A a = (i : I) → A [ i ↦ (λ _ → a) ]

Path : ∀ {ℓ} (A : Set ℓ) → A → A → Set ℓ
Path A a b = PathP (λ _ → A) a b

fix : ∀ {ℓ} (A : Set ℓ) (a b : A) (p : Path A a b) → post A b
fix A a b p = λ i → inc (p i)

unfix : ∀ {ℓ} (A : Set ℓ) (a : A) (p : post A a) → Path A (ouc (p i0)) a
unfix A a p = λ i → ouc (p i)

post-cong : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A → B) {a : A} (p : post A a) → post B (f a)
post-cong f p = λ i → inc (f (ouc (p i)))

leg-inv : ∀ {ℓ} {A : Set ℓ} {a : A} (p : post A a) → leg A a
leg-inv p = λ i → p (- i)

Path′ : ∀ {ℓ} (A : Set ℓ) → A → A → Typeω
Path′ A a b = (i : I) → A [ i ∨ - i ↦ (λ { (i = i0) → a; (i = i1) → b }) ]

Path-Path′ : ∀ {ℓ} {A : Set ℓ} {a b : A} (p : Path A a b) → Path′ A a b
Path-Path′ p = λ i → inc (p i)

Path′-Path : ∀ {ℓ} {A : Set ℓ} {a b : A} (p : Path′ A a b) → Path A a b
Path′-Path p = λ i → ouc (p i)

Path-Path′-Path : ∀ {ℓ} {A : Set ℓ} {a b : A} (p : Path A a b) → Path (Path A a b) (Path′-Path (Path-Path′ p)) p
Path-Path′-Path p = λ _ → p

-- not works since Path′ A a b is in Typeω
--Path′-Path-Path′ : ∀ {ℓ} {A : Set ℓ} {a b : A} (p : Path′ A a b) → Path (Path′ A a b) (Path-Path′ (Path′-Path p)) p
--Path′-Path-Path′ p = λ _ → p