PoorMansCubical.agda

{-# OPTIONS --without-K --rewriting --prop #-}

open import Agda.Primitive
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

variable
  ℓ : Level
  A B C : Set ℓ
  x y z : A


infix 4 _≡s_ _≡ss_
data _≡s_ {ℓ} {A : Set ℓ} (x : A) : A → SSet ℓ where
  instance
    refl : x ≡s x

data _≡ss_ {ℓ} {A : SSet ℓ} (x : A) : A → SSet ℓ where
  instance
    refl : x ≡ss x
{-# BUILTIN REWRITE _≡ss_ #-}

≡s→≡ : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡s y → x ≡ y
≡s→≡ refl = refl

sUIP : ∀ {ℓ} {A : Set ℓ} {x y : A} {p q : x ≡s y} → p ≡ss q
sUIP {p = refl} {q = refl} = refl

ssUIP : ∀ {ℓ} {A : SSet ℓ} {x y : A} {p q : x ≡ss y} → p ≡ss q
ssUIP {p = refl} {q = refl} = refl

data sNat : SSet lzero where
  zero : sNat
  suc  : sNat → sNat

postulate
  Nat→sNat : Nat → sNat
  zero→szero : Nat→sNat zero ≡ss zero
  suc→ssuc : ∀ n → Nat→sNat (suc n) ≡ss suc (Nat→sNat n)

{-# REWRITE zero→szero #-}
{-# REWRITE suc→ssuc #-}


postulate
  I : SSet lzero
  i0 i1 : I


variable
  i j k : I

infix 15 _∧_ _∨_

postulate
  _∧_ _∨_ : I → I → I
  i0∧ : i0 ∧ i ≡ss i0
  i1∧ : i1 ∧ i ≡ss i
  i0∨ : i0 ∨ i ≡ss i
  i1∨ : i1 ∨ i ≡ss i1
  ∧i0 : i ∧ i0 ≡ss i0
  ∧i1 : i ∧ i1 ≡ss i
  ∨i0 : i ∨ i0 ≡ss i
  ∨i1 : i ∨ i1 ≡ss i1

{-# REWRITE i0∧ i1∧ i0∨ i1∨ ∧i0 ∧i1 ∨i0 ∨i1 #-}

postulate
  1-_ : I → I
  1-i0 : 1- i0 ≡ss i1
  1-i1 : 1- i1 ≡ss i0

{-# REWRITE 1-i0 1-i1 #-}

module _ (φ : Prop) (A : I → Set) (u : φ → (i : I) → A i)
         (a₀ : A i0) (a₀-c : (p : φ) → u p i0 ≡s a₀) where
  postulate
    comp : A i1
    comp-c : (p : φ) → comp ≡s u p i1
  --{-# REWRITE comp-c #-}

{-# NO_UNIVERSE_CHECK #-}
record PathP {ℓ} (A : I → Set ℓ) (a0 : A i0) (a1 : A i1) : Set ℓ where
  field
    f : (i : I) → A i
    {{f0}} : f i0 ≡s a0
    {{f1}} : f i1 ≡s a1
open PathP

Path : (A : Set ℓ) → A → A → Set ℓ
Path A = PathP (λ _ → A)

reflP : {x : A} → PathP (λ _ → A) x x
f (reflP {x = x}) i = x

symP : {A : I → Set ℓ} {x : A i0} {y : A i1} → PathP A x y → PathP (λ i → A (1- i)) y x
f (symP p) i = f p (1- i)

transP : {A : Set ℓ} {x y z : A} → Path A x y → Path A y z → Path A x z
f (transP p q) i = comp {!!} {!!} {!!} {!!} {!!} {!!}
f0 (transP p q) = {!!}
f1 (transP p q) = {!!}