text:
module Data.Num.Surjection where

open import Data.Num.Core
open import Data.Num.Continuous

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra

open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤)
    renaming (zero to z; suc to s)
open import Data.Fin.Properties using (toℕ-fromℕ≤; bounded)
open import Data.Product
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)

open import Function
open import Function.Surjection hiding (_∘_)
open Surjective
open import Function.Equality using (_⟶_; _⟨$⟩_)
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

-- fromℕ that preserves equality

-- ℕ⟶Num : ∀ {b d o}
--     → (True (Continuous? b (suc d) o))
--     → (val : ℕ)
--     → (True (o ≤? val))
--     → Num b (suc d) o

-- ℕ⟶Num : ∀ b d o → True (Continuous? b (suc d) o) → setoid ℕ ⟶ setoid (Num b (suc d) o)
-- ℕ⟶Num b d o cont = record
--     { _⟨$⟩_ = fromℕ cont
--     ; cong = cong (fromℕ cont)
--     }
--
-- -- Surjective? : ∀ b d o → (True (Continuous? b (suc d) o)) → Dec (Surjective (ℕ⟶Num b d o))
-- -- Surjective? b d o with Continuous? b (suc d) o
-- -- Surjective? b d o | yes cont = {!   !}
-- -- Surjective? b d o | no ¬cont = {!   !}
--
-- Num⟶ℕ-Surjective : ∀ b d o → (cont : True (Continuous? b (suc d) o)) → Surjective (Num⟶ℕ b (suc d) o)
-- Num⟶ℕ-Surjective b d o cont = record
--     { from = ℕ⟶Num b d o cont
--     ; right-inverse-of = {! toℕ-fromℕ cont  !}
--     }

-- Surjective? : ∀ b d o → Dec (Surjective (Num⟶ℕ b d o))
-- Surjective? b d o with surjectionView b d o
-- Surjective? b d o | Surj cond = yes (record
--     { from = ℕ⟶Num b d o
--     ; right-inverse-of = toℕ-fromℕ {b} {d} {o} {SurjCond⇒IsSurj cond}
--     })
-- Surjective? b d o | NonSurj reason = no (NonSurjCond⇏Surjective reason)
--

-- Conditions of surjectiveness
-- data SurjCond : ℕ → ℕ → ℕ → Set where
--     WithZerosUnary : ∀ {  d}               → (d≥2 : d ≥ 2) → SurjCond 1 d 0
--     WithZeros      : ∀ {b d} (b≥2 : b ≥ 2) → (d≥b : d ≥ b) → SurjCond b d 0
--     Zeroless       : ∀ {b d} (b≥1 : b ≥ 1) → (d≥b : d ≥ b) → SurjCond b d 1
--
-- -- Conditions of non-surjectiveness
-- data NonSurjCond : ℕ → ℕ → ℕ → Set where
--     Base≡0             : ∀ {  d o}                 → NonSurjCond 0 d o
--     NoDigits           : ∀ {b   o}                 → NonSurjCond b 0 o
--     Offset≥2           : ∀ {b d o} → o ≥ 2         → NonSurjCond b d o
--     UnaryWithOnlyZeros :                              NonSurjCond 1 1 0
--     NotEnoughDigits    : ∀ {b d o} → d ≥ 1 → d ≱ b → NonSurjCond b d o
--
-- data SurjectionView : ℕ → ℕ → ℕ → Set where
--     Surj    : ∀ {b d o} →    SurjCond b d o → SurjectionView b d o
--     NonSurj : ∀ {b d o} → NonSurjCond b d o → SurjectionView b d o
--
--
-- surjectionView : (b d o : ℕ) → SurjectionView b d o
-- surjectionView 0             d             o             = NonSurj Base≡0
-- surjectionView (suc b)       0             o             = NonSurj NoDigits
-- surjectionView (suc b)       (suc d)       o             with suc b ≤? suc d
-- surjectionView 1             1             0             | yes p = NonSurj UnaryWithOnlyZeros
-- surjectionView 1             (suc (suc d)) 0             | yes p = Surj    (WithZerosUnary (s≤s (s≤s z≤n)))
-- surjectionView (suc (suc b)) (suc d)       0             | yes p = Surj    (WithZeros (s≤s (s≤s z≤n)) p)
-- surjectionView (suc b)       (suc d)       1             | yes p = Surj    (Zeroless (s≤s z≤n) p)
-- surjectionView (suc b)       (suc d)       (suc (suc o)) | yes p = NonSurj (Offset≥2 (s≤s (s≤s z≤n)))
-- surjectionView (suc b)       (suc d)       o             | no ¬p = NonSurj (NotEnoughDigits (s≤s z≤n) ¬p)
--
-- IsSurjective : ℕ → ℕ → ℕ → Set
-- IsSurjective b d o with surjectionView b d o
-- IsSurjective b d o | Surj    _ = ⊤
-- IsSurjective b d o | NonSurj _ = ⊥
--
-- SurjCond⇒b≥1 : ∀ {b d o} → SurjCond b d o → b ≥ 1
-- SurjCond⇒b≥1 (WithZerosUnary d≥2)      = s≤s z≤n
-- SurjCond⇒b≥1 (WithZeros (s≤s b≥1) d≥b) = s≤s z≤n
-- SurjCond⇒b≥1 (Zeroless b≥1 d≥b)        = b≥1
--
-- SurjCond⇒d≥b : ∀ {b d o} → SurjCond b d o → d ≥ b
-- SurjCond⇒d≥b (WithZerosUnary (s≤s d≥1)) = s≤s z≤n
-- SurjCond⇒d≥b (WithZeros b≥2 d≥b)        = d≥b
-- SurjCond⇒d≥b (Zeroless b≥1 d≥b)         = d≥b
--
-- SurjCond⇒IsSurj : ∀ {b d o} → SurjCond b d o → IsSurjective b d o
-- SurjCond⇒IsSurj {b} {d} {o} cond with surjectionView b d o
-- SurjCond⇒IsSurj cond | Surj x = tt
-- SurjCond⇒IsSurj (WithZeros () d≥b)        | NonSurj Base≡0
-- SurjCond⇒IsSurj (Zeroless () d≥b)         | NonSurj Base≡0
-- SurjCond⇒IsSurj (WithZerosUnary ())       | NonSurj NoDigits
-- SurjCond⇒IsSurj (WithZeros () z≤n)        | NonSurj NoDigits
-- SurjCond⇒IsSurj (Zeroless () z≤n)         | NonSurj NoDigits
-- SurjCond⇒IsSurj (WithZerosUnary _)        | NonSurj (Offset≥2 ())
-- SurjCond⇒IsSurj (WithZeros _ _)           | NonSurj (Offset≥2 ())
-- SurjCond⇒IsSurj (Zeroless _ _)            | NonSurj (Offset≥2 (s≤s ()))
-- SurjCond⇒IsSurj (WithZerosUnary (s≤s ())) | NonSurj UnaryWithOnlyZeros
-- SurjCond⇒IsSurj (WithZeros (s≤s ()) _)    | NonSurj UnaryWithOnlyZeros
-- SurjCond⇒IsSurj (WithZerosUnary _)        | NonSurj (NotEnoughDigits d≥1 d≱1) = contradiction d≥1 d≱1
-- SurjCond⇒IsSurj (WithZeros _ d≥b)         | NonSurj (NotEnoughDigits _ d≱b) = contradiction d≥b d≱b
-- SurjCond⇒IsSurj (Zeroless _ d≥b)          | NonSurj (NotEnoughDigits _ d≱b) = contradiction d≥b d≱b
--
-- ------------------------------------------------------------------------
-- -- Operations on Num (which does not necessary needs to be Surj)
-- ------------------------------------------------------------------------
--
-- starting-digit : ∀ {b d o} → SurjCond b d o → Digit d
-- starting-digit (WithZerosUnary d≥2) = fromℕ≤ {1} d≥2
-- starting-digit (WithZeros b≥2 d≥b) = fromℕ≤ {1} (≤-trans b≥2 d≥b)
-- starting-digit (Zeroless b≥1 d≥b) = fromℕ≤ {0} (≤-trans b≥1 d≥b)

