{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything

postulate
  magic : ∀ {ℓ : Level} {X : Type ℓ} → X

refl : ∀ {ℓ : Level} {A : Type ℓ} {x : A} → x ≡ x
refl {x = x} = λ i → x

_∙_ : ∀ {ℓ : Level} {A : Type ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
_∙_ {A = A} {x = x} p q j = hcomp (λ i → λ { (j = i0) → x ; (j = i1) → q i }) (p j)
infixr 80 _∙_

!_ : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x
!_ p i = p (~ i)
infixr 100 !_

-- in the diagram, φ = k ∨ ~ k where k is left to right

myhfill : ∀ {ℓ : Level} {A : Type ℓ} {φ : I}
  → (u : ∀ i → Partial φ A)
  → (u0 : A [ φ ↦ u i0 ])
  → (i : I) → A
myhfill {A = A} {φ = φ} u u0 i = hcomp walls bottom where
  walls : (j : I) → Partial (φ ∨ ~ i) A
  walls j (φ = i1) = u (i ∧ j) 1=1
  walls j (i = i0) = outS u0

  bottom : A
  bottom = outS u0

---------------------------------------------------------------

transport : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a
-- f = (λ x → f x)

transport-refl : ∀ {ℓ} {A : Type ℓ} (x : A) → transport refl x ≡ x
transport-refl {A = A} x i = transp (λ _ → A) i x
-- transp (λ i → A) i0 x ≡ transp (λ i → A) i1 x

squeeze : ∀ {ℓ} (A : I → Type ℓ) (i : I) → A i → A i1
squeeze A i a = transp (λ j → A (i ∨ j)) i0 a
-- i ? 0 --> i
-- i ? 1 --> 1

J : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {x : A} (B : (x' : A) → x ≡ x' → Type ℓ₂) (refl* : B x refl)
  {x' : A} (p : x ≡ x') → B x' p
J B refl* p = transp (λ i → B (p i) (λ j → p (i ∧ j))) i0 refl*

J-refl : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁} {x : A} (B : (x' : A) → x ≡ x' → Type ℓ₂) (refl* : B x refl)
  → J B refl* refl ≡ refl*
J-refl B refl* = transport-refl refl*

{- BONUS: define comp in terms of hcomp and transp -}

postulate
  mycomp : {ℓ : Level} (A : I → Type ℓ) -- A may change along the dimension
           {φ : I}
           (u : ∀ i → Partial φ (A i)) -- the type of u may change along the dimension
           (u0 : A i0 [ φ ↦ u i0 ])
           → A i1
  {- Hints: squeeze -}

---------------------------------------------------------------

-- Preparation for Homework 6 : (base ≡ base) ≃ Int

open import Agda.Builtin.Nat
open import Agda.Builtin.Int

-- "negsuc 0" means "-1"
-- "negsuc 3" means "-4"
succ : Int → Int
succ (pos n) = pos (suc n)
succ (negsuc 0) = pos 0
succ (negsuc (suc n)) = negsuc n

pred : Int → Int
pred = magic

succ-pred : ∀ i → succ (pred i) ≡ i
succ-pred = magic

pred-succ : ∀ i → pred (succ i) ≡ i
pred-succ = magic