{-# OPTIONS --cubical #-} open import Cubical.Core.Everything postulate magic : ∀ {ℓ : Level} {X : Type ℓ} → X Square : ∀ {ℓ : Level} {A : Type ℓ} {x0 x1 y0 y1 : A} → (bottom : x0 ≡ x1) (top : y0 ≡ y1) (left : x0 ≡ y0) (right : x1 ≡ y1) → Type ℓ Square bottom top left right = (λ i → bottom i ≡ top i) [ left ≡ right ] {- LaTeX: Path_{i.A} (M; N) Agda: PathP (λ i → A) M N (λ i → A) [ M ≡ N ] Path A M N := PathP (λ _ → A) M N M ≡ N -} refl : ∀ {ℓ : Level} {A : Type ℓ} {x : A} → x ≡ x refl {x = x} = λ i → x conection-∨ : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} → (p : x ≡ y) → Square p refl p refl conection-∨ p h v = p (h ∨ v) -- \land conection-∧ : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} → (p : x ≡ y) → Square refl p refl p conection-∧ p h v = p (h ∧ v) open import Agda.Builtin.Bool partial₁ : ∀ (i j : I) → Partial i Bool -- i = 1 partial₁ i j (i = i1) = true partial₂ : ∀ i j → Partial (i ∨ j) Bool -- i ∨ j = 1 <---> (i = 1) ∨ (j = 1) partial₂ i j (i = i1) = true partial₂ i j (j = i1) = true partial₃ : ∀ (i j : I) → Partial (i ∨ ~ i) Bool -- i ∨ ~ i = 1 <---> (i = 1) ∨ (~ i = 1) <---> (i = 1) ∨ (i = 0) partial₃ i j (i = i1) = true partial₃ i j (i = i0) = false extension₁ : ∀ i j → Bool [ i ↦ partial₁ i j ] extension₁ i j = inS true {- extension₂ : ∀ i j → Bool [ i ↦ partial₂ i j ] extension₂ i j = inS true extension₃ : Bool [ i1 ↦ magic ] extension₃ = inS magic -} -- the next week starts from here myhfill : ∀ {ℓ : Level} {A : Type ℓ} {φ : I} → (walls : ∀ i → Partial φ A) → (bottom : A [ φ ↦ walls i0 ]) → (i : I) → A myhfill {A = A} {φ = φ} walls bottom i = hcomp new-walls new-bottom where new-walls : ∀ k → Partial (φ ∨ ~ i) A new-walls k (φ = i1) = walls (k ∧ i) 1=1 new-walls k (i = i0) = outS bottom new-bottom : A new-bottom = outS bottom _∙_ : ∀ {ℓ : Level} {A : Type ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z _∙_ = magic infixr 80 _∙_ !_ : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x !_ = magic infixr 100 !_ {- alternative one -} !'_ : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} → x ≡ y → y ≡ x !'_ = magic ∙-unit-r : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (q : x ≡ y) → q ∙ refl ≡ q ∙-unit-r = magic ∙-unit-l : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (q : x ≡ y) → refl ∙ q ≡ q ∙-unit-l = magic !-inv-l : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (p : x ≡ y) → (! p) ∙ p ≡ refl !-inv-l = magic !-inv-r : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (p : x ≡ y) → p ∙ (! p) ≡ refl !-inv-r = magic !-! : ∀ {ℓ : Level} {A : Type ℓ} {x y : A} (p : x ≡ y) → ! (! p) ≡ p !-! = magic ∙-assoc : ∀ {ℓ : Level} {A : Type ℓ} {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → (p ∙ q) ∙ r ≡ p ∙ (q ∙ r) ∙-assoc = magic