-- 1+ : ∀ {b d o} → Num b d o → Num b d o
-- 1+ {b} {d} {o} xs with surjectionView b d o
-- 1+ ∙        | Surj cond = starting-digit cond ∷ ∙
-- 1+ (x ∷ xs) | Surj cond with greatest x
-- 1+ (x ∷ xs) | Surj cond | yes p = digit+1-b-legacy x (SurjCond⇒b≥1 cond) p ∷ 1+ xs -- carry
-- 1+ (x ∷ xs) | Surj cond | no ¬p = digit+1   x ¬p                     ∷    xs
-- 1+ ∙        | NonSurj reason = ∙
-- 1+ (x ∷ xs) | NonSurj reason = xs
--
--
-- n+ : ∀ {b d o} → ℕ → Num b d o → Num b d o
-- n+ zero xs = xs
-- n+ (suc n) xs = 1+ (n+ n xs)
--
-- fromℕ : ∀ {b d o} → ℕ → Num b d o
-- fromℕ {b} {d} {o} n with surjectionView b d o
-- fromℕ n |    Surj x = n+ n ∙
-- fromℕ n | NonSurj x = ∙
--
--
-- -- fromℕ that preserves equality
-- ℕ⟶Num : ∀ b d o → setoid ℕ ⟶ setoid (Num b d o)
-- ℕ⟶Num b d o = record
--     { _⟨$⟩_ = fromℕ
--     ; cong = cong fromℕ
--     }
--
-- toℕ-digit+1-b : ∀ {d b} (x : Digit d)
--     → (b≥1 : b ≥ 1) → (p : suc (Fin.toℕ x) ≡ d)     -- required props
--     → Fin.toℕ (digit+1-b-legacy x b≥1 p) ≡ suc (Fin.toℕ x) ∸ b
-- toℕ-digit+1-b {d} {b} x b≥1 p = toℕ-fromℕ≤ $ start
--         suc (suc (Fin.toℕ x) ∸ b)
--     ≤⟨ s≤s (∸-mono ≤-refl b≥1) ⟩
--         suc (Fin.toℕ x)
--     ≈⟨ p ⟩
--         d
--     □
--
-- ------------------------------------------------------------------------
-- -- toℕ-1+ : toℕ (1+ xs) ≡ suc (toℕ xs)
-- ------------------------------------------------------------------------
--
-- toℕ-1+-x∷xs-greatest-lemma : ∀ {b d o}
--     → (x : Digit d) → (xs : Num b d o)
--     → (cond : SurjCond b d o)
--     → (p : suc (Fin.toℕ x) ≡ d)
--     → (toℕ-1+-xs : toℕ (1+ xs) ≡ suc (toℕ xs))
--     → toℕ (digit+1-b-legacy x (SurjCond⇒b≥1 cond) p ∷ 1+ xs) ≡ suc (toℕ (x ∷ xs))
-- toℕ-1+-x∷xs-greatest-lemma {b} {d} {o} x xs cond p toℕ-1+-xs =
--     begin
--         toℕ (digit+1-b-legacy x (SurjCond⇒b≥1 cond) p ∷ 1+ xs)
--     -- toℕ-fromℕ≤ : toℕ (fromℕ≤ m<n) ≡ m
--     ≡⟨ cong (λ w → o + w + toℕ (1+ xs) * b) (toℕ-fromℕ≤ ((digit+1-b-legacy-lemma x (SurjCond⇒b≥1 cond) p))) ⟩
--         o + (suc (Fin.toℕ x) ∸ b) + toℕ (1+ xs) * b
--     -- induction hypothesis
--     ≡⟨ cong (λ w → o + (suc (Fin.toℕ x) ∸ b) + w * b) toℕ-1+-xs ⟩
--         o + (suc (Fin.toℕ x) ∸ b) + (b + toℕ xs * b)
--     ≡⟨ +-assoc o (suc (Fin.toℕ x) ∸ b) (b + toℕ xs * b) ⟩
--         o + (suc (Fin.toℕ x) ∸ b + (b + toℕ xs * b))
--     ≡⟨ cong (λ w → o + w) (sym (+-assoc (suc (Fin.toℕ x) ∸ b) b (toℕ xs * b))) ⟩
--         o + (suc (Fin.toℕ x) ∸ b + b + toℕ xs * b)
--     ≡⟨ cong (λ w → o + (w + toℕ xs * b)) (+-comm (suc (Fin.toℕ x) ∸ b) b) ⟩
--         o + (b + (suc (Fin.toℕ x) ∸ b) + toℕ xs * b)
--     -- m+n∸m≡n : m + (n ∸ m) ≡ n
--     ≡⟨ cong (λ w → o + (w + toℕ xs * b)) (m+n∸m≡n (
--             start
--                 b
--             ≤⟨ SurjCond⇒d≥b cond ⟩
--                 d
--             ≈⟨ sym p ⟩
--                 suc (Fin.toℕ x)
--             □)) ⟩
--         o + suc (Fin.toℕ x + toℕ xs * b)
--     ≡⟨ +-suc o (Fin.toℕ x + toℕ xs * b) ⟩
--         suc (o + (Fin.toℕ x + toℕ xs * b))
--     ≡⟨ cong suc (sym (+-assoc o (Fin.toℕ x) (toℕ xs * b))) ⟩
--         suc (o + Fin.toℕ x + toℕ xs * b)
--     ∎
--
-- toℕ-1+-x∷xs-not-greatest-lemma : ∀ {b d o}
--     → (x : Digit d) → (xs : Num b d o)
--     → (¬p : suc (Fin.toℕ x) ≢ d)
--     → toℕ (digit+1 x ¬p ∷ xs) ≡ suc (toℕ (x ∷ xs))
-- toℕ-1+-x∷xs-not-greatest-lemma {b} {d} {o} x xs ¬p =
--     begin
--         o + Fin.toℕ (fromℕ≤ (≤∧≢⇒< (bounded x) ¬p)) + toℕ xs * b
--     -- toℕ-fromℕ≤
--     ≡⟨ cong (λ w → o + w + toℕ xs * b) (toℕ-fromℕ≤ (≤∧≢⇒< (bounded x) ¬p)) ⟩
--         o + suc (Fin.toℕ x) + toℕ xs * b
--     ≡⟨ +-assoc o (suc (Fin.toℕ x)) (toℕ xs * b) ⟩
--         o + suc (Fin.toℕ x + toℕ xs * b)
--     ≡⟨ +-suc o (Fin.toℕ x + toℕ xs * b) ⟩
--         suc (o + (Fin.toℕ x + toℕ xs * b))
--     ≡⟨ cong suc (sym (+-assoc o (Fin.toℕ x) (toℕ xs * b))) ⟩
--         suc (o + Fin.toℕ x + toℕ xs * b)
--     ∎
--
-- toℕ-1+ : ∀ {b d o}
--     → {isSurj : IsSurjective b d o}
--     → (xs : Num b d o)
--     → toℕ (1+ xs) ≡ suc (toℕ xs)
-- toℕ-1+ {b} {d} {o} xs with surjectionView b d o
-- toℕ-1+ {1} {d} {0} ∙ | Surj (WithZerosUnary d≥2) =
--     begin
--         Fin.toℕ (fromℕ≤ d≥2) + zero
--     ≡⟨ +-right-identity (Fin.toℕ (fromℕ≤ d≥2)) ⟩
--         Fin.toℕ (fromℕ≤ d≥2)
--     ≡⟨ toℕ-fromℕ≤ d≥2 ⟩
--         suc zero
--     ∎
-- toℕ-1+ {b} {d} {0} ∙ | Surj (WithZeros b≥2 d≥b) =
--     begin
--         Fin.toℕ (fromℕ≤ (≤-trans b≥2 d≥b)) + zero * b
--     ≡⟨ +-right-identity (Fin.toℕ (fromℕ≤ (≤-trans b≥2 d≥b))) ⟩
--         Fin.toℕ (fromℕ≤ (≤-trans b≥2 d≥b))
--     ≡⟨ toℕ-fromℕ≤ (≤-trans b≥2 d≥b) ⟩
--         suc zero
--     ∎
-- toℕ-1+ {b} {d} {_} ∙ | Surj (Zeroless b≥1 d≥b) =
--     begin
--         suc (Fin.toℕ (fromℕ≤ (≤-trans b≥1 d≥b)) + zero)
--     ≡⟨ +-right-identity (suc (Fin.toℕ (fromℕ≤ (≤-trans b≥1 d≥b)))) ⟩
--         suc (Fin.toℕ (fromℕ≤ (≤-trans b≥1 d≥b)))
--     ≡⟨ cong suc (toℕ-fromℕ≤ (≤-trans b≥1 d≥b)) ⟩
--         suc zero
--     ∎
-- toℕ-1+ {b} {d} {o} (x ∷ xs) | Surj condition with greatest x
-- toℕ-1+ {b} {d} {o} (x ∷ xs) | Surj condition | yes p = toℕ-1+-x∷xs-greatest-lemma x xs condition p (toℕ-1+ {isSurj = SurjCond⇒IsSurj condition} xs)
-- toℕ-1+ {b} {d} {o} (x ∷ xs) | Surj condition | no ¬p = toℕ-1+-x∷xs-not-greatest-lemma x xs ¬p
-- toℕ-1+ {isSurj = ()} xs | NonSurj reason
--
-- ------------------------------------------------------------------------
-- -- toℕ-n+ : toℕ (n+ n xs) ≡ n + (toℕ xs)
-- ------------------------------------------------------------------------
--
-- toℕ-n+ : ∀ {b d o}
--     → {isSurj : IsSurjective b d o}
--     → (n : ℕ)
--     → (xs : Num b d o)
--     → toℕ (n+ n xs) ≡ n + (toℕ xs)
-- toℕ-n+ {b} {d} {o} n xs with surjectionView b d o
-- toℕ-n+ zero xs | Surj cond = refl
-- toℕ-n+ (suc n) xs | Surj cond =
--     begin
--         toℕ (n+ (suc n) xs)
--     ≡⟨ refl ⟩
--         toℕ (1+ (n+ n xs))
--     ≡⟨ toℕ-1+ {isSurj = SurjCond⇒IsSurj cond} (n+ n xs) ⟩
--         suc (toℕ (n+ n xs))
--     ≡⟨ cong suc (toℕ-n+ {isSurj = SurjCond⇒IsSurj cond} n xs) ⟩
--         suc (n + toℕ xs)
--     ∎
-- toℕ-n+ {isSurj = ()} n xs | NonSurj reason
--
-- ------------------------------------------------------------------------
-- -- toℕ-fromℕ : toℕ (fromℕ n) ≡ n
-- ------------------------------------------------------------------------
--
-- toℕ-fromℕ : ∀ {b d o}
--     → {isSurjective : IsSurjective b d o}
--     → (n : ℕ)
--     → toℕ (fromℕ {b} {d} {o} n) ≡ n
-- toℕ-fromℕ {b} {d} {o} n       with surjectionView b d o
-- toℕ-fromℕ             zero    | Surj (WithZerosUnary d≥2) = refl
-- toℕ-fromℕ {_} {d} {_} (suc n) | Surj (WithZerosUnary d≥2) =
--     begin
--         toℕ (1+ (n+ {1} {d} {0} n ∙))
--     ≡⟨ toℕ-1+ {1} {d} {0} {SurjCond⇒IsSurj (WithZerosUnary d≥2)} (n+ n ∙) ⟩
--         suc (toℕ (n+ n ∙))
--     ≡⟨ cong suc (toℕ-n+ {1} {d} {0} {SurjCond⇒IsSurj (WithZerosUnary d≥2)} n ∙) ⟩
--         suc (n + zero)
--     ≡⟨ cong suc (+-right-identity n) ⟩
--         suc n
--     ∎
-- toℕ-fromℕ             zero    | Surj (WithZeros b≥2 d≥b) = refl
-- toℕ-fromℕ {b} {d} {_} (suc n) | Surj (WithZeros b≥2 d≥b) =
--     begin
--         toℕ (1+ (n+ {b} {d} {0} n ∙))
--     ≡⟨ toℕ-1+ {b} {d} {0} {SurjCond⇒IsSurj (WithZeros b≥2 d≥b)} (n+ n ∙) ⟩
--         suc (toℕ (n+ n ∙))
--     ≡⟨ cong suc (toℕ-n+ {b} {d} {0} {SurjCond⇒IsSurj (WithZeros b≥2 d≥b)} n ∙) ⟩
--         suc (n + zero)
--     ≡⟨ cong suc (+-right-identity n) ⟩
--         suc n
--     ∎
-- toℕ-fromℕ {b} {d} {_} zero    | Surj (Zeroless b≥1 d≥b) = refl
-- toℕ-fromℕ {b} {d} {_} (suc n) | Surj (Zeroless b≥1 d≥b) =
--     begin
--         toℕ (1+ (n+ {b} {d} {1} n ∙))
--     ≡⟨ toℕ-1+ {b} {d} {1} {SurjCond⇒IsSurj (Zeroless b≥1 d≥b)} (n+ n ∙) ⟩
--         suc (toℕ (n+ n ∙))
--     ≡⟨ cong suc (toℕ-n+ {b} {d} {1} {SurjCond⇒IsSurj (Zeroless b≥1 d≥b)} n ∙) ⟩
--         suc (n + zero)
--     ≡⟨ cong suc (+-right-identity n) ⟩
--         suc n
--     ∎
-- toℕ-fromℕ {isSurjective = ()} n | NonSurj x
--
--
-- ------------------------------------------------------------------------
-- -- Lemmata for proving Spurious cases not surjective
-- ------------------------------------------------------------------------
--
-- NonSurjCond-Base≡0 : ∀ {d o} → (xs : Num 0 d o) → toℕ xs ≢ suc (o + d)
-- NonSurjCond-Base≡0 {d} {o} ∙        ()
-- NonSurjCond-Base≡0 {d} {o} (x ∷ xs) p = contradiction p (<⇒≢ ⟦x∷xs⟧<1+o+d)
--     where
--         ⟦x∷xs⟧<1+o+d : o + Fin.toℕ x + toℕ xs * 0 < suc (o + d)
--         ⟦x∷xs⟧<1+o+d = s≤s $
--             start
--                 o + Fin.toℕ x + toℕ xs * zero
--             ≈⟨ cong (λ w → o + Fin.toℕ x + w) (*-right-zero (toℕ xs)) ⟩
--                 o + Fin.toℕ x + zero
--             ≈⟨ +-right-identity (o + Fin.toℕ x) ⟩
--                 o + Fin.toℕ x
--             ≤⟨ n+-mono o (
--                 start
--                     Fin.toℕ x
--                 ≤⟨ n≤1+n (Fin.toℕ x) ⟩
--                     suc (Fin.toℕ x)
--                 ≤⟨ bounded x ⟩
--                     d
--                 □
--             )⟩
--                 o + d
--             □
--
-- NonSurjCond-NoDigits : ∀ {b o} → (xs : Num b 0 o) → toℕ xs ≢ 1
-- NonSurjCond-NoDigits ∙         ()
-- NonSurjCond-NoDigits (() ∷ xs)
--
-- NonSurjCond-Offset≥2 : ∀ {b d o} → o ≥ 2 → (xs : Num b d o) → toℕ xs ≢ 1
-- NonSurjCond-Offset≥2                   o≥2      ∙        ()
-- NonSurjCond-Offset≥2 {o = 0}           ()       (x ∷ xs) p
-- NonSurjCond-Offset≥2 {o = 1}           (s≤s ()) (x ∷ xs) p
-- NonSurjCond-Offset≥2 {o = suc (suc o)} o≥2      (x ∷ xs) ()
--
-- NonSurjCond-UnaryWithOnlyZeros : (xs : Num 1 1 0) → toℕ xs ≢ 1
-- NonSurjCond-UnaryWithOnlyZeros ∙ ()
-- NonSurjCond-UnaryWithOnlyZeros (z ∷ xs) p = contradiction (
--     begin
--         toℕ xs
--     ≡⟨ sym (*-right-identity (toℕ xs)) ⟩
--         toℕ xs * 1
--     ≡⟨ p ⟩
--         suc zero
--     ∎) (NonSurjCond-UnaryWithOnlyZeros xs)
-- NonSurjCond-UnaryWithOnlyZeros (s () ∷ xs)
--
-- NonSurjCond-NotEnoughDigits : ∀ {b d o} → d ≥ 1 → b ≰ d → (xs : Num b d o) → toℕ xs ≢ o + d
-- NonSurjCond-NotEnoughDigits {_} {_} {o} d≥1 b≰d ∙        = <⇒≢ (≤-steps o d≥1)
-- NonSurjCond-NotEnoughDigits {b} {d} {o} d≥1 b≰d (x ∷ xs) p with toℕ xs ≤? 0
-- NonSurjCond-NotEnoughDigits {b} {d} {o} d≥1 b≰d (x ∷ xs) p | yes q =
--     contradiction p (<⇒≢ ⟦x∷xs⟧>o+d)
--     where
--         ⟦xs⟧≡0 : toℕ xs ≡ 0
--         ⟦xs⟧≡0 = ≤0⇒≡0 (toℕ xs) q
--         ⟦x∷xs⟧>o+d : o + Fin.toℕ x + toℕ xs * b < o + d
--         ⟦x∷xs⟧>o+d = start
--                 suc (o + Fin.toℕ x + toℕ xs * b)
--             ≈⟨ begin
--                     suc (o + Fin.toℕ x + toℕ xs * b)
--                 ≡⟨ cong (λ w → suc (o + Fin.toℕ x + w * b)) ⟦xs⟧≡0 ⟩
--                     suc (o + Fin.toℕ x + zero)
--                 ≡⟨ +-right-identity (suc (o + Fin.toℕ x)) ⟩
--                     suc (o + Fin.toℕ x)
--                 ≡⟨ sym (+-suc o (Fin.toℕ x)) ⟩
--                     o + suc (Fin.toℕ x)
--                 ∎ ⟩
--                 o + suc (Fin.toℕ x)
--             ≤⟨ n+-mono o (bounded x) ⟩
--                 o + d
--             □
--
-- NonSurjCond-NotEnoughDigits {b} {d} {o} d≥1 b≰d (x ∷ xs) p | no ¬q =
--     contradiction p (>⇒≢ ⟦x∷xs⟧>o+d)
--     where
--         ⟦x∷xs⟧>o+d : o + Fin.toℕ x + toℕ xs * b > o + d
--         ⟦x∷xs⟧>o+d = start
--                 suc (o + d)
--             ≈⟨ sym (+-suc o d) ⟩
--                 o + suc d
--             ≤⟨ n+-mono o (
--                 start
--                     suc d
--                 ≤⟨ ≰⇒> b≰d ⟩
--                     b
--                 ≈⟨ sym (*-left-identity b) ⟩
--                     1 * b
--                 ≤⟨ _*-mono_ {1} {toℕ xs} {b} {b} (≰⇒> ¬q) ≤-refl ⟩
--                     toℕ xs * b
--                 ≤⟨ n≤m+n (Fin.toℕ x) (toℕ xs * b) ⟩
--                     Fin.toℕ x + toℕ xs * b
--                 □
--             ) ⟩
--                 o + (Fin.toℕ x + toℕ xs * b)
--             ≈⟨ sym (+-assoc o (Fin.toℕ x) (toℕ xs * b)) ⟩
--                 o + Fin.toℕ x + toℕ xs * b
--             □
--
-- NonSurjCond⇏Surjective : ∀ {b} {d} {o} → NonSurjCond b d o → ¬ (Surjective (Num⟶ℕ b d o))
-- NonSurjCond⇏Surjective {_} {d} {o} Base≡0  claim =
--     NonSurjCond-Base≡0
--         (from             claim ⟨$⟩ suc o + d)
--         (right-inverse-of claim   (suc (o + d)))
-- NonSurjCond⇏Surjective NoDigits claim =
--     NonSurjCond-NoDigits
--         (from             claim ⟨$⟩ 1)
--         (right-inverse-of claim     1)
-- NonSurjCond⇏Surjective (Offset≥2 p) claim =
--     NonSurjCond-Offset≥2 p
--         (from             claim ⟨$⟩ 1)
--         (right-inverse-of claim     1)
-- NonSurjCond⇏Surjective UnaryWithOnlyZeros claim =
--     NonSurjCond-UnaryWithOnlyZeros
--         (from             claim ⟨$⟩ 1)
--         (right-inverse-of claim     1)
-- NonSurjCond⇏Surjective {_} {d} {o} (NotEnoughDigits p q) claim =
--     NonSurjCond-NotEnoughDigits p q
--         (from             claim ⟨$⟩ o + d)
--         (right-inverse-of claim    (o + d))
--
-- SurjCond⇒Surjective : ∀ {b} {d} {o} → SurjCond b d o → Surjective (Num⟶ℕ b d o)
-- SurjCond⇒Surjective {b} {d} {o} cond = record
--     { from = ℕ⟶Num b d o
--     ; right-inverse-of = toℕ-fromℕ {b} {d} {o} {SurjCond⇒IsSurj cond}
--     }
--
-- Surjective? : ∀ b d o → Dec (Surjective (Num⟶ℕ b d o))
-- Surjective? b d o with surjectionView b d o
-- Surjective? b d o | Surj cond = yes (record
--     { from = ℕ⟶Num b d o
--     ; right-inverse-of = toℕ-fromℕ {b} {d} {o} {SurjCond⇒IsSurj cond}
--     })
-- Surjective? b d o | NonSurj reason = no (NonSurjCond⇏Surjective reason)
--
-- ------------------------------------------------------------------------
-- --
-- ------------------------------------------------------------------------
--
-- -- Surjective⇒SurjCond {b} {d} {o} surj = {!   !}
-- Surjective⇒SurjCond : ∀ {b} {d} {o}
--     → Surjective (Num⟶ℕ b d o)
--     → SurjCond b d o
-- Surjective⇒SurjCond {b} {d} {o} surj with surjectionView b d o
-- Surjective⇒SurjCond surj | Surj condition = condition
-- Surjective⇒SurjCond surj | NonSurj reason = contradiction surj (NonSurjCond⇏Surjective reason)
--
-- Surjective⇒IsSurj : ∀ {b} {d} {o} → Surjective (Num⟶ℕ b d o) → IsSurjective b d o
-- Surjective⇒IsSurj = SurjCond⇒IsSurj ∘ Surjective⇒SurjCond
--
-- Surjective⇒b≥1 : ∀ {b} {d} {o} → Surjective (Num⟶ℕ b d o) → b ≥ 1
-- Surjective⇒b≥1 = SurjCond⇒b≥1 ∘ Surjective⇒SurjCond
--
-- Surjective⇒d≥b : ∀ {b} {d} {o} → Surjective (Num⟶ℕ b d o) → b ≤ d
-- Surjective⇒d≥b = SurjCond⇒d≥b ∘ Surjective⇒SurjCond

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Localization where

open import Cubical.HITs.Localization.Base public

open import Cubical.HITs.Localization.Properties public

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
data ⊥ : Set where

postulate
  ∞  : ∀ {a} → Set a → Set a
  ♯_ : ∀ {a} {A : Set a} → (A → ⊥) → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A → ⊥

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

-- Issue #5610: with these bad types for sharp and flat, we can prove
-- false. The reason is that ∞ is assumed to be strictly-positive in
-- the positivity checker (even guarding positive). So making ∞ A
-- isomorphic to A → ⊥ will be contradictory to this assumption.

data D : Set where
  wrap : ∞ D → D

lam : (D → ⊥) → D
lam f = wrap (♯ f)

app : D → D → ⊥
app (wrap g) d = ♭ g d

delta : D
delta = lam (λ x → app x x)

omega : ⊥
omega = app delta delta

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- Andreas, 2021-08-19, issue #5283, reported by guilhermehas

-- 'tactic' should only appear in attributes and 'C.Tactic' is converted to
-- 'TacticAttribute' there.
-- Other occurrences of 'C.Tactic' should be a scope error.
-- At the time of writing, the scope checker passes it as A.Tactic to the type
-- checker, and that loops on it.

open import Agda.Builtin.Reflection

A : Set
A = tactic ?

-- Should be syntax error.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Builtin.Equality

postulate @0 A : Set

@0 f : (X : Set) → A ≡ X → Set
f X refl = {!!}


text:
{-# OPTIONS --no-positivity-check
            --no-termination-check
  #-}

-- A universe setoids
module Setoid where

import Chain

record True : Set where
data False : Set where

Rel : Set -> Set1
Rel A = A -> A -> Set

Pred : Set -> Set1
Pred A = A -> Set

Resp : {A : Set} -> Rel A -> {B : Set} -> Rel B -> Pred (A -> B)
Resp _R_ _S_ f = forall x y -> x R y -> f x S f y

mutual

  infix 40 _=El=_ _=S=_ _=Fam=_
  infix 60 _!_

  data Setoid : Set where
    nat : Setoid
    Π   : (A : Setoid)(F : Fam A) -> Setoid
    Σ   : (A : Setoid)(F : Fam A) -> Setoid

  data Fam (A : Setoid) : Set where
    fam : (F : El A -> Setoid) ->
          Resp _=El=_ _=S=_ F -> Fam A

  data El : Setoid -> Set where
    zero : El nat
    suc  : El nat -> El nat
    ƛ    : {A : Setoid}{F : Fam A}
           (f : (x : El A) -> El (F ! x)) ->
           ((x y : El A) -> x =El= y -> f x =El= f y) -> El (Π A F)
    _,_  : {A : Setoid}{F : Fam A}(x : El A) -> El (F ! x) -> El (Σ A F)

  data _=S=_ : (A B : Setoid) -> Set where
    eqNat : nat =S= nat
    eqΠ   : {A₁ A₂ : Setoid}{F₁ : Fam A₁}{F₂ : Fam A₂} ->
             A₂ =S= A₁ -> F₁ =Fam= F₂ -> Π A₁ F₁ =S= Π A₂ F₂
    eqΣ   : {A₁ A₂ : Setoid}{F₁ : Fam A₁}{F₂ : Fam A₂} ->
            A₁ =S= A₂ -> F₁ =Fam= F₂ -> Σ A₁ F₁ =S= Σ A₂ F₂

  data _=El=_ : {A B : Setoid} -> El A -> El B -> Set where
    eqInNat : {n : El nat} -> n =El= n
    eqInΠ   : {A₁ A₂ : Setoid}{F₁ : Fam A₁}{F₂ : Fam A₂}
              {f₁ : (x : El A₁) -> El (F₁ ! x)}
              {pf₁ : (x y : El A₁) -> x =El= y -> f₁ x =El= f₁ y}
              {f₂ : (x : El A₂) -> El (F₂ ! x)} ->
              {pf₂ : (x y : El A₂) -> x =El= y -> f₂ x =El= f₂ y} ->
              A₂ =S= A₁ ->
              ((x : El A₁)(y : El A₂) -> x =El= y -> f₁ x =El= f₂ y) ->
              ƛ f₁ pf₁ =El= ƛ f₂ pf₂
    eqInΣ   : {A₁ A₂ : Setoid}{F₁ : Fam A₁}{F₂ : Fam A₂}
              {x₁ : El A₁}{y₁ : El (F₁ ! x₁)}
              {x₂ : El A₂}{y₂ : El (F₂ ! x₂)} ->
              F₁ =Fam= F₂ -> x₁ =El= x₂ -> y₁ =El= y₂ -> (x₁ , y₁) =El= (x₂ , y₂)

  data _=Fam=_ {A B : Setoid}(F : Fam A)(G : Fam B) : Set where
    eqFam : B =S= A -> (forall x y -> x =El= y -> F ! x =S= G ! y) -> F =Fam= G

  _!_ : {A : Setoid} -> Fam A -> El A -> Setoid
  fam F _ ! x = F x

-- Inversions
famEqDom : {A B : Setoid}{F : Fam A}{G : Fam B} -> F =Fam= G -> B =S= A
famEqDom (eqFam p _) = p

famEqCodom : {A B : Setoid}{F : Fam A}{G : Fam B} -> F =Fam= G ->
        (x : El A)(y : El B) -> x =El= y -> F ! x =S= G ! y
famEqCodom (eqFam _ p) = p

eqΠ-inv₁ : {A₁ A₂ : Setoid}{F₁ : Fam A₁}{F₂ : Fam A₂} ->
           Π A₁ F₁ =S= Π A₂ F₂ -> A₂ =S= A₁
eqΠ-inv₁ (eqΠ p _) = p

eqΠ-inv₂ : {A₁ A₂ : Setoid}{F₁ : Fam A₁}{F₂ : Fam A₂} ->
           Π A₁ F₁ =S= Π A₂ F₂ -> F₁ =Fam= F₂
eqΠ-inv₂ (eqΠ _ p) = p

eqΣ-inv₁ : {A₁ A₂ : Setoid}{F₁ : Fam A₁}{F₂ : Fam A₂} ->
           Σ A₁ F₁ =S= Σ A₂ F₂ -> A₁ =S= A₂
eqΣ-inv₁ (eqΣ p _) = p

eqΣ-inv₂ : {A₁ A₂ : Setoid}{F₁ : Fam A₁}{F₂ : Fam A₂} ->
           Σ A₁ F₁ =S= Σ A₂ F₂ -> F₁ =Fam= F₂
eqΣ-inv₂ (eqΣ _ p) = p

-- Equivalence proofs and casts
mutual

  -- _=Fam=_ is an equivalence
  =Fam=-refl : {A : Setoid}{F : Fam A} -> F =Fam= F
  =Fam=-refl {F = fam _ p} = eqFam =S=-refl p

  =Fam=-sym : {A B : Setoid}{F : Fam A}{G : Fam B} -> F =Fam= G -> G =Fam= F
  =Fam=-sym (eqFam B=A F=G) = eqFam (=S=-sym B=A) \x y x=y -> =S=-sym (F=G _ _ (=El=-sym x=y))

  =Fam=-trans : {A B C : Setoid}{F : Fam A}{G : Fam B}{H : Fam C} ->
                F =Fam= G -> G =Fam= H -> F =Fam= H
  =Fam=-trans (eqFam B=A F=G) (eqFam C=B G=H) =
    eqFam (=S=-trans C=B B=A) \x y x=y ->
           =S=-trans (F=G x (B=A << x) (cast-id _))
                     (G=H _ y (=El=-trans (=El=-sym (cast-id _)) x=y))

  -- _=S=_ is an equivalence
  =S=-refl : {A : Setoid} -> A =S= A
  =S=-refl {nat}   = eqNat
  =S=-refl {Π A F} = eqΠ =S=-refl =Fam=-refl
  =S=-refl {Σ A F} = eqΣ =S=-refl =Fam=-refl

  =S=-sym : {A B : Setoid} -> A =S= B -> B =S= A
  =S=-sym eqNat = eqNat
  =S=-sym (eqΠ pA pF) = eqΠ (=S=-sym pA) (=Fam=-sym pF)
  =S=-sym (eqΣ pA pF) = eqΣ (=S=-sym pA) (=Fam=-sym pF)

  =S=-trans : {A B C : Setoid} -> A =S= B -> B =S= C -> A =S= C
  =S=-trans eqNat eqNat = eqNat
  =S=-trans (eqΠ B=A F=G) (eqΠ C=B G=H) = eqΠ (=S=-trans C=B B=A) (=Fam=-trans F=G G=H)
  =S=-trans (eqΣ A=B F=G) (eqΣ B=C G=H) = eqΣ (=S=-trans A=B B=C) (=Fam=-trans F=G G=H)

  -- _=El=_ is an equivalence
  =El=-refl : {A : Setoid}{x : El A} -> x =El= x
  =El=-refl {nat}   = eqInNat
  =El=-refl {Π A F}{ƛ f pf} = eqInΠ =S=-refl pf
  =El=-refl {Σ A F}{x , y}  = eqInΣ =Fam=-refl =El=-refl =El=-refl

  =El=-sym : {A B : Setoid}{x : El A}{y : El B} -> x =El= y -> y =El= x
  =El=-sym eqInNat = eqInNat
  =El=-sym (eqInΠ B=A p) = eqInΠ (=S=-sym B=A) \x y x=y -> =El=-sym (p y x (=El=-sym x=y))
  =El=-sym (eqInΣ pF px py) = eqInΣ (=Fam=-sym pF) (=El=-sym px) (=El=-sym py)

  =El=-trans : {A B C : Setoid}{x : El A}{y : El B}{z : El C} ->
             x =El= y -> y =El= z -> x =El= z
  =El=-trans eqInNat eqInNat = eqInNat
  =El=-trans (eqInΠ B=A f=g) (eqInΠ C=B g=h) =
    eqInΠ (=S=-trans C=B B=A) \x y x=y ->
      =El=-trans (f=g x (B=A << x) (cast-id _))
               (g=h _ y (=El=-trans (=El=-sym (cast-id _)) x=y))
  =El=-trans (eqInΣ F₁=F₂ x₁=x₂ y₁=y₂) (eqInΣ F₂=F₃ x₂=x₃ y₂=y₃) =
    eqInΣ (=Fam=-trans F₁=F₂ F₂=F₃) (=El=-trans x₁=x₂ x₂=x₃) (=El=-trans y₁=y₂ y₂=y₃)

  -- Casting. Important: don't look at the proof!
  infix 50 _<<_ _>>_

  _<<_ : {A B : Setoid} -> A =S= B -> El B -> El A
  _<<_ {nat}{Π _ _}   () _
  _<<_ {nat}{Σ _ _}   () _
  _<<_ {Π _ _}{nat}   () _
  _<<_ {Π _ _}{Σ _ _} () _
  _<<_ {Σ _ _}{nat}   () _
  _<<_ {Σ _ _}{Π _ _} () _
  _<<_ {nat}{nat} p x = x
  _<<_ {Π A₁ F₁}{Π A₂ F₂} p (ƛ f pf) = ƛ g pg
    where
      g : (x : El A₁) -> El (F₁ ! x)
      g x = let A₂=A₁ = eqΠ-inv₁ p
                F₁=F₂ = famEqCodom (eqΠ-inv₂ p) x _ (cast-id _)
            in  F₁=F₂ << f (A₂=A₁ << x)

      pg : (x y : El A₁) -> x =El= y -> g x =El= g y
      pg x y x=y = cast-irr _ _ (pf _ _ (cast-irr _ _ x=y))

  _<<_ {Σ A₁ F₁}{Σ A₂ F₂} p (x , y) = eqΣ-inv₁ p << x , F₁=F₂ << y
    where
      F₁=F₂ : F₁ ! (eqΣ-inv₁ p << x) =S= F₂ ! x
      F₁=F₂ = famEqCodom (eqΣ-inv₂ p) _ _ (=El=-sym (cast-id _))

  _>>_ : {A B : Setoid} -> Fam A -> A =S= B -> Fam B
  fam F pF >> A=B = fam G pG
    where
      G : El _ -> Setoid
      G y = F (A=B << y)

      pG : forall x y -> x =El= y -> G x =S= G y
      pG x y x=y = pF _ _ (cast-irr _ _ x=y)

  cast-id : {A B : Setoid}{x : El A}(p : B =S= A) -> x =El= p << x
  cast-id eqNat = eqInNat
  cast-id {x = x , y } (eqΣ A=B F=G) = eqInΣ (=Fam=-sym F=G) (cast-id _) (cast-id _)
  cast-id {x = ƛ f pf} (eqΠ B=A F=G) =
    eqInΠ (=S=-sym B=A) \x y x=y ->
      proof f x
          ≡ f (_ << y)      by pf _ _ (=El=-trans x=y (cast-id _))
          ≡ _ << f (_ << y) by cast-id _
      qed
    where
      open Chain El _=El=_ (\x -> =El=-refl) (\x y z -> =El=-trans)

  cast-irr : {A₁ A₂ B₁ B₂ : Setoid}{x : El A₁}{y : El A₂}
             (p₁ : B₁ =S= A₁)(p₂ : B₂ =S= A₂) -> x =El= y -> p₁ << x =El= p₂ << y
  cast-irr {x = x}{y = y} p q x=y =
    proof p << x
        ≡ x by =El=-sym (cast-id _)
        ≡ y by x=y
        ≡ q << y by cast-id _
    qed
    where
      open Chain El _=El=_ (\x -> =El=-refl) (\x y z -> =El=-trans)

-- Let's do some overloading

data EqFam : Set -> Set where
  el     : EqFam Setoid
  setoid : EqFam True
  fam    : EqFam Setoid

[_] : {I : Set} -> EqFam I -> I -> Set
[ el ]     A = El A
[ setoid ] _ = Setoid
[ fam ]    A = Fam A

_==_ : {I : Set}{eqf : EqFam I}{i j : I} -> [ eqf ] i -> [ eqf ] j -> Set
_==_ {eqf = el    } x y = x =El= y
_==_ {eqf = setoid} A B = A =S= B
_==_ {eqf = fam   } F G = F =Fam= G

refl : {I : Set}{eqf : EqFam I}{i : I}{x : [ eqf ] i} -> x == x
refl {eqf = el}     = =El=-refl
refl {eqf = setoid} = =S=-refl
refl {eqf = fam}    = =Fam=-refl

sym : {I : Set}{eqf : EqFam I}{i j : I}{x : [ eqf ] i}{y : [ eqf ] j} -> x == y -> y == x
sym {eqf = el}     = =El=-sym
sym {eqf = setoid} = =S=-sym
sym {eqf = fam}    = =Fam=-sym

trans : {I : Set}{eqf : EqFam I}{i j k : I}{x : [ eqf ] i}{y : [ eqf ] j}{z : [ eqf ] k} ->
        x == y -> y == z -> x == z
trans {eqf = el}     = =El=-trans
trans {eqf = setoid} = =S=-trans
trans {eqf = fam}    = =Fam=-trans

open module EqChain {I : Set}{eqf : EqFam I} =
  Chain ([ eqf ]) _==_ (\x -> refl) (\x y z -> trans)

homo : {A B : Setoid}{x : El A}{y : El B} -> x == y -> A == B
homo eqInNat = eqNat
homo (eqInΠ B=A p) = eqΠ B=A (eqFam B=A \x y x=y -> homo (p x y x=y))
homo (eqInΣ F=G p q) = eqΣ (homo p) F=G

cast-id' : {A B C : Setoid}{x : El A}{y : El B}(p : C == B) -> x == y -> x == p << y
cast-id' C=B x=y = trans x=y (cast-id _)

-- Some helper stuff
K : {A : Setoid} -> Setoid -> Fam A
K B = fam (\_ -> B) (\_ _ _ -> refl)

infixr 20 _==>_
infixl 70 _·_ _∘_ _○_
infixl 90 _#_

!-cong : {A B : Setoid}(F : Fam A)(G : Fam B){x : El A}{y : El B} ->
         F == G -> x == y -> F ! x == G ! y
!-cong F G (eqFam B=A F=G) x=y = F=G _ _ x=y

!-cong-R : {A : Setoid}(F : Fam A){x y : El A} ->
           x == y -> F ! x == F ! y
!-cong-R F x=y = !-cong F F refl x=y

_==>_ : Setoid -> Setoid -> Setoid
A ==> B = Π A (K B)

_#_ : {A : Setoid}{F : Fam A} -> El (Π A F) -> (x : El A) -> El (F ! x)
ƛ f _ # x = f x

#-cong : {A B : Setoid}{F : Fam A}{G : Fam B}
         (f : El (Π A F))(g : El (Π B G)){x : El A}{y : El B} ->
         f == g -> x == y -> f # x == g # y
#-cong ._ ._ (eqInΠ _ f=g) x=y = f=g _ _ x=y

#-cong-R : {A : Setoid}{F : Fam A}(f : El (Π A F)){x y : El A} ->
           x == y -> f # x == f # y
#-cong-R f p = #-cong f f refl p

id : {A : Setoid} -> El (A ==> A)
id = ƛ (\x -> x) (\_ _ p -> p)

-- Family composition
_○_ : {A B : Setoid} -> Fam A -> El (B ==> A) -> Fam B
F ○ f = fam (\x -> F ! (f # x)) (\x y x=y -> !-cong-R F (#-cong-R f x=y))

lem-○-id : {A : Setoid}{F : Fam A} -> F ○ id == F
lem-○-id {F = F} = eqFam refl \x y x=y -> !-cong-R F x=y

_∘_ : {A B : Setoid}{F : Fam B} -> El (Π B F) -> (g : El (A ==> B)) -> El (Π A (F ○ g))
f ∘ g = ƛ (\x -> f # (g # x)) \x y x=y -> #-cong-R f (#-cong-R g x=y)

lem-∘-id : {A : Setoid}{F : Fam A}(f : El (Π A F)) -> f ∘ id == f
lem-∘-id (ƛ f pf) = eqInΠ refl pf

lem-id-∘ : {A B : Setoid}(f : El (A ==> B)) -> id ∘ f == f
lem-id-∘ (ƛ f pf) = eqInΠ refl pf

-- Simply type composition (not quite a special case of ∘ because of proof relevance)
_·_ : {A B C : Setoid} -> El (B ==> C) -> El (A ==> B) -> El (A ==> C)
f · g = eqΠ refl (eqFam refl \_ _ _ -> refl) << f ∘ g

fst : {A : Setoid}{F : Fam A} -> El (Σ A F) -> El A
fst (x , y) = x

snd : {A : Setoid}{F : Fam A}(p : El (Σ A F)) -> El (F ! fst p)
snd (x , y) = y

fst-eq : {A B : Setoid}{F : Fam A}{G : Fam B}
         {x : El (Σ A F)}{y : El (Σ B G)} -> x == y -> fst x == fst y
fst-eq (eqInΣ _ x₁=x₂ _) = x₁=x₂

snd-eq : {A B : Setoid}{F : Fam A}{G : Fam B}
        {x : El (Σ A F)}{y : El (Σ B G)} -> x == y -> snd x == snd y
snd-eq (eqInΣ _ _ y₁=y₂) = y₁=y₂

η : {A : Setoid}{F : Fam A}(f : El (Π A F)){pf : (x y : El A) -> x == y -> f # x == f # y} ->
    f == ƛ {F = F} (_#_ f) pf
η (ƛ f pf) = eqInΠ refl pf

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
module Tactic.Reflection.DeBruijn where

open import Prelude hiding (abs)
open import Builtin.Reflection
open import Container.Traversable

record DeBruijn {a} (A : Set a) : Set a where
  field
    strengthenFrom : (from n : Nat) → A → Maybe A
    weakenFrom     : (from n : Nat) → A → A

  strengthen : Nat → A → Maybe A
  strengthen 0 = just
  strengthen n = strengthenFrom 0 n

  weaken : Nat → A → A
  weaken zero = id
  weaken n    = weakenFrom 0 n

open DeBruijn {{...}} public

patternBindings : List (Arg Pattern) → Nat
patternBindings = binds
  where
    binds : List (Arg Pattern) → Nat
    bind  : Pattern → Nat

    binds []             = 0
    binds (arg _ a ∷ as) = bind a + binds as

    bind (con c ps) = binds ps
    bind dot        = 1
    bind (var _)    = 1
    bind (lit l)    = 0
    bind (proj x)   = 0
    bind absurd     = 0

private
  Str : Set → Set
  Str A = Nat → Nat → A → Maybe A

  strVar : Str Nat
  strVar lo n x = if      x <? lo     then just x
                  else if x <? lo + n then nothing
                  else                just (x - n)

  strArgs    : Str (List (Arg Term))
  strArg     : Str (Arg Term)
  strSort    : Str Sort
  strClauses : Str (List Clause)
  strClause  : Str Clause
  strAbsTerm : Str (Abs Term)
  strAbsType : Str (Abs Type)

  strTerm : Str Term
  strTerm lo n (var x args)  = var <$> strVar lo n x <*> strArgs lo n args
  strTerm lo n (con c args)  = con c <$> strArgs lo n args
  strTerm lo n (def f args)  = def f <$> strArgs lo n args
  strTerm lo n (meta x args) = meta x <$> strArgs lo n args
  strTerm lo n (lam v t)     = lam v <$> strAbsTerm lo n t
  strTerm lo n (pi a b)      = pi    <$> strArg lo n a <*> strAbsType lo n b
  strTerm lo n (agda-sort s) = agda-sort <$> strSort lo n s
  strTerm lo n (lit l)       = just (lit l)
  strTerm lo n (pat-lam _ _) = just unknown -- todo
  strTerm lo n unknown       = just unknown

  strAbsTerm lo n (abs s t)  = abs s <$> strTerm (suc lo) n t
  strAbsType lo n (abs s t)  = abs s <$> strTerm (suc lo) n t

  strArgs    lo n []         = just []
  strArgs    lo n (x ∷ args) = _∷_   <$> strArg  lo n x <*> strArgs lo n args
  strArg     lo n (arg i v)  = arg i <$> strTerm lo n v
  strSort    lo n (set t)    = set   <$> strTerm lo n t
  strSort    lo n (lit l)    = just (lit l)
  strSort    lo n unknown    = just unknown

  strClauses lo k [] = just []
  strClauses lo k (c ∷ cs) = _∷_ <$> strClause lo k c <*> strClauses lo k cs

  strClause lo k (clause ps b)      = clause ps <$> strTerm (lo + patternBindings ps) k b
  strClause lo k (absurd-clause ps) = just (absurd-clause ps)

private
  Wk : Set → Set
  Wk A = Nat → Nat → A → A

  wkVar : Wk Nat
  wkVar lo k x = if x <? lo then x else x + k

  wkArgs    : Wk (List (Arg Term))
  wkArg     : Wk (Arg Term)
  wkSort    : Wk Sort
  wkClauses : Wk (List Clause)
  wkClause  : Wk Clause
  wkAbsTerm : Wk (Abs Term)

  wk : Wk Term
  wk lo k (var x args)  = var (wkVar lo k x) (wkArgs lo k args)
  wk lo k (con c args)  = con c (wkArgs lo k args)
  wk lo k (def f args)  = def f (wkArgs lo k args)
  wk lo k (meta x args) = meta x (wkArgs lo k args)
  wk lo k (lam v t)     = lam v (wkAbsTerm lo k t)
  wk lo k (pi a b)      = pi (wkArg lo k a) (wkAbsTerm lo k b)
  wk lo k (agda-sort s) = agda-sort (wkSort lo k s)
  wk lo k (lit l)       = lit l
  wk lo k (pat-lam cs args) = pat-lam (wkClauses lo k cs) (wkArgs lo k args)
  wk lo k unknown       = unknown

  wkAbsTerm lo k (abs s t)  = abs s (wk (suc lo) k t)
  wkArgs    lo k [] = []
  wkArgs    lo k (x ∷ args) = wkArg lo k x ∷ wkArgs lo k args
  wkArg     lo k (arg i v)  = arg i (wk lo k v)
  wkSort    lo k (set t)    = set (wk lo k t)
  wkSort    lo k (lit n)    = lit n
  wkSort    lo k unknown    = unknown

  wkClauses lo k [] = []
  wkClauses lo k (c ∷ cs) = wkClause lo k c ∷ wkClauses lo k cs

  wkClause lo k (clause ps b)      = clause ps (wk (lo + patternBindings ps) k b)
  wkClause lo k (absurd-clause ps) = absurd-clause ps

-- Instances --

DeBruijnTraversable : ∀ {a} {F : Set a → Set a} {{_ : Traversable F}}
                        {A : Set a} {{_ : DeBruijn A}} → DeBruijn (F A)
strengthenFrom {{DeBruijnTraversable}} lo k = traverse (strengthenFrom lo k)
weakenFrom     {{DeBruijnTraversable}} lo k = fmap     (weakenFrom lo k)

instance
  DeBruijnNat : DeBruijn Nat
  strengthenFrom {{DeBruijnNat}} = strVar
  weakenFrom     {{DeBruijnNat}} = wkVar

  DeBruijnTerm : DeBruijn Term
  strengthenFrom {{DeBruijnTerm}} = strTerm
  weakenFrom     {{DeBruijnTerm}} = wk

  DeBruijnList : ∀ {a} {A : Set a} {{_ : DeBruijn A}} → DeBruijn (List A)
  DeBruijnList = DeBruijnTraversable

  DeBruijnVec : ∀ {a} {A : Set a} {{_ : DeBruijn A}} {n : Nat} → DeBruijn (Vec A n)
  DeBruijnVec = DeBruijnTraversable

  DeBruijnArg : {A : Set} {{_ : DeBruijn A}} → DeBruijn (Arg A)
  DeBruijnArg = DeBruijnTraversable

  DeBruijnMaybe : {A : Set} {{_ : DeBruijn A}} → DeBruijn (Maybe A)
  DeBruijnMaybe = DeBruijnTraversable

-- Strip bound names (to ensure _==_ checks α-equality)
-- Doesn't touch pattern variables in pattern lambdas.

mutual

  stripBoundNames : Term → Term
  stripBoundNames (var x args)      = var x (stripArgs args)
  stripBoundNames (con c args)      = con c (stripArgs args)
  stripBoundNames (def f args)      = def f (stripArgs args)
  stripBoundNames (lam v t)         = lam v (stripAbs t)
  stripBoundNames (pat-lam cs args) = pat-lam (stripClauses cs) (stripArgs args)
  stripBoundNames (pi a b)          = pi (stripArg a) (stripAbs b)
  stripBoundNames (agda-sort s)     = agda-sort (stripSort s)
  stripBoundNames (lit l)           = lit l
  stripBoundNames (meta x args)     = meta x (stripArgs args)
  stripBoundNames unknown           = unknown

  private
    stripArgs : List (Arg Term) → List (Arg Term)
    stripArgs [] = []
    stripArgs (x ∷ xs) = stripArg x ∷ stripArgs xs

    stripArg : Arg Term → Arg Term
    stripArg (arg i t) = arg i (stripBoundNames t)

    stripAbs : Abs Term → Abs Term
    stripAbs (abs _ t) = abs "" (stripBoundNames t)

    stripClauses : List Clause → List Clause
    stripClauses [] = []
    stripClauses (x ∷ xs) = stripClause x ∷ stripClauses xs

    stripClause : Clause → Clause
    stripClause (clause ps t) = clause ps (stripBoundNames t)
    stripClause (absurd-clause ps) = absurd-clause ps

    stripSort : Sort → Sort
    stripSort (set t) = set (stripBoundNames t)
    stripSort (lit n) = lit n
    stripSort unknown = unknown

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
{-

A Cubical proof of Blakers-Massey Theorem (KANG Rongji, Oct. 2021)

Based on the previous type-theoretic proof described in
  Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine,
  "A Mechanization of the Blakers–Massey Connectivity Theorem in Homotopy Type Theory"
  (https://arxiv.org/abs/1605.03227)

Also the HoTT-Agda formalization by Favonia:
  (https://github.com/HoTT/HoTT-Agda/blob/master/theorems/homotopy/BlakersMassey.agda)

Using cubes explicitly as much as possible.

-}
{-# OPTIONS  --safe #-}
module Cubical.Homotopy.BlakersMassey where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Isomorphism
open Iso
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv.HalfAdjoint

open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.HITs.Truncation renaming (hLevelTrunc to Trunc)
open import Cubical.HITs.Pushout hiding (PushoutGenFib)

open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.WedgeConnectivity

module BlakersMassey {ℓ₁ ℓ₂ ℓ₃ : Level}
  (X : Type ℓ₁)(Y : Type ℓ₂)(Q : X → Y → Type ℓ₃)
  {m : HLevel} (leftConn  : (x : X) → isConnected (1 + m) (Σ[ y ∈ Y ] Q x y))
  {n : HLevel} (rightConn : (y : Y) → isConnected (1 + n) (Σ[ x ∈ X ] Q x y))
  where

  ℓ : Level
  ℓ = ℓ-max (ℓ-max ℓ₁ ℓ₂) ℓ₃

  leftFiber  : X → Type (ℓ-max ℓ₂ ℓ₃)
  leftFiber x  = Σ[ y ∈ Y ] Q x y

  rightFiber : Y → Type (ℓ-max ℓ₁ ℓ₃)
  rightFiber y = Σ[ x ∈ X ] Q x y

  {- We use the alternative formulation of pushout with fewer parameters -}

  PushoutQ = PushoutGen Q

  {- Some preliminary definitions for convenience -}

  fiberSquare :
      {x₀ x₁ : X}{y₀ : Y}{p : PushoutQ}(q₀₀ : Q x₀ y₀)(q₁₀ : Q x₁ y₀)
    → inl x₁ ≡ p → inl x₀ ≡ p → Type ℓ
  fiberSquare q₀₀ q₁₀ r' r = PathP (λ i → push q₀₀ (~ i) ≡ r' i) (sym (push q₁₀)) r

  fiberSquarePush :
      {x₀ x₁ : X}{y₀ y₁ : Y}(q₀₀ : Q x₀ y₀)(q₁₀ : Q x₁ y₀)(q₁₁ : Q x₁ y₁)
    → inl x₀ ≡ inr y₁ → Type ℓ
  fiberSquarePush q₀₀ q₁₀ q₁₁ = fiberSquare q₀₀ q₁₀ (push q₁₁)

  fiber' : {x₀ : X}{y₀ : Y}(q₀₀ : Q x₀ y₀){x₁ : X}{p : PushoutQ} → inl x₁ ≡ p → inl x₀ ≡ p → Type ℓ
  fiber' {y₀ = y₀} q₀₀ {x₁ = x₁} r' r = Σ[ q₁₀ ∈ Q x₁ y₀ ] fiberSquare q₀₀ q₁₀ r' r

  fiber'Push : {x₀ x₁ : X}{y₀ y₁ : Y}(q₀₀ : Q x₀ y₀)(q₁₁ : Q x₁ y₁) → inl x₀ ≡ inr y₁ → Type ℓ
  fiber'Push q₀₀ q₁₁ = fiber' q₀₀ (push q₁₁)

  leftCodeExtended :
      {x₀ : X}{y₀ : Y}(q₀₀ : Q x₀ y₀)
    → (x₁ : X){p : PushoutQ} → inl x₁ ≡ p → inl x₀ ≡ p → Type ℓ
  leftCodeExtended {y₀ = y₀} q₀₀ x₁ r' r = Trunc (m + n) (fiber' q₀₀ r' r)

  rightCode : {x₀ : X}(y : Y) → Path PushoutQ (inl x₀) (inr y) → Type ℓ
  rightCode y r = Trunc (m + n) (fiber push r)

  {- Bunch of coherence data that will be used to construct Code -}

  {- Definitions of fiber→ -}

  module _
    {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀) where

    {- (x₀ , q₀₀) = (x₁ , q₁₀) -}
    module _
      {y₁ : Y}(q₁₁ : Q x₁ y₁)
      (r : inl x₁ ≡ inr y₁)
      (p : fiberSquarePush q₁₀ q₁₀ q₁₁ r) where

      fiber→[q₀₀=q₁₀]-filler : (i j k : I) → PushoutQ
      fiber→[q₀₀=q₁₀]-filler i j k' =
        hfill (λ k → λ { (i = i0) → push q₁₁ (j ∧ k)
                       ; (i = i1) → p k j
                       ; (j = i0) → push q₁₀ (i ∧ ~ k)
                       ; (j = i1) → push q₁₁ k })
              (inS (push q₁₀ (i ∧ ~ j))) k'

      fiber→[q₀₀=q₁₀] : fiber push r
      fiber→[q₀₀=q₁₀] .fst = q₁₁
      fiber→[q₀₀=q₁₀] .snd i j = fiber→[q₀₀=q₁₀]-filler i j i1

      ∣fiber→[q₀₀=q₁₀]∣ : rightCode _ r
      ∣fiber→[q₀₀=q₁₀]∣ = ∣ fiber→[q₀₀=q₁₀] ∣ₕ

    {- (y₁ , q₁₁) = (y₀ , q₁₀) -}
    module _
      {x₀ : X}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₀)
      (p : fiberSquarePush q₀₀ q₁₀ q₁₀ r) where

      fiber→[q₁₁=q₁₀]-filler : (i j k : I) → PushoutQ
      fiber→[q₁₁=q₁₀]-filler i j k' =
        hfill (λ k → λ { (i = i0) → push q₀₀ (j ∨ ~ k)
                       ; (i = i1) → p k j
                       ; (j = i0) → push q₀₀ (~ k)
                       ; (j = i1) → push q₁₀ (~ i ∨ k) })
              (inS (push q₁₀ (~ i ∨ ~ j))) k'

      fiber→[q₁₁=q₁₀] : fiber push r
      fiber→[q₁₁=q₁₀] .fst = q₀₀
      fiber→[q₁₁=q₁₀] .snd i j = fiber→[q₁₁=q₁₀]-filler i j i1

      ∣fiber→[q₁₁=q₁₀]∣ : rightCode _ r
      ∣fiber→[q₁₁=q₁₀]∣ = ∣ fiber→[q₁₁=q₁₀] ∣ₕ

    {- q₀₀ = q₁₁ = q₁₀ -}
    fiber→[q₀₀=q₁₀=q₁₁]-filler :
        (r : inl x₁ ≡ inr y₀)
      → (p : fiberSquarePush q₁₀ q₁₀ q₁₀ r)
      → (i j k l : I) → PushoutQ
    fiber→[q₀₀=q₁₀=q₁₁]-filler r p i j k l' =
      hfill (λ l → λ { (i = i0) → fiber→[q₀₀=q₁₀]-filler q₁₀ r p j k l
                     ; (i = i1) → fiber→[q₁₁=q₁₀]-filler q₁₀ r p j k l
                     ; (j = i0) → push q₁₀ ((i ∨ (k ∧ l)) ∧ (k ∨ (i ∧ ~ l)))
                     ; (j = i1) → p l k
                     ; (k = i0) → push q₁₀ ((i ∨ j) ∧ ~ l)
                     ; (k = i1) → push q₁₀ ((i ∧ ~ j) ∨ l) })
            (inS (push q₁₀ ((i ∨ (~ k ∧ j)) ∧ (~ k ∨ (i ∧ ~ j))))) l'

    fiber→[q₀₀=q₁₀=q₁₁] : fiber→[q₀₀=q₁₀] q₁₀ ≡ fiber→[q₁₁=q₁₀] q₁₀
    fiber→[q₀₀=q₁₀=q₁₁] i r p .fst = q₁₀
    fiber→[q₀₀=q₁₀=q₁₁] i r p .snd j k = fiber→[q₀₀=q₁₀=q₁₁]-filler r p i j k i1

    ∣fiber→[q₀₀=q₁₀=q₁₁]∣ : ∣fiber→[q₀₀=q₁₀]∣ q₁₀ ≡ ∣fiber→[q₁₁=q₁₀]∣ q₁₀
    ∣fiber→[q₀₀=q₁₀=q₁₁]∣ i r p = ∣ fiber→[q₀₀=q₁₀=q₁₁] i r p ∣ₕ

  {- Definitions of fiber← -}

  module _
    {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁) where

    {- (x₁ , q₁₁) = (x₀ , q₀₁) -}
    module _
      {y₀ : Y}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      fiber←[q₁₁=q₀₁]-filler : (i j k : I) → PushoutQ
      fiber←[q₁₁=q₀₁]-filler i j k' =
        hfill (λ k → λ { (i = i0) → push q₀₀ (~ j ∧ k)
                       ; (i = i1) → p k j
                       ; (j = i0) → push q₀₀ (~ i ∧ k)
                       ; (j = i1) → push q₀₁ i })
              (inS (push q₀₁ (i ∧ j))) k'

      fiber←[q₁₁=q₀₁] : fiber'Push  q₀₀ q₀₁ r
      fiber←[q₁₁=q₀₁] .fst = q₀₀
      fiber←[q₁₁=q₀₁] .snd i j = fiber←[q₁₁=q₀₁]-filler i j i1

      ∣fiber←[q₁₁=q₀₁]∣ : leftCodeExtended q₀₀ _ (push q₀₁) r
      ∣fiber←[q₁₁=q₀₁]∣ = ∣ fiber←[q₁₁=q₀₁] ∣ₕ

    {- (y₀ , q₀₀) = (y₁ , q₀₁) -}
    module _
      {x₁ : X}(q₁₁ : Q x₁ y₁)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      fiber←[q₀₀=q₀₁]-filler : (i j k : I) → PushoutQ
      fiber←[q₀₀=q₀₁]-filler i j k' =
        hfill (λ k → λ { (i = i0) → push q₁₁ (~ j ∨ ~ k)
                       ; (i = i1) → p k j
                       ; (j = i0) → push q₀₁ (~ i)
                       ; (j = i1) → push q₁₁ (i ∨ ~ k) })
              (inS (push q₀₁ (~ i ∨ j))) k'

      fiber←[q₀₀=q₀₁] : fiber'Push q₀₁ q₁₁ r
      fiber←[q₀₀=q₀₁] .fst = q₁₁
      fiber←[q₀₀=q₀₁] .snd i j = fiber←[q₀₀=q₀₁]-filler i j i1

      ∣fiber←[q₀₀=q₀₁]∣ : leftCodeExtended q₀₁ _ (push q₁₁) r
      ∣fiber←[q₀₀=q₀₁]∣ = ∣ fiber←[q₀₀=q₀₁] ∣ₕ

    {- q₀₀ = q₀₁ = q₁₁ -}
    fiber←[q₀₀=q₀₁=q₁₁]-filler :
        (r : inl x₀ ≡ inr y₁)
      → (p : push q₀₁ ≡ r)
      → (i j k l : I) → PushoutQ
    fiber←[q₀₀=q₀₁=q₁₁]-filler r p i j k l' =
      hfill (λ l → λ { (i = i0) → fiber←[q₁₁=q₀₁]-filler q₀₁ r p j k l
                     ; (i = i1) → fiber←[q₀₀=q₀₁]-filler q₀₁ r p j k l
                     ; (j = i0) → push q₀₁ ((i ∨ (~ k ∧ l)) ∧ (~ k ∨ (i ∧ ~ l)))
                     ; (j = i1) → p l k
                     ; (k = i0) → push q₀₁ ((i ∨ l) ∧ ~ j)
                     ; (k = i1) → push q₀₁ ((i ∧ ~ l) ∨ j) })
            (inS (push q₀₁ ((i ∨ (k ∧ j)) ∧ (k ∨ (i ∧ ~ j))))) l'

    fiber←[q₀₀=q₀₁=q₁₁] : fiber←[q₁₁=q₀₁] q₀₁ ≡ fiber←[q₀₀=q₀₁] q₀₁
    fiber←[q₀₀=q₀₁=q₁₁] i r p .fst = q₀₁
    fiber←[q₀₀=q₀₁=q₁₁] i r p .snd j k = fiber←[q₀₀=q₀₁=q₁₁]-filler r p i j k i1

    ∣fiber←[q₀₀=q₀₁=q₁₁]∣ : ∣fiber←[q₁₁=q₀₁]∣ q₀₁ ≡ ∣fiber←[q₀₀=q₀₁]∣ q₀₁
    ∣fiber←[q₀₀=q₀₁=q₁₁]∣ i r p = ∣ fiber←[q₀₀=q₀₁=q₁₁] i r p ∣ₕ

  {- Definitions of fiber→← -}

  module _
    {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀) where

    {- (x₀ , q₀₀) = (x₁ , q₁₀) -}
    module _
      {y₁ : Y}(q₁₁ : Q x₁ y₁)
      (r : inl x₁ ≡ inr y₁)
      (p : fiberSquarePush q₁₀ q₁₀ q₁₁ r) where

      fiber→←[q₀₀=q₁₀]-filler : (i j k l : I) → PushoutQ
      fiber→←[q₀₀=q₁₀]-filler i j k l' =
        let p' = fiber→[q₀₀=q₁₀] q₁₀ q₁₁ r p .snd in
        hfill (λ l → λ { (i = i0) → fiber←[q₁₁=q₀₁]-filler q₁₁ q₁₀ r p' j k l
                       ; (i = i1) → fiber→[q₀₀=q₁₀]-filler q₁₀ q₁₁ r p l k j
                       ; (j = i0) → push q₁₀ (~ k ∧ l)
                       ; (j = i1) → p' l k
                       ; (k = i0) → push q₁₀ (~ j ∧ l)
                       ; (k = i1) → push q₁₁ j })
              (inS (push q₁₁ (j ∧ k))) l'

      fiber→←[q₀₀=q₁₀] : fiber←[q₁₁=q₀₁] q₁₁ q₁₀ r (fiber→[q₀₀=q₁₀] q₁₀ q₁₁ r p .snd) .snd ≡ p
      fiber→←[q₀₀=q₁₀] i j k = fiber→←[q₀₀=q₁₀]-filler i j k i1

    {- (y₁ , q₁₁) = (y₀ , q₁₀) -}
    module _
      {x₀ : X}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₀)
      (p : fiberSquarePush q₀₀ q₁₀ q₁₀ r) where

      fiber→←[q₁₁=q₁₀]-filler : (i j k l : I) → PushoutQ
      fiber→←[q₁₁=q₁₀]-filler i j k l' =
        let p' = fiber→[q₁₁=q₁₀] q₁₀ q₀₀ r p .snd in
        hfill (λ l → λ { (i = i0) → fiber←[q₀₀=q₀₁]-filler q₀₀ q₁₀ r p' j k l
                       ; (i = i1) → fiber→[q₁₁=q₁₀]-filler q₁₀ q₀₀ r p l k j
                       ; (j = i0) → push q₁₀ (~ k ∨ ~ l)
                       ; (j = i1) → p' l k
                       ; (k = i0) → push q₀₀ (~ j)
                       ; (k = i1) → push q₁₀ (j ∨ ~ l) })
              (inS (push q₀₀ (~ j ∨ k))) l'

      fiber→←[q₁₁=q₁₀] : fiber←[q₀₀=q₀₁] q₀₀ q₁₀ r (fiber→[q₁₁=q₁₀] q₁₀ q₀₀ r p .snd) .snd ≡ p
      fiber→←[q₁₁=q₁₀] i j k = fiber→←[q₁₁=q₁₀]-filler i j k i1

    {- q₀₀ = q₁₀ = q₁₁ -}
    fiber→←hypercube :
        (r : inl x₁ ≡ inr y₀)
      → (p : fiberSquarePush q₁₀ q₁₀ q₁₀ r)
      → PathP (λ i → fiber←[q₀₀=q₀₁=q₁₁] q₁₀ i r (fiber→[q₀₀=q₁₀=q₁₁] q₁₀ i r p .snd) .snd ≡ p)
              (fiber→←[q₀₀=q₁₀] q₁₀ r p) (fiber→←[q₁₁=q₁₀] q₁₀ r p)
    fiber→←hypercube r p i j u v =
      hcomp (λ l → λ { (i = i0) → fiber→←[q₀₀=q₁₀]-filler q₁₀ r p j u v l
                     ; (i = i1) → fiber→←[q₁₁=q₁₀]-filler q₁₀ r p j u v l
                     ; (j = i0) → fiber←[q₀₀=q₀₁=q₁₁]-filler q₁₀ r (fiber→[q₀₀=q₁₀=q₁₁] q₁₀ i r p .snd) i u v l
                     ; (j = i1) → fiber→[q₀₀=q₁₀=q₁₁]-filler q₁₀ r p i l v u
                     ; (u = i0) → push q₁₀ ((i ∨ (~ v ∧ l)) ∧ (~ v ∨ (i ∧ ~ l)))
                     ; (u = i1) → fiber→[q₀₀=q₁₀=q₁₁] q₁₀ i r p .snd l v
                     ; (v = i0) → push q₁₀ ((i ∨ l) ∧ ~ u)
                     ; (v = i1) → push q₁₀ ((i ∧ ~ l) ∨ u) })
            (push q₁₀ ((i ∨ (v ∧ u)) ∧ (v ∨ (i ∧ ~ u))))

  {- Definitions of fiber←→ -}

  module _
    {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁) where

    {- (x₁ , q₁₁) = (x₀ , q₀₁) -}
    module _
      {y₀ : Y}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      fiber←→[q₁₁=q₀₁]-filler : (i j k l : I) → PushoutQ
      fiber←→[q₁₁=q₀₁]-filler i j k l' =
        let p' = fiber←[q₁₁=q₀₁] q₀₁ q₀₀ r p .snd in
        hfill (λ l → λ { (i = i0) → fiber→[q₀₀=q₁₀]-filler q₀₀ q₀₁ r p' j k l
                       ; (i = i1) → fiber←[q₁₁=q₀₁]-filler q₀₁ q₀₀ r p l k j
                       ; (j = i0) → push q₀₁ (k ∧ l)
                       ; (j = i1) → p' l k
                       ; (k = i0) → push q₀₀ (j ∧ ~ l)
                       ; (k = i1) → push q₀₁ l })
              (inS (push q₀₀ (j ∧ ~ k))) l'

      fiber←→[q₁₁=q₀₁] : fiber→[q₀₀=q₁₀] q₀₀ q₀₁ r (fiber←[q₁₁=q₀₁] q₀₁ q₀₀ r p .snd) .snd ≡ p
      fiber←→[q₁₁=q₀₁] i j k = fiber←→[q₁₁=q₀₁]-filler i j k i1

    {- (y₀ , q₀₀) = (y₁ , q₀₁) -}
    module _
      {x₁ : X}(q₁₁ : Q x₁ y₁)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      fiber←→[q₀₀=q₀₁]-filler : (i j k l : I) → PushoutQ
      fiber←→[q₀₀=q₀₁]-filler i j k l' =
        let p' = fiber←[q₀₀=q₀₁] q₀₁ q₁₁ r p .snd in
        hfill (λ l → λ { (i = i0) → fiber→[q₁₁=q₁₀]-filler q₁₁ q₀₁ r p' j k l
                       ; (i = i1) → fiber←[q₀₀=q₀₁]-filler q₀₁ q₁₁ r p l k j
                       ; (j = i0) → push q₀₁ (k ∨ ~ l)
                       ; (j = i1) → p' l k
                       ; (k = i0) → push q₀₁ (~ l)
                       ; (k = i1) → push q₁₁ (~ j ∨ l) })
              (inS (push q₁₁ (~ j ∨ ~ k))) l'

      fiber←→[q₀₀=q₀₁] : fiber→[q₁₁=q₁₀] q₁₁ q₀₁ r (fiber←[q₀₀=q₀₁] q₀₁ q₁₁ r p .snd) .snd ≡ p
      fiber←→[q₀₀=q₀₁] i j k = fiber←→[q₀₀=q₀₁]-filler i j k i1

    {- q₀₀ = q₀₁ = q₁₁ -}
    fiber←→hypercube :
        (r : inl x₀ ≡ inr y₁)
      → (p : push q₀₁ ≡ r)
      → PathP (λ i → fiber→[q₀₀=q₁₀=q₁₁] q₀₁ i r (fiber←[q₀₀=q₀₁=q₁₁] q₀₁ i r p .snd) .snd ≡ p)
              (fiber←→[q₁₁=q₀₁] q₀₁ r p) (fiber←→[q₀₀=q₀₁] q₀₁ r p)
    fiber←→hypercube r p i j u v =
      hcomp (λ l → λ { (i = i0) → fiber←→[q₁₁=q₀₁]-filler q₀₁ r p j u v l
                     ; (i = i1) → fiber←→[q₀₀=q₀₁]-filler q₀₁ r p j u v l
                     ; (j = i0) → fiber→[q₀₀=q₁₀=q₁₁]-filler q₀₁ r (fiber←[q₀₀=q₀₁=q₁₁] q₀₁ i r p .snd) i u v l
                     ; (j = i1) → fiber←[q₀₀=q₀₁=q₁₁]-filler q₀₁ r p i l v u
                     ; (u = i0) → push q₀₁ ((i ∨ (v ∧ l)) ∧ (v ∨ (i ∧ ~ l)))
                     ; (u = i1) → fiber←[q₀₀=q₀₁=q₁₁] q₀₁ i r p .snd l v
                     ; (v = i0) → push q₀₁ ((i ∨ u) ∧ ~ l)
                     ; (v = i1) → push q₀₁ ((i ∧ ~ u) ∨ l) })
           (push q₀₁ ((i ∨ (~ v ∧ u)) ∧ (~ v ∨ (i ∧ ~ u))))

  module Fiber→
    {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀) =
    WedgeConnectivity m n
      (leftFiber  x₁ , (y₀ , q₁₀)) (leftConn  x₁)
      (rightFiber y₀ , (x₁ , q₁₀)) (rightConn y₀)
      (λ (y₁ , q₁₁) (x₀ , q₀₀) →
        (((r : inl x₀ ≡ inr y₁) → fiberSquarePush q₀₀ q₁₀ q₁₁ r → rightCode _ r)
        , isOfHLevelΠ2 _ (λ x y → isOfHLevelTrunc _)))
      (λ (y₁ , q₁₁) → ∣fiber→[q₀₀=q₁₀]∣ q₁₀ q₁₁)
      (λ (x₀ , q₀₀) → ∣fiber→[q₁₁=q₁₀]∣ q₁₀ q₀₀)
      (∣fiber→[q₀₀=q₁₀=q₁₁]∣ q₁₀)

  fiber→ :
      {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀)
    → {x₀ : X}(q₀₀ : Q x₀ y₀) → {y₁ : Y}(q₁₁ : Q x₁ y₁)
    → (r : inl x₀ ≡ inr y₁)
    → fiberSquarePush q₀₀ q₁₀ q₁₁ r → rightCode _ r
  fiber→ q₁₀ q₀₀ q₁₁ = Fiber→.extension q₁₀ (_ , q₁₁) (_ , q₀₀)

  module Fiber←
    {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁) =
    WedgeConnectivity m n
      (leftFiber  x₀ , (y₁ , q₀₁)) (leftConn  x₀)
      (rightFiber y₁ , (x₀ , q₀₁)) (rightConn y₁)
      (λ (y₀ , q₀₀) (x₁ , q₁₁) →
        (((r : inl x₀ ≡ inr y₁) → push q₀₁ ≡ r → leftCodeExtended q₀₀ _ (push q₁₁) r)
        , isOfHLevelΠ2 _ (λ x y → isOfHLevelTrunc _)))
      (λ (y₀ , q₀₀) → ∣fiber←[q₁₁=q₀₁]∣ q₀₁ q₀₀)
      (λ (x₁ , q₁₁) → ∣fiber←[q₀₀=q₀₁]∣ q₀₁ q₁₁)
      (∣fiber←[q₀₀=q₀₁=q₁₁]∣ q₀₁)

  fiber← :
      {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁)
    → {y₀ : Y}(q₀₀ : Q x₀ y₀) → {x₁ : X}(q₁₁ : Q x₁ y₁)
    → (r : inl x₀ ≡ inr y₁)
    → push q₀₁ ≡ r → leftCodeExtended q₀₀ _ (push q₁₁) r
  fiber← q₀₁ q₀₀ q₁₁ = Fiber←.extension q₀₁ (_ , q₀₀) (_ , q₁₁)

  module _
    {x₀ x₁ : X}{y₀ y₁ : Y}
    (q₀₀ : Q x₀ y₀)(q₁₁ : Q x₁ y₁)
    (r : inl x₀ ≡ inr y₁) where

    left→rightCodeExtended : leftCodeExtended q₀₀ _ (push q₁₁) r → rightCode _ r
    left→rightCodeExtended =
      rec (isOfHLevelTrunc _) (λ (q₁₀ , p) → fiber→ q₁₀ q₀₀ q₁₁ r p)

    right→leftCodeExtended : rightCode _ r → leftCodeExtended q₀₀ _ (push q₁₁) r
    right→leftCodeExtended =
      rec (isOfHLevelTrunc _) (λ (q₀₁ , p) → fiber← q₀₁ q₀₀ q₁₁ r p)

  {- Definition of one-side homotopy -}

  module _
    {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀) where

    {- (x₀ , q₀₀) = (x₁ , q₁₀) -}
    module _
      {y₁ : Y}(q₁₁ : Q x₁ y₁)
      (r : inl x₁ ≡ inr y₁)
      (p : fiberSquarePush q₁₀ q₁₀ q₁₁ r) where

      ∣fiber→←[q₀₀=q₁₀]∣ : right→leftCodeExtended q₁₀ q₁₁ r (fiber→ q₁₀ q₁₀ q₁₁ r p) ≡ ∣ q₁₀ , p ∣ₕ
      ∣fiber→←[q₀₀=q₁₀]∣ =
          (λ i → right→leftCodeExtended q₁₀ q₁₁ r (Fiber→.left q₁₀ (_ , q₁₁) i r p))
        ∙ recUniq {n = m + n} _ _ _
        ∙ (λ i → Fiber←.left q₁₁ (_ , q₁₀) i r (fiber→[q₀₀=q₁₀] q₁₀ q₁₁ r p .snd))
        ∙ (λ i → ∣ q₁₀ , fiber→←[q₀₀=q₁₀] q₁₀ q₁₁ r p i ∣ₕ)

    {- (y₁ , q₁₁) = (y₀ , q₁₀) -}
    module _
      {x₀ : X}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₀)
      (p : fiberSquarePush q₀₀ q₁₀ q₁₀ r) where

      ∣fiber→←[q₁₁=q₁₀]∣ : right→leftCodeExtended q₀₀ q₁₀ r (fiber→ q₁₀ q₀₀ q₁₀ r p) ≡ ∣ q₁₀ , p ∣ₕ
      ∣fiber→←[q₁₁=q₁₀]∣ =
          (λ i → right→leftCodeExtended q₀₀ q₁₀ r (Fiber→.right q₁₀ (_ , q₀₀) i r p))
        ∙ recUniq {n = m + n} _ _ _
        ∙ (λ i → Fiber←.right q₀₀ (_ , q₁₀) i r (fiber→[q₁₁=q₁₀] q₁₀ q₀₀ r p .snd))
        ∙ (λ i → ∣ q₁₀ , fiber→←[q₁₁=q₁₀] q₁₀ q₀₀ r p i ∣ₕ)

    {- q₀₀ = q₁₁ = q₁₀ -}
    module _
      (r : inl x₁ ≡ inr y₀)
      (p : fiberSquarePush q₁₀ q₁₀ q₁₀ r) where

      path→←Square =
           (λ i j → right→leftCodeExtended q₁₀ q₁₀ r (Fiber→.homSquare q₁₀ i j r p))
        ∙₂ (λ i → recUniq {n = m + n} _ _ _)
        ∙₂ (λ i j → Fiber←.homSquare q₁₀ i j r (fiber→[q₀₀=q₁₀=q₁₁] q₁₀ i r p .snd))
        ∙₂ (λ i j → ∣ (q₁₀ , fiber→←hypercube q₁₀ r p i j) ∣ₕ)

    ∣fiber→←[q₀₀=q₁₀=q₁₁]∣ : ∣fiber→←[q₀₀=q₁₀]∣ q₁₀ ≡ ∣fiber→←[q₁₁=q₁₀]∣ q₁₀
    ∣fiber→←[q₀₀=q₁₀=q₁₁]∣ i r p = path→←Square r p i

  fiber→← :
      {x₁ : X}{y₀ : Y}(q₁₀ : Q x₁ y₀)
    → {x₀ : X}(q₀₀ : Q x₀ y₀) → {y₁ : Y}(q₁₁ : Q x₁ y₁)
    → (r : inl x₀ ≡ inr y₁)
    → (p : fiberSquarePush q₀₀ q₁₀ q₁₁ r)
    → right→leftCodeExtended q₀₀ q₁₁ r (fiber→ q₁₀ q₀₀ q₁₁ r p) ≡ ∣ q₁₀ , p ∣ₕ
  fiber→← {x₁ = x₁} {y₀ = y₀} q₁₀ q₀₀' q₁₁' =
    WedgeConnectivity.extension m n
      (leftFiber  x₁ , (y₀ , q₁₀)) (leftConn  x₁)
      (rightFiber y₀ , (x₁ , q₁₀)) (rightConn y₀)
      (λ (y₁ , q₁₁) (x₀ , q₀₀) →
        ((  (r : inl x₀ ≡ inr y₁) → (p : fiberSquarePush q₀₀ q₁₀ q₁₁ r)
          → right→leftCodeExtended q₀₀ q₁₁ r (fiber→ q₁₀ q₀₀ q₁₁ r p) ≡ ∣ q₁₀ , p ∣ₕ )
        , isOfHLevelΠ2 _ (λ x y → isOfHLevelTruncPath)))
      (λ (y₁ , q₁₁) → ∣fiber→←[q₀₀=q₁₀]∣ q₁₀ q₁₁)
      (λ (x₀ , q₀₀) → ∣fiber→←[q₁₁=q₁₀]∣ q₁₀ q₀₀)
      (∣fiber→←[q₀₀=q₁₀=q₁₁]∣ q₁₀)
      (_ , q₁₁') (_ , q₀₀')

  {- Definition of the other side homotopy -}

  module _
    {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁) where

    {- (x₁ , q₁₁) = (x₀ , q₀₁) -}
    module _
      {y₀ : Y}(q₀₀ : Q x₀ y₀)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      ∣fiber←→[q₁₁=q₀₁]∣ : left→rightCodeExtended q₀₀ q₀₁ r (fiber← q₀₁ q₀₀ q₀₁ r p) ≡ ∣ q₀₁ , p ∣ₕ
      ∣fiber←→[q₁₁=q₀₁]∣ =
          (λ i → left→rightCodeExtended q₀₀ q₀₁ r (Fiber←.left q₀₁ (_ , q₀₀) i r p))
        ∙ recUniq {n = m + n} _ _ _
        ∙ (λ i → Fiber→.left q₀₀ (_ , q₀₁) i r (fiber←[q₁₁=q₀₁] q₀₁ q₀₀ r p .snd))
        ∙ (λ i → ∣ q₀₁ , fiber←→[q₁₁=q₀₁] q₀₁ q₀₀ r p i ∣ₕ)

    {- (y₀ , q₀₀) = (y₁ , q₀₁) -}
    module _
      {x₁ : X}(q₁₁ : Q x₁ y₁)
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      ∣fiber←→[q₀₀=q₀₁]∣ : left→rightCodeExtended q₀₁ q₁₁ r (fiber← q₀₁ q₀₁ q₁₁ r p) ≡ ∣ q₀₁ , p ∣ₕ
      ∣fiber←→[q₀₀=q₀₁]∣  =
          (λ i → left→rightCodeExtended q₀₁ q₁₁ r (Fiber←.right q₀₁ (_ , q₁₁) i r p))
        ∙ recUniq {n = m + n} _ _ _
        ∙ (λ i → Fiber→.right q₁₁ (_ , q₀₁) i r (fiber←[q₀₀=q₀₁] q₀₁ q₁₁ r p .snd))
        ∙ (λ i → ∣ q₀₁ , fiber←→[q₀₀=q₀₁] q₀₁ q₁₁ r p i ∣ₕ)

    {- q₀₀ = q₀₁ = q₁₁ -}
    module _
      (r : inl x₀ ≡ inr y₁)
      (p : push q₀₁ ≡ r) where

      path←→Square =
           (λ i j → left→rightCodeExtended q₀₁ q₀₁ r (Fiber←.homSquare q₀₁ i j r p))
        ∙₂ (λ i → recUniq {n = m + n} _ _ _)
        ∙₂ (λ i j → Fiber→.homSquare q₀₁ i j r (fiber←[q₀₀=q₀₁=q₁₁] q₀₁ i r p .snd))
        ∙₂ (λ i j → ∣ q₀₁ , fiber←→hypercube q₀₁ r p i j ∣ₕ)

    ∣fiber←→[q₀₀=q₀₁=q₁₁]∣ : ∣fiber←→[q₁₁=q₀₁]∣ q₀₁ ≡ ∣fiber←→[q₀₀=q₀₁]∣ q₀₁
    ∣fiber←→[q₀₀=q₀₁=q₁₁]∣ i r p = path←→Square r p i

  fiber←→ :
      {x₀ : X}{y₁ : Y}(q₀₁ : Q x₀ y₁)
    → {y₀ : Y}(q₀₀ : Q x₀ y₀) → {x₁ : X}(q₁₁ : Q x₁ y₁)
    → (r : inl x₀ ≡ inr y₁)
    → (p : push q₀₁ ≡ r)
    → left→rightCodeExtended q₀₀ q₁₁ r (fiber← q₀₁ q₀₀ q₁₁ r p) ≡ ∣ q₀₁ , p ∣ₕ
  fiber←→ {x₀ = x₀} {y₁ = y₁} q₀₁ q₀₀' q₁₁' =
    WedgeConnectivity.extension m n
      (leftFiber  x₀ , (y₁ , q₀₁)) (leftConn  x₀)
      (rightFiber y₁ , (x₀ , q₀₁)) (rightConn y₁)
      (λ (y₀ , q₀₀) (x₁ , q₁₁) →
        ((  (r : inl x₀ ≡ inr y₁) → (p : push q₀₁ ≡ r)
          → left→rightCodeExtended q₀₀ q₁₁ r (fiber← q₀₁ q₀₀ q₁₁ r p) ≡ ∣ q₀₁ , p ∣ₕ )
        , isOfHLevelΠ2 _ (λ x y → isOfHLevelTruncPath)))
      (λ (y₀ , q₀₀) → ∣fiber←→[q₁₁=q₀₁]∣ q₀₁ q₀₀)
      (λ (x₁ , q₁₁) → ∣fiber←→[q₀₀=q₀₁]∣ q₀₁ q₁₁)
      (∣fiber←→[q₀₀=q₀₁=q₁₁]∣ q₀₁)
      (_ , q₀₀') (_ , q₁₁')

  module _
    {x₀ x₁ : X}{y₀ y₁ : Y}
    (q₀₀ : Q x₀ y₀)(q₁₁ : Q x₁ y₁)
    (r : inl x₀ ≡ inr y₁) where

    left→right→leftCodeExtended :
        (a : leftCodeExtended q₀₀ _ (push q₁₁) r)
      → right→leftCodeExtended q₀₀ q₁₁ r (left→rightCodeExtended q₀₀ q₁₁ r a) ≡ a
    left→right→leftCodeExtended a =
      sym (∘rec _ _ _ (right→leftCodeExtended q₀₀ q₁₁ r) a) ∙
      (λ i → recId _ (λ (q₁₀ , p) → fiber→← q₁₀ q₀₀ q₁₁ r p) i a)

    right→left→rightCodeExtended :
        (a : rightCode _ r)
      → left→rightCodeExtended q₀₀ q₁₁ r (right→leftCodeExtended q₀₀ q₁₁ r a) ≡ a
    right→left→rightCodeExtended a =
      sym (∘rec _ _ _ (left→rightCodeExtended q₀₀ q₁₁ r) a) ∙
      (λ i → recId _ (λ (q₀₁ , p) → fiber←→ q₀₁ q₀₀ q₁₁ r p) i a)

    left≃rightCodeExtended : leftCodeExtended q₀₀ _ (push q₁₁) r ≃ rightCode y₁ r
    left≃rightCodeExtended =
      isoToEquiv (iso (left→rightCodeExtended _ _ _) (right→leftCodeExtended _ _ _)
                       right→left→rightCodeExtended left→right→leftCodeExtended)

  {- Definition and properties of Code -}

  module _ (x₀ : X)(y₀ : Y)(q₀₀ : Q x₀ y₀) where

    leftCode' : (x : X){p : PushoutQ} → inl x ≡ p → inl x₀ ≡ p → Type ℓ
    leftCode' x r' = leftCodeExtended q₀₀ x r'

    leftCode : (x : X) → inl x₀ ≡ inl x → Type ℓ
    leftCode x = leftCode' x refl

    fiberPath : {x : X}{y : Y} → (q : Q x y) → leftCode' x (push q) ≡ rightCode y
    fiberPath q i r = ua (left≃rightCodeExtended q₀₀ q r) i

    pushCode :
        {x : X}{y : Y} → (q : Q x y)
      → PathP (λ i → inl x₀ ≡ push q i → Type ℓ) (leftCode x) (rightCode y)
    pushCode q i =
      hcomp (λ j → λ { (i = i0) → leftCode _
                     ; (i = i1) → fiberPath q j })
            (leftCode' _ (λ j → push q (i ∧ j)))

    Code : (p : PushoutQ) → inl x₀ ≡ p → Type ℓ
    Code (inl x) = leftCode  x
    Code (inr y) = rightCode y
    Code (push q i) = pushCode q i

    {- Transportation rule of pushCode -}

    transpLeftCode : (y : Y) → (q : Q x₀ y) → (q' : leftCodeExtended q₀₀ _ refl refl) → leftCode' _ (push q) (push q)
    transpLeftCode y q q' =
      transport (λ i → leftCode' _ (λ j → push q (i ∧ j)) (λ j → push q (i ∧ j))) q'

    transpPushCodeβ' :
        (y : Y) → (q : Q x₀ y) → (q' : leftCodeExtended q₀₀ _ refl refl)
      → transport (λ i → pushCode q i (λ j → push q (i ∧ j))) q' ≡ left→rightCodeExtended _ _ _ (transpLeftCode y q q')
    transpPushCodeβ' y q q' i = transportRefl (left→rightCodeExtended _ _ _ (transpLeftCode y q (transportRefl q' i))) i

    module _
      {p : PushoutQ}(r : inl x₀ ≡ p) where

      fiber-filler : I → Type ℓ
      fiber-filler i = fiber' q₀₀ (λ j → r (i ∧ j)) (λ j → r (i ∧ j))

      module _
        (q : fiberSquare q₀₀ q₀₀ refl refl) where

        transpLeftCode-filler : (i j k : I) → PushoutQ
        transpLeftCode-filler i j k' =
          hfill (λ k → λ { (i = i0) → push q₀₀ (~ j)
                         ; (i = i1) → r (j ∧ k)
                         ; (j = i0) → push q₀₀ (~ i)
                         ; (j = i1) → r (i ∧ k) })
                (inS (q i j)) k'

    transpLeftCodeβ' :
        {p : PushoutQ} → (r : inl x₀ ≡ p) → (q : fiberSquare q₀₀ q₀₀ refl refl)
      → transport (λ i → fiber-filler r i) (q₀₀ , q) ≡ (q₀₀ , λ i j → transpLeftCode-filler r q i j i1)
    transpLeftCodeβ' r q =
      J (λ p r → transport (λ i → fiber-filler r i) (q₀₀ , q) ≡ (q₀₀ , λ i j → transpLeftCode-filler r q i j i1))
        (transportRefl _ ∙ (λ k → (q₀₀ , λ i j → transpLeftCode-filler refl q i j k))) r

    transpLeftCodeβ :
        (y : Y) → (q : Q x₀ y) → (q' : fiberSquare q₀₀ q₀₀ refl refl)
      → transpLeftCode y q ∣ q₀₀ , q' ∣ₕ ≡ ∣ q₀₀ , (λ i j → transpLeftCode-filler (push q) q' i j i1) ∣ₕ
    transpLeftCodeβ y q q' = transportTrunc _ ∙ (λ i → ∣ transpLeftCodeβ' _ q' i ∣ₕ)

    transpPushCodeβ :
        (y : Y) → (q : Q x₀ y) → (q' : fiberSquare q₀₀ q₀₀ refl refl)
      →   transport (λ i → pushCode q i (λ j → push q (i ∧ j))) ∣ q₀₀ , q' ∣ₕ
        ≡ ∣fiber→[q₀₀=q₁₀]∣ q₀₀ q (push q) (λ i j → transpLeftCode-filler (push q) q' i j i1)
    transpPushCodeβ y q q' =
        transpPushCodeβ' _ _ _
      ∙ (λ i → left→rightCodeExtended _ _ _ (transpLeftCodeβ _ _ q' i))
      ∙ recUniq {n = m + n} _ _ _
      ∙ (λ i' → Fiber→.left q₀₀ (_ , q) i' (push q) (λ i j → transpLeftCode-filler (push q) q' i j i1))

    {- The contractibility of Code -}

    centerCode : {p : PushoutQ} → (r : inl x₀ ≡ p) → Code p r
    centerCode r =
      transport (λ i → Code _ (λ j → r (i ∧ j))) ∣ q₀₀ , (λ i j → push q₀₀ (~ i ∧ ~ j)) ∣ₕ

    module _
      (y : Y)(q : Q x₀ y) where

      transp-filler : (i j k : I) → PushoutQ
      transp-filler = transpLeftCode-filler (push q) (λ i' j' → push q₀₀ (~ i' ∧ ~ j'))

      transp-square : fiberSquare q₀₀ q₀₀ (push q) (push q)
      transp-square i j = transp-filler i j i1

      contractionCodeRefl' :
        fiber→[q₀₀=q₁₀] q₀₀ q (push q) transp-square .snd ≡ refl
      contractionCodeRefl' i j k =
        hcomp (λ l → λ { (i = i0) → fiber→[q₀₀=q₁₀]-filler q₀₀ q (push q) transp-square j k l
                       ; (i = i1) → transp-square (~ j ∨ l) k
                       ; (j = i0) → push q (k ∧ (i ∨ l))
                       ; (j = i1) → transp-square l k
                       ; (k = i0) → push q₀₀ (j ∧ ~ l)
                       ; (k = i1) → push q ((i ∧ ~ j) ∨ l) })
              (transp-filler (~ j) k i)

      contractionCodeRefl : centerCode (push q) ≡ ∣ q , refl ∣ₕ
      contractionCodeRefl = transpPushCodeβ _ _ _ ∙ (λ i → ∣ q , contractionCodeRefl' i ∣ₕ)

    module _
      (y : Y)(r : inl x₀ ≡ inr y) where

      contractionCode' : (a : fiber push r) → centerCode r ≡ ∣ a ∣ₕ
      contractionCode' (q , p') = J (λ r' p → centerCode r' ≡ ∣ q , p ∣ₕ) (contractionCodeRefl _ q) p'

      contractionCode : (a : Code _ r) → centerCode r ≡ a
      contractionCode = elim (λ _ → isOfHLevelTruncPath) contractionCode'

      isContrCode : isContr (Code _ r)
      isContrCode = centerCode r , contractionCode

  excision-helper :
      (x : X) → Trunc (1 + m) (Σ[ y₀ ∈ Y ] Q x y₀)
    → (y : Y) → (r : inl x ≡ inr y) → isContr (Trunc (m + n) (fiber push r))
  excision-helper x y' y r = rec (isProp→isOfHLevelSuc m isPropIsContr) (λ (y₀ , q₀₀) → isContrCode x y₀ q₀₀ y r ) y'

  {- The Main Result : Blakers-Massey Homotopy Excision Theorem -}
  Excision : (x : X)(y : Y) → isConnectedFun (m + n) (push {x = x} {y = y})
  Excision x y = excision-helper x (leftConn x .fst) y

{-
We also give the following version of the theorem: Given a square

          g
  A --------------> B
  |\              ↗ |
  |  \         ↗    |
  |    \    ↗       |
f |      X          |  inr
  |    /            |
  |   /             |
  |  /              |
  v /               v
  B -----------> Pushout f g
         inl

where X is the pullback of inl and inr
  (X := Σ[ (b , c) ∈ B × C ] (inl b ≡ inr c)).

If f in n-connected and g in m-connected, then the diagonal map
A → X is (n+m)-connected
-}

private
  shuffleFibIso₁ :
       {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
       (f : A → B) (g : A → C) (b : B)
     → Iso (Σ[ c ∈ C ] Σ[ a ∈ A ] (f a ≡ b) × (g a ≡ c))
             (Σ[ a ∈ A ] ((Σ[ c ∈ C ] (g a ≡ c)) × (f a ≡ b)))
  shuffleFibIso₁ f g b =
    compIso (invIso Σ-assoc-Iso)
     (compIso (Σ-cong-iso-fst Σ-swap-Iso)
      (compIso
       (Σ-cong-iso-snd (λ y → Σ-swap-Iso))
       (compIso Σ-assoc-Iso
         (Σ-cong-iso-snd λ a → invIso Σ-assoc-Iso))))

  shuffleFibIso₂ : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
         (f : A → B) (g : A → C) (x : _)
         → Iso (Σ[ a ∈ A ] ((Σ[ c ∈ C ] (g a ≡ c)) × (f a ≡ x)))
                (fiber f x)
  shuffleFibIso₂ f g x = Σ-cong-iso-snd
        λ a → compIso (Σ-cong-iso-fst
                        (isContr→Iso (isContrSingl (g a))
                         isContrUnit))
                       lUnit×Iso

module BlakersMassey□ {ℓ ℓ' ℓ'' : Level}
  {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
  (f : A → B) (g : A → C) (n m : ℕ)
  (con-f : isConnectedFun (suc n) f)
  (con-g : isConnectedFun (suc m) g) where

  {- Some abbreviations and connectivity -}
  private
    fib = doubleFib f g

    B-con : (x : B) → isConnected (suc n) (Σ[ c ∈ C ] (fib x c))
    B-con x =
      isConnectedRetractFromIso (suc n)
        (compIso
          (shuffleFibIso₁ f g x)
          (shuffleFibIso₂ f g x))
        (con-f x)

    C-con : (c : C) → isConnected (suc m) (Σ[ b ∈ B ] (fib b c))
    C-con c =
      isConnectedRetractFromIso (suc m)
        (compIso
          (compIso (Σ-cong-iso-snd
                    (λ _ → Σ-cong-iso-snd λ _ → Σ-swap-Iso))
            (shuffleFibIso₁ g f c))
            (shuffleFibIso₂ g f c))
        (con-g c)

  open module BM-f-g = BlakersMassey B C fib {m = n} B-con {n = m} C-con

  fib× : (B × C) → Type _
  fib× (b , c) = fib b c

  PushoutGenPath× : B × C → Type _
  PushoutGenPath× (b , c) = Path (PushoutGen fib) (inl b) (inr c)

  PushoutPath× : B × C → Type _
  PushoutPath× (b , c) = Path (Pushout f g) (inl b) (inr c)

  {- The function in question -}
  toPullback : A → Σ (B × C) PushoutPath×
  toPullback a = (f a , g a) , push a

  {- We redescribe toPullback as a composition of three maps,
     two of which are equivs and one of which is (n+m)-connected -}
  Totalfib×→Total : Σ (B × C) fib× → Σ (B × C) PushoutGenPath×
  Totalfib×→Total =
    TotalFun {A = B × C} {B = fib×} {C = PushoutGenPath×} (λ a → push)

  isConnectedTotalFun : isConnectedFun (n + m) Totalfib×→Total
  isConnectedTotalFun =
    FunConnected→TotalFunConnected (λ _ → push) (n + m) (uncurry BM-f-g.Excision)

  TotalPathGen×Iso : Iso (Σ (B × C) PushoutGenPath×) (Σ (B × C) PushoutPath×)
  TotalPathGen×Iso =
    Σ-cong-iso-snd λ x
      → congIso (invIso (IsoPushoutPushoutGen f g))

  Totalfib×Iso : Iso (Σ (B × C) fib×) A
  fun Totalfib×Iso ((b , c) , a , p) = a
  inv Totalfib×Iso a = (f a , g a) , a , refl , refl
  rightInv Totalfib×Iso _ = refl
  leftInv Totalfib×Iso ((b , c) , a , (p , q)) i =
    ((p i) , (q i)) , (a , ((λ j → p (i ∧ j)) , (λ j → q (i ∧ j))))

  toPullback' : A → Σ (B × C) PushoutPath×
  toPullback' =
    (fun TotalPathGen×Iso ∘ Totalfib×→Total) ∘ inv Totalfib×Iso

  toPullback'≡toPullback : toPullback' ≡ toPullback
  toPullback'≡toPullback =
    funExt λ x → ΣPathP (refl , (sym (rUnit (push x))))

  isConnected-toPullback : isConnectedFun (n + m) toPullback
  isConnected-toPullback =
    subst (isConnectedFun (n + m)) toPullback'≡toPullback
      (isConnectedComp
        (fun TotalPathGen×Iso ∘ Totalfib×→Total)
        (inv Totalfib×Iso) (n + m)
        (isConnectedComp (fun TotalPathGen×Iso) Totalfib×→Total (n + m)
          (isEquiv→isConnected _ (isoToIsEquiv TotalPathGen×Iso) (n + m))
          isConnectedTotalFun)
        (isEquiv→isConnected _ (isoToIsEquiv (invIso Totalfib×Iso)) (n + m)))

max_stars_repo_name: FernandoLarrain/cubical

max_issues_repo_name: FernandoLarrain/cubical

max_forks_repo_name: FernandoLarrain/cubical


text:
-- Andreas, 2012-10-09
-- Testcase to ensure we do not fire catch all clause on neutrals in literal matching
module DoNotFireLiteralCatchAllForNeutrals where

{-# BUILTIN STRING String #-}

data ⊥ : Set where
record ⊤ : Set where
  constructor trivial

NotNull : String → Set
NotNull "" = ⊥
NotNull s  = ⊤ -- never reduces on open terms

allNull : (s : String) → NotNull s
allNull s = trivial -- should fail

bot : ⊥
bot = allNull ""

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Hurkens' paradox [1].

-- [1] A. Hurkens, A simplification of Girard's paradox.

{-# OPTIONS --type-in-type
  #-}

module Hurkens where

⊥ : Set
⊥ = (A : Set) -> A

¬_ : Set -> Set
¬ A = A -> ⊥

P : Set -> Set
P A = A -> Set

U : Set
U = (X : Set) -> (P (P X) -> X) -> P (P X)

τ : P (P U) -> U
τ t = \X f p -> t \x -> p (f (x X f))

σ : U -> P (P U)
σ s = s U \t -> τ t

Δ : P U
Δ = \y -> ¬ ((p : P U) -> σ y p -> p (τ (σ y)))

Ω : U
Ω = τ \p -> (x : U) -> σ x p -> p x

D : Set
D = (p : P U) -> σ Ω p -> p (τ (σ Ω))

lem₁ : (p : P U) -> ((x : U) -> σ x p -> p x) -> p Ω
lem₁ p H1 = H1 Ω \x -> H1 (τ (σ x))

lem₂ : ¬ D
lem₂ = lem₁ Δ \x H2 H3 -> H3 Δ H2 \p -> H3 \y -> p (τ (σ y))

lem₃ : D
lem₃ p = lem₁ \y -> p (τ (σ y))

loop : ⊥
loop = lem₂ lem₃


text:
{-# OPTIONS --cubical #-}
module Cubical.Experiments.Brunerie where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Data.Bool
open import Cubical.Data.Nat
open import Cubical.Data.Int
open import Cubical.HITs.S1
open import Cubical.HITs.S2
open import Cubical.HITs.S3
open import Cubical.HITs.Join
open import Cubical.HITs.Hopf
open import Cubical.HITs.SetTruncation
open import Cubical.HITs.GroupoidTruncation
open import Cubical.HITs.2GroupoidTruncation

-- This code is adapted from examples/brunerie3.ctt on the pi4s3_nobug branch of cubicaltt

ptType : Type₁
ptType = Σ[ A ∈ Type₀ ] A

pt : ∀ (A : ptType) → A .fst
pt A = A .snd

ptBool ptS¹ ptS² ptS³ : ptType
ptBool = (Bool , true)
ptS¹ = (S¹ , base)
ptS² = (S² , base)
ptS³ = (S³ , base)

pt∥_∥₁ pt∥_∥₂ : ptType → ptType
pt∥ A , a ∥₁ = ∥ A ∥₁ , ∣ a ∣₁
pt∥ A , a ∥₂ = ∥ A ∥₂ , ∣ a ∣₂

ptjoin : ptType → Type₀ → ptType
ptjoin (A , a) B = join A B , inl a

Ω Ω² Ω³ : ptType → ptType
Ω (A , a) = (Path A a a) , refl
Ω² A = Ω (Ω A)
Ω³ A = Ω (Ω² A)

mapΩrefl : {A : ptType} {B : Type₀} (f : A .fst → B) → Ω A .fst → Ω (B , f (pt A)) .fst
mapΩrefl f p i = f (p i)

mapΩ²refl : {A : ptType} {B : Type₀} (f : A .fst → B) → Ω² A .fst → Ω² (B , f (pt A)) .fst
mapΩ²refl f p i j = f (p i j)

mapΩ³refl : {A : ptType} {B : Type₀} (f : A .fst → B) → Ω³ A .fst → Ω³ (B , f (pt A)) .fst
mapΩ³refl f p i j k = f (p i j k)

PROP SET GROUPOID TWOGROUPOID : ∀ ℓ → Type (ℓ-suc ℓ)
PROP ℓ = Σ (Type ℓ) isProp
SET ℓ = Σ (Type ℓ) isSet
GROUPOID ℓ = Σ (Type ℓ) isGroupoid
TWOGROUPOID ℓ = Σ (Type ℓ) is2Groupoid

meridS² : S¹ → Path S² base base
meridS² base _ = base
meridS² (loop i) j = surf i j

alpha : join S¹ S¹ → S²
alpha (inl x) = base
alpha (inr y) = base
alpha (push x y i) = (meridS² y ∙ meridS² x) i

connectionBoth : {A : Type₀} {a : A} (p : Path A a a) → PathP (λ i → Path A (p i) (p i)) p p
connectionBoth {a = a} p i j =
  hcomp
    (λ k → λ
      { (i = i0) → p (j ∨ ~ k)
      ; (i = i1) → p (j ∧ k)
      ; (j = i0) → p (i ∨ ~ k)
      ; (j = i1) → p (i ∧ k)
      })
    a

data PostTotalHopf : Type₀ where
  base : S¹ → PostTotalHopf
  loop : (x : S¹) → PathP (λ i → Path PostTotalHopf (base x) (base (rotLoop x (~ i)))) refl refl

tee12 : (x : S²) → HopfS² x → PostTotalHopf
tee12 base y = base y
tee12 (surf i j) y =
  hcomp
    (λ k → λ
      { (i = i0) → base y
      ; (i = i1) → base y
      ; (j = i0) → base y
      ; (j = i1) → base (rotLoopInv y (~ i) k)
      })
    (loop (unglue (i ∨ ~ i ∨ j ∨ ~ j) y) i j)

tee34 : PostTotalHopf → join S¹ S¹
tee34 (base x) = inl x
tee34 (loop x i j) =
  hcomp
    (λ k → λ
      { (i = i0) → push x x (j ∧ ~ k)
      ; (i = i1) → push x x (j ∧ ~ k)
      ; (j = i0) → inl x
      ; (j = i1) → push (rotLoop x (~ i)) x (~ k)
      })
    (push x x j)

tee : (x : S²) → HopfS² x → join S¹ S¹
tee x y = tee34 (tee12 x y)

fibΩ : {B : ptType} (P : B .fst → Type₀) → P (pt B) → Ω B .fst → Type₀
fibΩ P f p = PathP (λ i → P (p i)) f f

fibΩ² : {B : ptType} (P : B .fst → Type₀) → P (pt B) → Ω² B .fst → Type₀
fibΩ² P f = fibΩ (fibΩ P f) refl

fibΩ³ : {B : ptType} (P : B .fst → Type₀) → P (pt B) → Ω³ B .fst → Type₀
fibΩ³ P f = fibΩ² (fibΩ P f) refl

Ω³Hopf : Ω³ ptS² .fst → Type₀
Ω³Hopf = fibΩ³ HopfS² base

fibContrΩ³Hopf : ∀ p → Ω³Hopf p
fibContrΩ³Hopf p i j k =
  hcomp
    (λ m → λ
      { (i = i0) → base
      ; (i = i1) → base
      ; (j = i0) → base
      ; (j = i1) → base
      ; (k = i0) → base
      ; (k = i1) →
        isSetΩS¹ refl refl
          (λ i j → transp (λ n → HopfS² (p i j n)) (i ∨ ~ i ∨ j ∨ ~ j) base)
          (λ _ _ → base)
          m i j
      })
    (transp (λ n → HopfS² (p i j (k ∧ n))) (i ∨ ~ i ∨ j ∨ ~ j ∨ ~ k) base)

h : Ω³ ptS² .fst → Ω³ (ptjoin ptS¹ S¹) .fst
h p i j k = tee (p i j k) (fibContrΩ³Hopf p i j k)

multTwoAux : (x : S²) → Path (Path ∥ S² ∥₂ ∣ x ∣₂ ∣ x ∣₂) refl refl
multTwoAux base i j = ∣ surf i j ∣₂
multTwoAux (surf k l) i j =
  hcomp
    (λ m → λ
      { (i = i0) → ∣ surf k l ∣₂
      ; (i = i1) → ∣ surf k l ∣₂
      ; (j = i0) → ∣ surf k l ∣₂
      ; (j = i1) → ∣ surf k l ∣₂
      ; (k = i0) → ∣ surf i j ∣₂
      ; (k = i1) → ∣ surf i j ∣₂
      ; (l = i0) → ∣ surf i j ∣₂
      ; (l = i1) → squash₂ _ _ _ _ _ _ (λ k i j → step₁ k i j) refl m k i j
      })
    (step₁ k i j)

  where
  step₁ : I → I → I → ∥ S² ∥₂
  step₁ k i j =
    hcomp {A = ∥ S² ∥₂}
      (λ m → λ
        { (i = i0) → ∣ surf k (l ∧ m) ∣₂
        ; (i = i1) → ∣ surf k (l ∧ m) ∣₂
        ; (j = i0) → ∣ surf k (l ∧ m) ∣₂
        ; (j = i1) → ∣ surf k (l ∧ m) ∣₂
        ; (k = i0) → ∣ surf i j ∣₂
        ; (k = i1) → ∣ surf i j ∣₂
        ; (l = i0) → ∣ surf i j ∣₂
        })
     ∣ surf i j ∣₂

multTwoTildeAux : (t : ∥ S² ∥₂) → Path (Path ∥ S² ∥₂ t t) refl refl
multTwoTildeAux ∣ x ∣₂ = multTwoAux x
multTwoTildeAux (squash₂ _ _ _ _ _ _ t u k l m n) i j =
  squash₂ _ _ _ _ _ _
    (λ k l m → multTwoTildeAux (t k l m) i j)
    (λ k l m → multTwoTildeAux (u k l m) i j)
    k l m n

multTwoEquivAux : Path (Path (∥ S² ∥₂ ≃ ∥ S² ∥₂) (idEquiv _) (idEquiv _)) refl refl
multTwoEquivAux i j =
  ( f i j
  , hcomp
      (λ l → λ
        { (i = i0) → isPropIsEquiv _ (idIsEquiv _) (idIsEquiv _) l
        ; (i = i1) → isPropIsEquiv _ (idIsEquiv _) (idIsEquiv _) l
        ; (j = i0) → isPropIsEquiv _ (idIsEquiv _) (idIsEquiv _) l
        ; (j = i1) →
          isPropIsEquiv _
            (transp (λ k → isEquiv (f i k)) (i ∨ ~ i) (idIsEquiv _))
            (idIsEquiv _)
            l
        })
      (transp (λ k → isEquiv (f i (j ∧ k))) (i ∨ ~ i ∨ ~ j) (idIsEquiv _))
  )
  where
  f : I → I → ∥ S² ∥₂ → ∥ S² ∥₂
  f i j t = multTwoTildeAux t i j

tHopf³ : S³ → Type₀
tHopf³ base = ∥ S² ∥₂
tHopf³ (surf i j k) =
  Glue ∥ S² ∥₂
    (λ { (i = i0) → (∥ S² ∥₂ , idEquiv _)
       ; (i = i1) → (∥ S² ∥₂ , idEquiv _)
       ; (j = i0) → (∥ S² ∥₂ , idEquiv _)
       ; (j = i1) → (∥ S² ∥₂ , idEquiv _)
       ; (k = i0) → (∥ S² ∥₂ , multTwoEquivAux i j)
       ; (k = i1) → (∥ S² ∥₂ , idEquiv _)
       })

π₃S³ : Ω³ ptS³ .fst → Ω² pt∥ ptS² ∥₂ .fst
π₃S³ p i j = transp (λ k → tHopf³ (p j k i)) i0 ∣ base ∣₂

postulate
  is2GroupoidGROUPOID : ∀ {ℓ} → is2Groupoid (GROUPOID ℓ)
  isGroupoidSET : ∀ {ℓ} → isGroupoid (SET ℓ)

codeS² : S² → GROUPOID _
codeS² s = ∥ HopfS² s ∥₁ , squash₁

codeTruncS² : ∥ S² ∥₂ → GROUPOID _
codeTruncS² = rec2GroupoidTrunc is2GroupoidGROUPOID codeS²

encodeTruncS² : Ω pt∥ ptS² ∥₂ .fst → ∥ S¹ ∥₁
encodeTruncS² p = transp (λ i → codeTruncS² (p i) .fst) i0 ∣ base ∣₁

codeS¹ : S¹ → SET _
codeS¹ s = ∥ helix s ∥₀ , squash₀

codeTruncS¹ : ∥ S¹ ∥₁ → SET _
codeTruncS¹ = recGroupoidTrunc isGroupoidSET codeS¹

encodeTruncS¹ : Ω pt∥ ptS¹ ∥₁ .fst → ∥ Int ∥₀
encodeTruncS¹ p = transp (λ i → codeTruncS¹ (p i) .fst) i0 ∣ pos zero ∣₀

-- THE BIG GAME

f3 : Ω³ ptS³ .fst → Ω³ (ptjoin ptS¹ S¹) .fst
f3 = mapΩ³refl S³→joinS¹S¹

f4 : Ω³ (ptjoin ptS¹ S¹) .fst → Ω³ ptS² .fst
f4 = mapΩ³refl alpha

f5 : Ω³ ptS² .fst → Ω³ (ptjoin ptS¹ S¹) .fst
f5 = h

f6 : Ω³ (ptjoin ptS¹ S¹) .fst → Ω³ ptS³ .fst
f6 = mapΩ³refl joinS¹S¹→S³

f7 : Ω³ ptS³ .fst → Ω² pt∥ ptS² ∥₂ .fst
f7 = π₃S³

g8 : Ω² pt∥ ptS² ∥₂ .fst → Ω pt∥ ptS¹ ∥₁ .fst
g8 = mapΩrefl encodeTruncS²

g9 : Ω pt∥ ptS¹ ∥₁ .fst → ∥ Int ∥₀
g9 = encodeTruncS¹

g10 : ∥ Int ∥₀ → Int
g10 = elimSetTrunc (λ _ → isSetInt) (idfun Int)

-- don't run me
brunerie : Int
brunerie = g10 (g9 (g8 (f7 (f6 (f5 (f4 (f3 (λ i j k → surf i j k))))))))

-- simpler tests

test63 : ℕ → Int
test63 n = g10 (g9 (g8 (f7 (63n n))))
  where
  63n : ℕ → Ω³ ptS³ .fst
  63n zero i j k = surf i j k
  63n (suc n) = f6 (f3 (63n n))

foo : Ω³ ptS² .fst
foo i j k =
  hcomp
    (λ l → λ
      { (i = i0) → surf l l
      ; (i = i1) → surf l l
      ; (j = i0) → surf l l
      ; (j = i1) → surf l l
      ; (k = i0) → surf l l
      ; (k = i1) → surf l l
      })
    base

sorghum : Ω³ ptS² .fst
sorghum i j k =
  hcomp
    (λ l → λ
      { (i = i0) → surf j l
      ; (i = i1) → surf k (~ l)
      ; (j = i0) → surf k (i ∧ ~ l)
      ; (j = i1) → surf k (i ∧ ~ l)
      ; (k = i0) → surf j (i ∨ l)
      ; (k = i1) → surf j (i ∨ l)
      })
    (hcomp
      (λ l → λ
        { (i = i0) → base
        ; (i = i1) → surf j l
        ; (j = i0) → surf k i
        ; (j = i1) → surf k i
        ; (k = i0) → surf j (i ∧ l)
        ; (k = i1) → surf j (i ∧ l)
        })
      (surf k i))

goo : Ω³ ptS² .fst → Int
goo x = g10 (g9 (g8 (f7 (f6 (f5 x)))))

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
{-# OPTIONS --cubical-compatible #-}
postulate
  A : Set
  B : A → Set

T = (@0 x : A) → B x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The basic code for equational reasoning with a partial relation
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Relation.Binary

module Relation.Binary.Reasoning.Base.Partial
  {a ℓ} {A : Set a} (_∼_ : Rel A ℓ) (trans : Transitive _∼_)
  where

open import Level using (_⊔_)
open import Relation.Binary.PropositionalEquality.Core as P
  using (_≡_)

infix  4 _IsRelatedTo_
infix  3 _∎⟨_⟩
infixr 2 step-∼ step-≡ step-≡˘
infixr 2 _≡⟨⟩_
infix  1 begin_

------------------------------------------------------------------------
-- Definition of "related to"

-- This seemingly unnecessary type is used to make it possible to
-- infer arguments even if the underlying equality evaluates.

data _IsRelatedTo_ (x y : A) : Set ℓ where
  relTo : (x∼y : x ∼ y) → x IsRelatedTo y

------------------------------------------------------------------------
-- Reasoning combinators

-- Note that the arguments to the `step`s are not provided in their
-- "natural" order and syntax declarations are later used to re-order
-- them. This is because the `step` ordering allows the type-checker to
-- better infer the middle argument `y` from the `_IsRelatedTo_`
-- argument (see issue 622).
--
-- This has two practical benefits. First it speeds up type-checking by
-- approximately a factor of 5. Secondly it allows the combinators to be
-- used with macros that use reflection, e.g. `Tactic.RingSolver`, where
-- they need to be able to extract `y` using reflection.

-- Beginning of a proof

begin_ : ∀ {x y} → x IsRelatedTo y → x ∼ y
begin relTo x∼y = x∼y

-- Standard step with the relation

step-∼ : ∀ x {y z} → y IsRelatedTo z → x ∼ y → x IsRelatedTo z
step-∼ _ (relTo y∼z) x∼y = relTo (trans x∼y y∼z)

-- Step with a non-trivial propositional equality

step-≡ : ∀ x {y z} → y IsRelatedTo z → x ≡ y → x IsRelatedTo z
step-≡ _ x∼z P.refl = x∼z

-- Step with a flipped non-trivial propositional equality

step-≡˘ : ∀ x {y z} → y IsRelatedTo z → y ≡ x → x IsRelatedTo z
step-≡˘ _ x∼z P.refl = x∼z

-- Step with a trivial propositional equality

_≡⟨⟩_ : ∀ x {y} → x IsRelatedTo y → x IsRelatedTo y
_ ≡⟨⟩ x∼y = x∼y

-- Termination step

_∎⟨_⟩ : ∀ x → x ∼ x → x IsRelatedTo x
_ ∎⟨ x∼x ⟩  = relTo x∼x

-- Syntax declarations

syntax step-∼  x y∼z x∼y = x ∼⟨  x∼y ⟩ y∼z
syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z


text:
{-# OPTIONS --universe-polymorphism #-}

open import Data.Bool using ( Bool ; true ; false ; _∧_ )
open import Data.Empty using ()
open import Data.List using ( List ; [] ; _∷_ ; _++_ ; map )
open import Data.List.Any using ( here ; there )
open import Data.List.Membership.Propositional using ()
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Data.Product using ( ∃ ; ∄ ; _×_ ; _,_ )
open import Data.Unit using ()
open import Level using ( zero )
open import Relation.Binary using ()
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )
open import Relation.Nullary using ( Dec ; yes ; no )
open import Relation.Unary using ( _∈_ ; _⊆_ )

module Web.Semantic.Util where

infixr 9 _∘_

id : ∀ {X : Set} → X → X
id x = x

_∘_ : ∀ {X Y Z : Set} → (Y → Z) → (X → Y) → (X → Z)
(f ∘ g) = λ x → f (g x)

Setoid : Set₁
Setoid = Relation.Binary.Setoid zero zero

Subset : Set → Set₁
Subset X = X → Set

⁅_⁆ : ∀ {X} → X → Subset X
⁅ x ⁆ y = x ≡ y

⊆-refl : ∀ {X} (P : Subset X) → (P ⊆ P)
⊆-refl P x∈P = x∈P

_⁻¹ :  ∀ {X Y : Set} → Subset (X × Y) → Subset (Y × X)
(R ⁻¹) (y , x) = R (x , y)

-- Some proofs are classical, and depend on excluded middle.

ExclMiddle : Set₁
ExclMiddle = ∀ (X : Set) → Dec X

ExclMiddle₁ : Set₂
ExclMiddle₁ = ∀ (X : Set₁) → Dec X

smaller-excl-middle : ExclMiddle₁ → ExclMiddle
smaller-excl-middle excl-middle₁ X = X? where

  data Large : Set₁ where
    large : X → Large

  X? : Dec X
  X? with excl-middle₁ Large
  X? | yes (large x) = yes x
  X? | no ¬x         = no (λ x → ¬x (large x))

-- Some nameclashes between the standard library and semantic web terminology:
-- ⊤ and ⊥ are used for concepts, and T is used to range over T-Boxes.

open Data.Bool public using () renaming ( T to □ )
open Data.Empty public using () renaming ( ⊥ to False ; ⊥-elim to elim )
open Data.Unit public using ( tt ) renaming ( ⊤ to True )

□-proj₁ : ∀ {b c} → □(b ∧ c) → □ b
□-proj₁ {true}  □c = tt
□-proj₁ {false} ()

□-proj₂ : ∀ {b c} → □(b ∧ c) → □ c
□-proj₂ {true}  □c = □c
□-proj₂ {false} ()

-- Convert back and forth from Dec and Bool.

is : ∀ {ℓ} {X : Set ℓ} → Dec X → Bool
is (yes _) = true
is (no _) = false

is✓ : ∀ {ℓ} {X : Set ℓ} {x : Dec X} → □(is x) → X
is✓ {ℓ} {X} {yes x} _ = x
is✓ {ℓ} {X} {no _} ()

is! : ∀ {ℓ} {X : Set ℓ} {x : Dec X} → X → □(is x)
is! {ℓ} {X} {yes _} x = tt
is! {ℓ} {X} {no ¬x} x = ¬x x

-- Finite sets are ones backed by a list

open Data.List.Membership.Propositional  public using () renaming ( _∈_ to _∈ˡ_ )

Finite : Set → Set
Finite X = ∃ λ xs → ∀ (x : X) → (x ∈ˡ xs)

False∈Fin : False ∈ Finite
False∈Fin = ([] , λ ())

⊎-resp-Fin : ∀ {X Y} → (X ∈ Finite) → (Y ∈ Finite) → ((X ⊎ Y) ∈ Finite)
⊎-resp-Fin {X} {Y} (xs , ∀x∙x∈xs) (ys , ∀y∙y∈ys) =
  ((map inj₁ xs ++ map inj₂ ys) , lemma) where

  lemma₁ : ∀ {x : X} {xs : List X} →
    (x ∈ˡ xs) → (inj₁ x ∈ˡ (map inj₁ xs ++ map inj₂ ys))
  lemma₁ (here refl) = here refl
  lemma₁ (there x∈xs) = there (lemma₁ x∈xs)

  lemma₂ : ∀ (xs : List X) {y : Y} {ys : List Y} →
    (y ∈ˡ ys) → (inj₂ y ∈ˡ (map inj₁ xs ++ map inj₂ ys))
  lemma₂ [] (here refl) = here refl
  lemma₂ [] (there y∈ys) = there (lemma₂ [] y∈ys)
  lemma₂ (x ∷ xs) y∈ys = there (lemma₂ xs y∈ys)

  lemma : ∀ x → (x ∈ˡ (map inj₁ xs ++ map inj₂ ys))
  lemma (inj₁ x) = lemma₁ (∀x∙x∈xs x)
  lemma (inj₂ y) = lemma₂ xs (∀y∙y∈ys y)

-- symmetric monoidal structure of sum

_⟨⊎⟩_ : ∀ {W X Y Z : Set} → (W → X) → (Y → Z) → (W ⊎ Y) → (X ⊎ Z)
_⟨⊎⟩_ f g (inj₁ x) = inj₁ (f x)
_⟨⊎⟩_ f g (inj₂ y) = inj₂ (g y)

_≡⊎≡_ : ∀ {X Y Z : Set} {f g : (X ⊎ Y) → Z} →
  (∀ x → (f (inj₁ x) ≡ g (inj₁ x))) → (∀ x → (f (inj₂ x) ≡ g (inj₂ x))) →
    ∀ x → (f x ≡ g x)
(f₁≡g₁ ≡⊎≡ f₂≡g₂) (inj₁ x) = f₁≡g₁ x
(f₁≡g₁ ≡⊎≡ f₂≡g₂) (inj₂ y) = f₂≡g₂ y

⊎-swap : ∀ {X Y : Set} → (X ⊎ Y) → (Y ⊎ X)
⊎-swap (inj₁ x) = inj₂ x
⊎-swap (inj₂ y) = inj₁ y

⊎-assoc : ∀ {X Y Z : Set} → ((X ⊎ Y) ⊎ Z) → (X ⊎ (Y ⊎ Z))
⊎-assoc (inj₁ (inj₁ x)) = inj₁ x
⊎-assoc (inj₁ (inj₂ y)) = inj₂ (inj₁ y)
⊎-assoc (inj₂ z) = inj₂ (inj₂ z)

⊎-assoc⁻¹ : ∀ {X Y Z : Set} → (X ⊎ (Y ⊎ Z)) → ((X ⊎ Y) ⊎ Z)
⊎-assoc⁻¹ (inj₁ x) = inj₁ (inj₁ x)
⊎-assoc⁻¹ (inj₂ (inj₁ y)) = inj₁ (inj₂ y)
⊎-assoc⁻¹ (inj₂ (inj₂ z)) = inj₂ z

⊎-unit₁ : ∀ {X : Set} → (False ⊎ X) → X
⊎-unit₁ (inj₁ ())
⊎-unit₁ (inj₂ x) = x

⊎-unit₂ : ∀ {X : Set} → (X ⊎ False) → X
⊎-unit₂ (inj₁ x) = x
⊎-unit₂ (inj₂ ())

inj⁻¹ : ∀ {X : Set} → (X ⊎ X) → X
inj⁻¹ (inj₁ x) = x
inj⁻¹ (inj₂ x) = x

-- A set divided, like Gaul, into three parts

infix 6 _⊕_⊕_

data _⊕_⊕_ (X V Y : Set) : Set where
  inode : (x : X) → (X ⊕ V ⊕ Y) -- Imported node
  bnode : (v : V) → (X ⊕ V ⊕ Y) -- Blank node
  enode : (y : Y) → (X ⊕ V ⊕ Y) -- Exported node

_⟨⊕⟩_⟨⊕⟩_ : ∀ {U V W X Y Z} → (W → X) → (U → V) → (Y → Z) →
  (W ⊕ U ⊕ Y) → (X ⊕ V ⊕ Z)
(f ⟨⊕⟩ g ⟨⊕⟩ h) (inode w) = inode (f w)
(f ⟨⊕⟩ g ⟨⊕⟩ h) (bnode u) = bnode (g u)
(f ⟨⊕⟩ g ⟨⊕⟩ h) (enode y) = enode (h y)

_[⊕]_[⊕]_ : ∀ {X V Y Z : Set} → (X → Z) → (V → Z) → (Y → Z) →
   (X ⊕ V ⊕ Y) → Z
(f [⊕] g [⊕] h) (inode x) = f x
(f [⊕] g [⊕] h) (bnode v) = g v
(f [⊕] g [⊕] h) (enode y) = h y

left : ∀ {V W X Y Z} → (X ⊕ V ⊕ Y) → (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z)
left (inode x) = inode x
left (bnode v) = bnode (inode v)
left (enode y) = bnode (bnode y)

right : ∀ {V W X Y Z} → (Y ⊕ W ⊕ Z) → (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z)
right (inode y) = bnode (bnode y)
right (bnode w) = bnode (enode w)
right (enode z) = enode z

hmerge : ∀ {V W X Y Z A : Set} →
  ((X ⊕ V ⊕ Y) → A) → ((Y ⊕ W ⊕ Z) → A) →
    (X ⊕ (V ⊕ Y ⊕ W) ⊕ Z) → A
hmerge f g (inode x)         = f (inode x)
hmerge f g (bnode (inode v)) = f (bnode v)
hmerge f g (bnode (bnode y)) = g (inode y)
hmerge f g (bnode (enode w)) = g (bnode w)
hmerge f g (enode z)         = g (enode z)

→-dist-⊕ : ∀ {V X Y Z : Set} → ((X ⊕ V ⊕ Y) → Z) →
  ((X → Z) × (V → Z) × (Y → Z))
→-dist-⊕ i = ((i ∘ inode) , (i ∘ bnode) , (i ∘ enode))

up : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (X₁ ⊕ V₁ ⊕ Y₁) →
  ((X₁ ⊎ X₂) ⊕ (V₁ ⊎ V₂) ⊕ (Y₁ ⊎ Y₂))
up (inode x) = inode (inj₁ x)
up (bnode v) = bnode (inj₁ v)
up (enode y) = enode (inj₁ y)

down : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂} → (X₂ ⊕ V₂ ⊕ Y₂) →
  ((X₁ ⊎ X₂) ⊕ (V₁ ⊎ V₂) ⊕ (Y₁ ⊎ Y₂))
down (inode x) = inode (inj₂ x)
down (bnode v) = bnode (inj₂ v)
down (enode y) = enode (inj₂ y)

vmerge : ∀ {V₁ V₂ X₁ X₂ Y₁ Y₂ A : Set} →
  ((X₁ ⊕ V₁ ⊕ Y₁) → A) → ((X₂ ⊕ V₂ ⊕ Y₂) → A) →
    ((X₁ ⊎ X₂) ⊕ (V₁ ⊎ V₂) ⊕ (Y₁ ⊎ Y₂)) → A
vmerge j k (inode (inj₁ x)) = j (inode x)
vmerge j k (inode (inj₂ x)) = k (inode x)
vmerge j k (bnode (inj₁ v)) = j (bnode v)
vmerge j k (bnode (inj₂ v)) = k (bnode v)
vmerge j k (enode (inj₁ y)) = j (enode y)
vmerge j k (enode (inj₂ y)) = k (enode y)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


text:
module Fail.TuplePat where

open import Haskell.Prelude

fst₃ : a × b × c → a
fst₃ (x ∷ xs) = x

{-# COMPILE AGDA2HS fst₃ #-}


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Lens | L

type
  S : 0-ary
  A : 0-ary

term
  get : S  ->  A
  put : S  A  ->  S

theory
  (PG) s : S  a : A   |> get (put (s, a))   = a
  (GP) s : S          |> put (s, get(s))    = s
  (PP) s : S  a b : A |> put (put(s, a), b) = put (s, a)
-}

module Lens.Signature where

open import SOAS.Context

-- Type declaration
data LT : Set where
  S : LT
  A : LT

open import SOAS.Syntax.Signature LT public
open import SOAS.Syntax.Build LT public

-- Operator symbols
data Lₒ : Set where
  getₒ putₒ : Lₒ

-- Term signature
L:Sig : Signature Lₒ
L:Sig = sig λ
  {  getₒ  → (⊢₀ S) ⟼₁ A
  ;  putₒ  → (⊢₀ S) , (⊢₀ A) ⟼₂ S
  }

open Signature L:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

module Cubical.HITs.Modulo.Properties where

open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Fin
open import Cubical.Data.Sigma

open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence

open import Cubical.HITs.Modulo.Base
open import Cubical.HITs.Modulo.FinEquiv public

private
  variable
    ℓ : Level
    k : ℕ

-- `Modulo 0` is easily shown equivalent to `ℕ`, because we don't need
-- to account for the path constructor at all.
Modulo0≡ℕ : Modulo 0 ≡ ℕ
Modulo0≡ℕ = isoToPath lemma
 where
 open Iso
 lemma : Iso (Modulo 0) ℕ
 fun lemma (embed n) = n
 inv lemma = embed
 rightInv lemma n = refl
 leftInv lemma (embed n) = refl

isSetModulo0 : isSet (Modulo 0)
isSetModulo0 = subst isSet (sym Modulo0≡ℕ) isSetℕ

-- `Modulo 1` is contractible just like `Fin 1`
isContrModulo1 : isContr (Modulo 1)
isContrModulo1
  = value , λ
  { (embed n) → universal n
  ; (step n i) → universal-path n i
  }
  where
  value : Modulo 1
  value = embed 0

  universal : ∀ n → value ≡ embed n
  universal zero = refl
  universal (suc n) = universal n ∙ step n

  universal-path
   : ∀ n → PathP (λ i → value ≡ step n i) (universal n) (universal (suc n))
  universal-path n i j
    = compPath-filler (universal n) (step n) i j

-- `expand o k m` is congruent to `m` modulo `k`, so there is a path
-- between their image in `Modulo k`.
steps : ∀ m o → embed {k = k} m ≡ embed (expand o k m)
steps m zero = refl
steps {k} m (suc o) = steps m o ∙ ztep (expand o k m)

steps≡
  : ∀ m n
  → PathP (λ i → embed {k} m ≡ ztep (expand n k m) i)
      (steps m n)
      (steps m (suc n))
steps≡ m n = λ i j → compPath-filler (steps m n) (ztep (expand n _ m)) i j

stepOver : ∀ m n o → expand o k m ≡ n → embed {k = k} m ≡ embed n
stepOver m n o p = steps m o ∙ cong embed p

-- `Modulo k` is a set for all `k`, because we can transport the
-- evidence from either `ℕ` or `Fin k`.
isSetModulo : isSet (Modulo k)
isSetModulo {0} = isSetModulo0
isSetModulo {suc k} = subst isSet (sym Modulo≡Fin) isSetFin


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Constraints( x : X) where
  open X(x)

  data Strata : Set where
    Flat : Strata
    Extended : Strata

  data Implication (knot : Set → Set)(n : Set) : Set where
    ∃_·_⊃_ : (v : ℕ) → QConstraint n → knot (n ⨁ v) → Implication knot n

  {- SYNTAX -}
  data Constraint (n : Set) : Strata → Set where
    QC : ∀ {x} → QConstraint n → Constraint n x
    Imp : Implication (λ n → Constraint n Flat) n → Constraint n Flat
    Imp′ : QConstraint n → Constraint n Extended → Constraint n Extended
    _∧′_ : ∀ {x} → Constraint n x → Constraint n x → Constraint n x
    Ⅎ_ : Constraint (Ⓢ n) Extended → Constraint n Extended

  ε′ : ∀ {n}{x} → Constraint n x
  ε′ = QC ε

  _∼′_ : ∀ {n}{x} → Type n → Type n → Constraint n x
  τ₁ ∼′ τ₂ = QC (τ₁ ∼ τ₂)

  Ⅎ′_·_ : {n : Set}(v : ℕ) → Constraint (n ⨁ v) Extended → Constraint n Extended
  Ⅎ′ (suc n) · c = Ⅎ (Ⅎ′ n · c)
  Ⅎ′ zero · c = c

  infixl 6 Ⅎ′_·_
{-
  toAE : {n : Set}{s : Strata} → Constraint n s → Constraint n Extended
  toAE (QC x) = QC x
  toAE (a ∧′ b) = toAE a ∧′ toAE b
  toAE (Imp (∃ n · Q ⊃ C)) = Imp (∃ n · Q ⊃ toAE C)
  toAE (Ⅎ c) = Ⅎ c
-}
  infixl 6 Ⅎ_

  infixl 7 _∧′_

  {- INSTANCES -}
  private
    pn-is-functor = λ {n} → Monad.is-functor (PlusN-is-monad {n})
    module PlusN-f n = Functor (Monad.is-functor (PlusN-is-monad {n}))
    module Ⓢ-f = Functor Ⓢ-is-functor
    module Type-f = Functor (type-is-functor)
    module QC-f = Functor (qconstraint-is-functor)

  private
    fmap-c : ∀ {s}{a b} → (a → b) → Constraint a s → Constraint b s
    fmap-c f (QC x) = QC (QC-f.map f x)
    fmap-c f (C₁ ∧′ C₂) = (fmap-c f C₁) ∧′ (fmap-c f C₂)
    fmap-c f (Imp′ Q C) = Imp′ (QC-f.map f Q) (fmap-c f C)
    fmap-c f (Imp (∃ n · Q ⊃ C)) = Imp (∃ n · (QC-f.map f Q) ⊃ (fmap-c (pn.map f) C))
      where module pn = PlusN-f n
    fmap-c f (Ⅎ C) = Ⅎ (fmap-c (Ⓢ-f.map f) C)
    fmap-c-id : ∀{s}{A : Set} {f : A → A} → isIdentity f → isIdentity (fmap-c {s} f)
    fmap-c-id {f = f} isid {QC x       } = cong QC (QC-f.identity isid)
    fmap-c-id {f = f} isid {Imp′ Q C   } = cong₂ Imp′ (QC-f.identity isid) (fmap-c-id isid)
    fmap-c-id {f = f} isid {Imp(∃ n · Q ⊃ C)} = cong Imp
                                                     (cong₂ (∃_·_⊃_ n)
                                                            (QC-f.identity isid)
                                                            (fmap-c-id (pn.identity isid)))
        where module pn = PlusN-f n
    fmap-c-id {f = f} isid {C₁ ∧′ C₂} = cong₂ _∧′_ (fmap-c-id isid) (fmap-c-id isid)
    fmap-c-id {f = f} isid {Ⅎ C    }  = cong Ⅎ_ (fmap-c-id (Ⓢ-f.identity isid))
    fmap-c-comp : {s : Strata}{A B C : Set} {f : A → B} {g : B → C} {x : Constraint A s}
                → fmap-c (g ∘ f) x ≡ fmap-c g (fmap-c f x)
    fmap-c-comp {x = QC x} = cong QC QC-f.composite
    fmap-c-comp {x = Imp′ Q C} = cong₂ Imp′ (QC-f.composite) (fmap-c-comp)
    fmap-c-comp {x = C₁ ∧′ C₂} = cong₂ _∧′_ (fmap-c-comp {x = C₁}) (fmap-c-comp {x = C₂})
    fmap-c-comp {x = Ⅎ C} = cong Ⅎ_ (combine-composite′ ⦃ Ⓢ-is-functor ⦄ fmap-c fmap-c-comp)
    fmap-c-comp {x = Imp(∃ n · Q ⊃ C)} = cong Imp
                                              (cong₂ (∃_·_⊃_ n) QC-f.composite
                                                     (combine-composite′ ⦃ pn-is-functor {n}⦄
                                                                         fmap-c fmap-c-comp))
      where module pn = PlusN-f n

  constraint-is-functor : ∀ {s : Strata} → Functor (λ n → Constraint n s)
  constraint-is-functor = record { map = fmap-c
                                 ; identity = fmap-c-id
                                 ; composite = fmap-c-comp
                                 }

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
module Agda.Builtin.TrustMe where

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Erase

private
  postulate
    unsafePrimTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y

primTrustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
primTrustMe = primEraseEquality unsafePrimTrustMe

{-# DISPLAY primEraseEquality unsafePrimTrustMe = primTrustMe #-}

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda