text:
------------------------------------------------------------------------
-- A variant of the propositional truncation operator with an erased
-- truncation constructor
------------------------------------------------------------------------

-- Partly following the HoTT book, but adapted for erasure.

{-# OPTIONS --erased-cubical --safe #-}

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the propositional truncation
-- operator uses path equality, but the supplied notion of equality is
-- used for many other things.

import Equality.Path as P

module H-level.Truncation.Propositional.Erased
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Prelude as P
open import Logical-equivalence using (_⇔_)

open import Bijection equality-with-J as Bijection using (_↔_)
import Colimit.Sequential.Very-erased eq as C
open import Embedding equality-with-J as Emb using (Is-embedding)
open import Equality.Decidable-UIP equality-with-J
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq
  using (_≃_; Is-equivalence)
open import Equivalence.Erased equality-with-J as EEq
  using (_≃ᴱ_; Is-equivalenceᴱ)
open import Equivalence.Erased.Contractible-preimages equality-with-J
  as ECP using (Contractibleᴱ; _⁻¹ᴱ_)
open import Equivalence-relation equality-with-J
open import Erased.Cubical eq as Er
  using (Erased; [_]; erased; Very-stableᴱ-≡; Erased-singleton)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional.One-step eq as O
  using (∥_∥¹-out-^)
import H-level.Truncation.Propositional.Non-recursive.Erased eq as N
open import Monad equality-with-J
open import Preimage equality-with-J using (_⁻¹_)
open import Surjection equality-with-J as S
  using (_↠_; Split-surjective)

private
  variable
    a b ℓ p r         : Level
    A A₁ A₂ B B₁ B₂ C : Type a
    P Q               : A → Type p
    R                 : A → A → Type r
    f g k x y         : A

------------------------------------------------------------------------
-- The type former

-- A propositional truncation operator with an erased higher
-- constructor.

data ∥_∥ᴱ (A : Type a) : Type a where
  ∣_∣                           : A → ∥ A ∥ᴱ
  @0 truncation-is-propositionᴾ : P.Is-proposition ∥ A ∥ᴱ

-- The truncation produces propositions (in erased contexts).

@0 truncation-is-proposition : Is-proposition ∥ A ∥ᴱ
truncation-is-proposition =
  _↔_.from (H-level↔H-level 1) truncation-is-propositionᴾ

------------------------------------------------------------------------
-- Eliminators

-- A dependent eliminator, expressed using paths.

record Elimᴾ′ {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ : (x : A) → P ∣ x ∣

    @0 truncation-is-propositionʳ :
      (p : P x) (q : P y) →
      P.[ (λ i → P (truncation-is-propositionᴾ x y i)) ] p ≡ q

open Elimᴾ′ public

elimᴾ′ : Elimᴾ′ P → (x : ∥ A ∥ᴱ) → P x
elimᴾ′ {A = A} {P = P} e = helper
  where
  module E = Elimᴾ′ e

  helper : (x : ∥ A ∥ᴱ) → P x
  helper ∣ x ∣                              = E.∣∣ʳ x
  helper (truncation-is-propositionᴾ x y i) =
    E.truncation-is-propositionʳ (helper x) (helper y) i

-- A possibly more useful dependent eliminator, expressed using paths.

record Elimᴾ {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ : (x : A) → P ∣ x ∣

    @0 truncation-is-propositionʳ :
      (x : ∥ A ∥ᴱ) → P.Is-proposition (P x)

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : ∥ A ∥ᴱ) → P x
elimᴾ e = elimᴾ′ λ where
    .∣∣ʳ                            → E.∣∣ʳ
    .truncation-is-propositionʳ _ _ →
      P.heterogeneous-irrelevance E.truncation-is-propositionʳ
  where
  module E = Elimᴾ e

-- A non-dependent eliminator, expressed using paths.

record Recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ                           : A → B
    @0 truncation-is-propositionʳ : P.Is-proposition B

open Recᴾ public

recᴾ : Recᴾ A B → ∥ A ∥ᴱ → B
recᴾ r = elimᴾ λ where
    .∣∣ʳ                          → R.∣∣ʳ
    .truncation-is-propositionʳ _ → R.truncation-is-propositionʳ
  where
  module R = Recᴾ r

-- A dependently typed eliminator.

record Elim {A : Type a} (P : ∥ A ∥ᴱ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ : (x : A) → P ∣ x ∣

    @0 truncation-is-propositionʳ :
      (x : ∥ A ∥ᴱ) → Is-proposition (P x)

open Elim public

elim : Elim P → (x : ∥ A ∥ᴱ) → P x
elim e = elimᴾ λ where
    .∣∣ʳ                        → E.∣∣ʳ
    .truncation-is-propositionʳ →
      _↔_.to (H-level↔H-level 1) ∘ E.truncation-is-propositionʳ
  where
  module E = Elim e

-- Primitive "recursion".

record Rec (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ                           : A → B
    @0 truncation-is-propositionʳ : Is-proposition B

open Rec public

rec : Rec A B → ∥ A ∥ᴱ → B
rec r = recᴾ λ where
    .∣∣ʳ                        → R.∣∣ʳ
    .truncation-is-propositionʳ →
      _↔_.to (H-level↔H-level 1) R.truncation-is-propositionʳ
  where
  module R = Rec r

------------------------------------------------------------------------
-- Conversion functions

-- ∥_∥ᴱ is pointwise equivalent to N.∥_∥ᴱ.

∥∥ᴱ≃∥∥ᴱ : ∥ A ∥ᴱ ≃ N.∥ A ∥ᴱ
∥∥ᴱ≃∥∥ᴱ = Eq.↔→≃
  (rec λ where
     .∣∣ʳ                        → N.∣_∣
     .truncation-is-propositionʳ → N.∥∥ᴱ-proposition)
  (N.elim λ where
     .N.∣∣ʳ               → ∣_∣
     .N.is-propositionʳ _ → truncation-is-proposition)
  (N.elim λ where
     .N.∣∣ʳ _             → refl _
     .N.is-propositionʳ _ → mono₁ 1 N.∥∥ᴱ-proposition)
  (elim λ where
     .∣∣ʳ _                        → refl _
     .truncation-is-propositionʳ _ → mono₁ 1 truncation-is-proposition)

------------------------------------------------------------------------
-- Some preservation lemmas and related results

-- A map function.

∥∥ᴱ-map : (A → B) → ∥ A ∥ᴱ → ∥ B ∥ᴱ
∥∥ᴱ-map f = rec λ where
  .∣∣ʳ                        → ∣_∣ ∘ f
  .truncation-is-propositionʳ → truncation-is-proposition

mutual

  -- If A and B are logically equivalent, then there is an equivalence
  -- with erased proofs between ∥ A ∥ᴱ and ∥ B ∥ᴱ.

  ∥∥ᴱ-cong-⇔ : A ⇔ B → ∥ A ∥ᴱ ≃ᴱ ∥ B ∥ᴱ
  ∥∥ᴱ-cong-⇔ A⇔B = ∥∥ᴱ-cong-⇔′ (∣_∣ ∘ _⇔_.to A⇔B) (∣_∣ ∘ _⇔_.from A⇔B)

  -- A variant of the previous result.

  ∥∥ᴱ-cong-⇔′ : (A → ∥ B ∥ᴱ) → (B → ∥ A ∥ᴱ) → ∥ A ∥ᴱ ≃ᴱ ∥ B ∥ᴱ
  ∥∥ᴱ-cong-⇔′ A→∥B∥ B→∥A∥ = EEq.⇔→≃ᴱ
    truncation-is-proposition
    truncation-is-proposition
    (rec λ where
       .∣∣ʳ                        → A→∥B∥
       .truncation-is-propositionʳ → truncation-is-proposition)
    (rec λ where
       .∣∣ʳ                        → B→∥A∥
       .truncation-is-propositionʳ → truncation-is-proposition)

-- If there is a split surjection from A to B, then there is a split
-- surjection from ∥ A ∥ᴱ to ∥ B ∥ᴱ.

∥∥ᴱ-cong-↠ : A ↠ B → ∥ A ∥ᴱ ↠ ∥ B ∥ᴱ
∥∥ᴱ-cong-↠ A↠B = record
  { logical-equivalence = record
    { to   = ∥∥ᴱ-map (_↠_.to   A↠B)
    ; from = ∥∥ᴱ-map (_↠_.from A↠B)
    }
  ; right-inverse-of = elim λ where
      .∣∣ʳ x →
        ∣ _↠_.to A↠B (_↠_.from A↠B x) ∣  ≡⟨ cong ∣_∣ (_↠_.right-inverse-of A↠B x) ⟩∎
        ∣ x ∣                            ∎
      .truncation-is-propositionʳ _ →
        mono₁ 1 truncation-is-proposition
  }

private

  ∥∥ᴱ-cong-↔ : A ↔ B → ∥ A ∥ᴱ ↔ ∥ B ∥ᴱ
  ∥∥ᴱ-cong-↔ A↔B = record
    { surjection      = ∥∥ᴱ-cong-↠ (_↔_.surjection A↔B)
    ; left-inverse-of = elim λ where
        .∣∣ʳ x →
          ∣ _↔_.from A↔B (_↔_.to A↔B x) ∣  ≡⟨ cong ∣_∣ (_↔_.left-inverse-of A↔B x) ⟩∎
          ∣ x ∣                            ∎
        .truncation-is-propositionʳ _ →
          mono₁ 1 truncation-is-proposition
    }

-- The truncation operator preserves "symmetric" functions.

∥∥ᴱ-cong : A ↝[ ⌊ k ⌋-sym ] B → ∥ A ∥ᴱ ↝[ ⌊ k ⌋-sym ] ∥ B ∥ᴱ
∥∥ᴱ-cong {k = logical-equivalence} = _≃ᴱ_.logical-equivalence ∘
                                     ∥∥ᴱ-cong-⇔
∥∥ᴱ-cong {k = bijection}           = ∥∥ᴱ-cong-↔
∥∥ᴱ-cong {k = equivalence}         = from-isomorphism ∘ ∥∥ᴱ-cong-↔ ∘
                                     from-isomorphism
∥∥ᴱ-cong {k = equivalenceᴱ}        = ∥∥ᴱ-cong-⇔ ∘
                                     _≃ᴱ_.logical-equivalence

------------------------------------------------------------------------
-- Some bijections/erased equivalences

-- If the underlying type is a proposition, then truncations of the
-- type are isomorphic to the type itself.

∥∥ᴱ↔ : @0 Is-proposition A → ∥ A ∥ᴱ ↔ A
∥∥ᴱ↔ A-prop = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec λ where
          .∣∣ʳ                        → id
          .truncation-is-propositionʳ → A-prop
      ; from = ∣_∣
      }
    ; right-inverse-of = λ _ → refl _
    }
  ; left-inverse-of = elim λ where
      .∣∣ʳ _                        → refl _
      .truncation-is-propositionʳ _ → mono₁ 1 truncation-is-proposition
  }

-- If A is merely inhabited, then the truncation of A is equivalent
-- (with erased proofs) to the unit type.

inhabited⇒∥∥ᴱ≃ᴱ⊤ : ∥ A ∥ᴱ → ∥ A ∥ᴱ ≃ᴱ ⊤
inhabited⇒∥∥ᴱ≃ᴱ⊤ ∥a∥ =
  EEq.inhabited→Is-proposition→≃ᴱ⊤ ∥a∥ truncation-is-proposition

-- If A is not inhabited, then the propositional truncation of A is
-- isomorphic to the empty type.

not-inhabited⇒∥∥ᴱ↔⊥ : ¬ A → ∥ A ∥ᴱ ↔ ⊥ {ℓ = ℓ}
not-inhabited⇒∥∥ᴱ↔⊥ {A = A} =
  ¬ A         ↝⟨ (λ ¬a → rec λ where
                           .∣∣ʳ                        → ¬a
                           .truncation-is-propositionʳ → ⊥-propositional) ⟩
  ¬ ∥ A ∥ᴱ    ↝⟨ inverse ∘ Bijection.⊥↔uninhabited ⟩□
  ∥ A ∥ᴱ ↔ ⊥  □

-- The negation of the truncation of A is isomorphic to the negation
-- of A.

¬∥∥ᴱ↔¬ : ¬ ∥ A ∥ᴱ ↔ ¬ A
¬∥∥ᴱ↔¬ {A = A} = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f → f ∘ ∣_∣
      ; from = λ ¬A → rec λ where
                        .∣∣ʳ                        → ¬A
                        .truncation-is-propositionʳ → ⊥-propositional
      }
    ; right-inverse-of = λ _ → ¬-propositional ext _ _
    }
  ; left-inverse-of = λ _ → ¬-propositional ext _ _
  }

-- A form of idempotence for binary sums.

idempotent : ∥ A ⊎ A ∥ᴱ ≃ᴱ ∥ A ∥ᴱ
idempotent = ∥∥ᴱ-cong-⇔ (record { to = P.[ id , id ]; from = inj₁ })

------------------------------------------------------------------------
-- The universal property, and some related results

mutual

  -- The propositional truncation operator's universal property.
  --
  -- See also Quotient.Erased.Σ→Erased-Constant≃∥∥ᴱ→.

  universal-property :
    @0 Is-proposition B →
    (∥ A ∥ᴱ → B) ≃ (A → B)
  universal-property B-prop = universal-property-Π (λ _ → B-prop)

  -- A generalisation of the universal property.

  universal-property-Π :
    @0 (∀ x → Is-proposition (P x)) →
    ((x : ∥ A ∥ᴱ) → P x) ≃ ((x : A) → P ∣ x ∣)
  universal-property-Π {A = A} {P = P} P-prop =
    ((x : ∥ A ∥ᴱ) → P x)      ↝⟨ Eq.↔⇒≃ (record
                                   { surjection = record
                                     { logical-equivalence = record
                                       { to   = λ f → ∣ f ∘ ∣_∣ ∣
                                       ; from = rec λ where
                                           .∣∣ʳ f → elim λ where
                                             .∣∣ʳ                        → f
                                             .truncation-is-propositionʳ → P-prop
                                           .truncation-is-propositionʳ →
                                             Π-closure ext 1 λ _ → P-prop _
                                       }
                                     ; right-inverse-of = elim λ where
                                         .∣∣ʳ _                        → refl _
                                         .truncation-is-propositionʳ _ →
                                           mono₁ 1 truncation-is-proposition
                                     }
                                   ; left-inverse-of = λ f → ⟨ext⟩ $ elim λ where
                                       .∣∣ʳ _                        → refl _
                                       .truncation-is-propositionʳ _ →
                                         mono₁ 1 (P-prop _)
                                   }) ⟩
    ∥ ((x : A) → P ∣ x ∣) ∥ᴱ  ↔⟨ ∥∥ᴱ↔ (Π-closure ext 1 λ _ → P-prop _) ⟩□
    ((x : A) → P ∣ x ∣)       □

-- The universal property computes in the "right" way.

_ :
  (@0 B-prop : Is-proposition B)
  (f : ∥ A ∥ᴱ → B) →
  _≃_.to (universal-property B-prop) f ≡ f ∘ ∣_∣
_ = λ _ _ → refl _

_ :
  (@0 B-prop : Is-proposition B)
  (f : A → B) (x : A) →
  _≃_.from (universal-property B-prop) f ∣ x ∣ ≡ f x
_ = λ _ _ _ → refl _

-- Functions from ∥ A ∥ᴱ can be expressed as functions from A along
-- with some erased data.

∥∥ᴱ→≃ :
  (∥ A ∥ᴱ → B)
    ≃
  (∃ λ (f : A → B) →
     Erased (∃ λ (g : ∀ n → ∥ A ∥¹-out-^ (suc n) → B) →
               (∀ x → g zero O.∣ x ∣ ≡ f x) ×
               (∀ n x → g (suc n) O.∣ x ∣ ≡ g n x)))
∥∥ᴱ→≃ {A = A} {B = B} =
  (∥ A ∥ᴱ → B)                                           ↝⟨ →-cong ext ∥∥ᴱ≃∥∥ᴱ F.id ⟩

  (N.∥ A ∥ᴱ → B)                                         ↝⟨ C.universal-property ⟩□

  (∃ λ (f : A → B) →
     Erased (∃ λ (g : ∀ n → ∥ A ∥¹-out-^ (suc n) → B) →
               (∀ x → g zero O.∣ x ∣ ≡ f x) ×
               (∀ n x → g (suc n) O.∣ x ∣ ≡ g n x)))     □

-- A function of type (x : ∥ A ∥ᴱ) → P x, along with an erased proof
-- showing that the function is equal to some erased function, is
-- equivalent to a function of type (x : A) → P ∣ x ∣, along with an
-- erased equality proof.

Σ-Π-∥∥ᴱ-Erased-≡-≃ :
  {@0 g : (x : ∥ A ∥ᴱ) → P x} →
  (∃ λ (f : (x : ∥ A ∥ᴱ) → P x) → Erased (f ≡ g)) ≃
  (∃ λ (f : (x : A) → P ∣ x ∣) → Erased (f ≡ g ∘ ∣_∣))
Σ-Π-∥∥ᴱ-Erased-≡-≃ {A = A} {P = P} {g = g} =
  (∃ λ (f : (x : ∥ A ∥ᴱ) → P x) → Erased (f ≡ g))       ↝⟨ (Σ-cong lemma λ _ → Er.Erased-cong (inverse $ Eq.≃-≡ lemma)) ⟩

  (∃ λ (f : (x : N.∥ A ∥ᴱ) → P (_≃_.from ∥∥ᴱ≃∥∥ᴱ x)) →
     Erased (f ≡ g ∘ _≃_.from ∥∥ᴱ≃∥∥ᴱ))                 ↝⟨ N.Σ-Π-∥∥ᴱ-Erased-≡-≃ ⟩□

  (∃ λ (f : (x : A) → P ∣ x ∣) → Erased (f ≡ g ∘ ∣_∣))  □
  where
  lemma = Π-cong-contra ext (inverse ∥∥ᴱ≃∥∥ᴱ) λ _ → Eq.id

------------------------------------------------------------------------
-- Some results based on "Generalizations of Hedberg's Theorem" by
-- Kraus, Escardó, Coquand and Altenkirch

-- Types with constant endofunctions are "h-stable" (meaning that
-- "mere inhabitance" implies inhabitance).

constant-endofunction⇒h-stable :
  {f : A → A} → @0 Constant f → ∥ A ∥ᴱ → A
constant-endofunction⇒h-stable {A = A} {f = f} c =
  ∥ A ∥ᴱ                            ↝⟨ (rec λ where
                                          .∣∣ʳ x → f x , [ c (f x) x ]
                                          .truncation-is-propositionʳ → prop) ⟩
  (∃ λ (x : A) → Erased (f x ≡ x))  ↝⟨ proj₁ ⟩□
  A                                 □
  where
  @0 prop : _
  prop =                                       $⟨ fixpoint-lemma f c ⟩
    Is-proposition (∃ λ x → f x ≡ x)           ↝⟨ H-level-cong _ 1 (∃-cong λ _ → inverse $ Er.erased Er.Erased↔) ⦂ (_ → _) ⟩□
    Is-proposition (∃ λ x → Erased (f x ≡ x))  □

-- Having a constant endofunction is logically equivalent to being
-- h-stable.

constant-endofunction⇔h-stable :
  (∃ λ (f : A → A) → Erased (Constant f)) ⇔ (∥ A ∥ᴱ → A)
constant-endofunction⇔h-stable = record
  { to   = λ (_ , [ c ]) → constant-endofunction⇒h-stable c
  ; from = λ f → f ∘ ∣_∣
         , [ (λ x y →
                f ∣ x ∣  ≡⟨ cong f $ truncation-is-proposition _ _ ⟩∎
                f ∣ y ∣  ∎)
           ]
  }

------------------------------------------------------------------------
-- Some results related to _×_

-- The cartesian product of the truncation of A and A is equivalent
-- (with erased "proofs") to A.

∥∥ᴱ×≃ᴱ : (∥ A ∥ᴱ × A) ≃ᴱ A
∥∥ᴱ×≃ᴱ = EEq.↔→≃ᴱ
  proj₂
  (λ x → ∣ x ∣ , x)
  refl
  (λ _ → cong (_, _) (truncation-is-proposition _ _))

-- The application _≃ᴱ_.right-inverse-of ∥∥ᴱ×≃ᴱ x computes in a
-- certain way.

_ : _≃ᴱ_.right-inverse-of ∥∥ᴱ×≃ᴱ x ≡ refl _
_ = refl _

-- ∥_∥ᴱ commutes with _×_.

∥∥ᴱ×∥∥ᴱ↔∥×∥ᴱ : (∥ A ∥ᴱ × ∥ B ∥ᴱ) ↔ ∥ A × B ∥ᴱ
∥∥ᴱ×∥∥ᴱ↔∥×∥ᴱ = record
  { surjection = record
    { logical-equivalence = record
      { from = λ p → ∥∥ᴱ-map proj₁ p , ∥∥ᴱ-map proj₂ p
      ; to   = uncurry $ rec λ where
                 .∣∣ʳ x → rec λ where
                   .∣∣ʳ y                      → ∣ x , y ∣
                   .truncation-is-propositionʳ →
                     truncation-is-proposition
                 .truncation-is-propositionʳ →
                   Π-closure ext 1 λ _ →
                   truncation-is-proposition
      }
    ; right-inverse-of = elim λ where
        .∣∣ʳ _                        → refl _
        .truncation-is-propositionʳ _ →
          mono₁ 1 truncation-is-proposition
    }
  ; left-inverse-of = uncurry $ elim λ where
      .∣∣ʳ _ → elim λ where
        .∣∣ʳ _ → refl _
        .truncation-is-propositionʳ _ →
          mono₁ 1 $
          ×-closure 1 truncation-is-proposition
                      truncation-is-proposition
      .truncation-is-propositionʳ _ →
        Π-closure ext 1 λ _ →
        mono₁ 1 $
        ×-closure 1 truncation-is-proposition
                    truncation-is-proposition
  }

------------------------------------------------------------------------
-- Some results related to h-levels

-- Variants of proj₁-closure.

private

  H-level-×₁-lemma :
    (A → ∥ B ∥ᴱ) →
    ∀ n → H-level (suc n) (A × B) → H-level (suc n) A
  H-level-×₁-lemma inhabited n h =
    [inhabited⇒+]⇒+ n λ a →
    flip rec (inhabited a) λ where
      .∣∣ʳ b →
        proj₁-closure (λ _ → b) (suc n) h
      .truncation-is-propositionʳ →
        H-level-propositional ext (suc n)

H-level-×₁ :
  (A → ∥ B ∥ᴱ) →
  ∀ n → H-level n (A × B) → H-level n A
H-level-×₁ inhabited zero h =
  propositional⇒inhabited⇒contractible
    (H-level-×₁-lemma inhabited 0 (mono₁ 0 h))
    (proj₁ (proj₁ h))
H-level-×₁ inhabited (suc n) =
  H-level-×₁-lemma inhabited n

H-level-×₂ :
  (B → ∥ A ∥ᴱ) →
  ∀ n → H-level n (A × B) → H-level n B
H-level-×₂ {B = B} {A = A} inhabited n =
  H-level n (A × B)  ↝⟨ H-level.respects-surjection (from-bijection ×-comm) n ⟩
  H-level n (B × A)  ↝⟨ H-level-×₁ inhabited n ⟩□
  H-level n B        □

------------------------------------------------------------------------
-- Flattening

-- A generalised flattening lemma.

flatten′ :
  (F : (Type ℓ → Type ℓ) → Type f)
  (map : ∀ {G H} → (∀ {A} → G A → H A) → F G → F H)
  (f : F ∥_∥ᴱ → ∥ F id ∥ᴱ) →
  (∀ x → f (map ∣_∣ x) ≡ ∣ x ∣) →
  (∀ x → ∥∥ᴱ-map (map ∣_∣) (f x) ≡ ∣ x ∣) →
  ∥ F ∥_∥ᴱ ∥ᴱ ↔ ∥ F id ∥ᴱ
flatten′ _ map f f-map map-f = record
  { surjection = record
    { logical-equivalence = record
      { to   = rec λ where
                 .∣∣ʳ                        → f
                 .truncation-is-propositionʳ → truncation-is-proposition
      ; from = ∥∥ᴱ-map (map ∣_∣)
      }
    ; right-inverse-of = elim λ where
        .∣∣ʳ                          → f-map
        .truncation-is-propositionʳ _ →
          mono₁ 1 truncation-is-proposition
    }
  ; left-inverse-of = elim λ where
      .∣∣ʳ                          → map-f
      .truncation-is-propositionʳ _ →
        mono₁ 1 truncation-is-proposition
  }

-- Nested truncations can be flattened.

flatten : ∥ ∥ A ∥ᴱ ∥ᴱ ↔ ∥ A ∥ᴱ
flatten {A = A} = flatten′
  (λ F → F A)
  (λ f → f)
  id
  (λ _ → refl _)
  (elim λ where
     .∣∣ʳ _                        → refl _
     .truncation-is-propositionʳ _ → mono₁ 1 truncation-is-proposition)

private

  -- Another flattening lemma, given as an example of how flatten′ can
  -- be used.

  ∥∃∥∥ᴱ∥ᴱ↔∥∃∥ᴱ : ∥ ∃ (∥_∥ᴱ ∘ P) ∥ᴱ ↔ ∥ ∃ P ∥ᴱ
  ∥∃∥∥ᴱ∥ᴱ↔∥∃∥ᴱ {P = P} = flatten′
    (λ F → ∃ (F ∘ P))
    (λ f → Σ-map id f)
    (uncurry λ x → ∥∥ᴱ-map (x ,_))
    (λ _ → refl _)
    (uncurry λ _ → elim λ where
       .∣∣ʳ _ → refl _
       .truncation-is-propositionʳ _ →
         mono₁ 1 truncation-is-proposition)

-- A variant of flatten′ with _≃ᴱ_ instead of _↔_.

flatten-≃ᴱ :
  (F : (Type ℓ → Type ℓ) → Type f)
  (map : ∀ {G H} → (∀ {A} → G A → H A) → F G → F H)
  (f : F ∥_∥ᴱ → ∥ F id ∥ᴱ) →
  @0 (∀ x → f (map ∣_∣ x) ≡ ∣ x ∣) →
  @0 (∀ x → ∥∥ᴱ-map (map ∣_∣) (f x) ≡ ∣ x ∣) →
  ∥ F ∥_∥ᴱ ∥ᴱ ≃ᴱ ∥ F id ∥ᴱ
flatten-≃ᴱ _ map f f-map map-f = EEq.↔→≃ᴱ
  (rec λ where
     .∣∣ʳ                        → f
     .truncation-is-propositionʳ → truncation-is-proposition)
  (∥∥ᴱ-map (map ∣_∣))
  (elim λ @0 where
     .∣∣ʳ                          → f-map
     .truncation-is-propositionʳ _ →
       mono₁ 1 truncation-is-proposition)
  (elim λ @0 where
     .∣∣ʳ                          → map-f
     .truncation-is-propositionʳ _ →
       mono₁ 1 truncation-is-proposition)

------------------------------------------------------------------------
-- The propositional truncation operator is a monad

-- A universe-polymorphic variant of bind.

infixl 5 _>>=′_

_>>=′_ : ∥ A ∥ᴱ → (A → ∥ B ∥ᴱ) → ∥ B ∥ᴱ
x >>=′ f = _↔_.to flatten (∥∥ᴱ-map f x)

-- The universe-polymorphic variant of bind is associative.

>>=′-associative :
  (x : ∥ A ∥ᴱ) →
  x >>=′ (λ x → f x >>=′ g) ≡ x >>=′ f >>=′ g
>>=′-associative = elim λ where
  .∣∣ʳ _                        → refl _
  .truncation-is-propositionʳ _ → ⇒≡ 1 truncation-is-proposition

instance

  -- The propositional truncation operator is a monad.

  raw-monad : Raw-monad (∥_∥ᴱ {a = a})
  Raw-monad.return raw-monad = ∣_∣
  Raw-monad._>>=_  raw-monad = _>>=′_

  monad : Monad (∥_∥ᴱ {a = a})
  Monad.raw-monad monad           = raw-monad
  Monad.left-identity monad _ _   = refl _
  Monad.associativity monad x _ _ = >>=′-associative x
  Monad.right-identity monad      = elim λ where
    .∣∣ʳ                        _ → refl _
    .truncation-is-propositionʳ _ → ⇒≡ 1 truncation-is-proposition

------------------------------------------------------------------------
-- Surjectivity

-- A variant of surjectivity with "erased proofs".

Surjectiveᴱ :
  {A : Type a} {B : Type b} →
  (A → B) → Type (a ⊔ b)
Surjectiveᴱ f = ∀ y → ∥ f ⁻¹ᴱ y ∥ᴱ

-- The property Surjectiveᴱ f is a proposition (in erased contexts).

@0 Surjectiveᴱ-propositional : Is-proposition (Surjectiveᴱ f)
Surjectiveᴱ-propositional =
  Π-closure ext 1 λ _ →
  truncation-is-proposition

-- The function ∣_∣ is surjective (with erased proofs).

∣∣-surjective : Surjectiveᴱ (∣_∣ {A = A})
∣∣-surjective = elim λ where
  .∣∣ʳ x                        → ∣ x , [ refl _ ] ∣
  .truncation-is-propositionʳ _ → truncation-is-proposition

-- Split surjective functions are surjective (with erased proofs).

Split-surjective→Surjectiveᴱ :
  Split-surjective f → Surjectiveᴱ f
Split-surjective→Surjectiveᴱ s = λ y → ∣ ECP.⁻¹→⁻¹ᴱ (s y) ∣

-- Being both surjective (with erased proofs) and an embedding
-- (completely erased) is equivalent to being an equivalence (with
-- erased proofs).
--
-- This result, without erasure, is Corollary 4.6.4 from the first
-- edition of the HoTT book.

Surjectiveᴱ×Erased-Is-embedding≃ᴱIs-equivalenceᴱ :
  (Surjectiveᴱ f × Erased (Is-embedding f)) ≃ᴱ Is-equivalenceᴱ f
Surjectiveᴱ×Erased-Is-embedding≃ᴱIs-equivalenceᴱ {f = f} = EEq.⇔→≃ᴱ
  (×-closure 1
     Surjectiveᴱ-propositional
     (Er.H-level-Erased 1
        (Emb.Is-embedding-propositional ext)))
  (EEq.Is-equivalenceᴱ-propositional ext f)
  (λ (is-surj , is-emb) →
     _⇔_.from EEq.Is-equivalenceᴱ⇔Is-equivalenceᴱ-CP $ λ y →
                              $⟨ is-surj y ⟩
     ∥ f ⁻¹ᴱ y ∥ᴱ             ↝⟨ (rec λ where
                                    .∣∣ʳ p → ECP.inhabited→Is-proposition→Contractibleᴱ p
                                               (H-level-cong _ 1
                                                  ECP.⁻¹≃⁻¹ᴱ
                                                  (Emb.embedding→⁻¹-propositional (Er.erased is-emb) _))
                                    .truncation-is-propositionʳ →
                                      ECP.Contractibleᴱ-propositional ext) ⟩□
     Contractibleᴱ (f ⁻¹ᴱ y)  □)
  (λ is-eq@(inv , [ r-inv , _ ]) →
       (λ y →           $⟨ inv y , [ r-inv y ] ⟩
          f ⁻¹ᴱ y       ↝⟨ ∣_∣ ⟩
          ∥ f ⁻¹ᴱ y ∥ᴱ  □)

     ,                            ($⟨ is-eq ⟩
       Is-equivalenceᴱ f           ↝⟨ Er.[_]→ ⟩
       Erased (Is-equivalenceᴱ f)  ↝⟨ Er.map EEq.Is-equivalenceᴱ→Is-equivalence ⟩
       Erased (Is-equivalence f)   ↝⟨ Er.map Emb.Is-equivalence→Is-embedding ⟩□
       Erased (Is-embedding f)     □))

------------------------------------------------------------------------
-- Another lemma

-- The function λ R x y → ∥ R x y ∥ᴱ preserves Is-equivalence-relation.

∥∥ᴱ-preserves-Is-equivalence-relation :
  Is-equivalence-relation R →
  Is-equivalence-relation (λ x y → ∥ R x y ∥ᴱ)
∥∥ᴱ-preserves-Is-equivalence-relation R-equiv = record
  { reflexive  = ∣ reflexive ∣
  ; symmetric  = symmetric ⟨$⟩_
  ; transitive = λ p q → transitive ⟨$⟩ p ⊛ q
  }
  where
  open Is-equivalence-relation R-equiv

------------------------------------------------------------------------
-- Definitions related to truncated binary sums

-- Truncated binary sums.

infixr 1 _∥⊎∥ᴱ_

_∥⊎∥ᴱ_ : Type a → Type b → Type (a ⊔ b)
A ∥⊎∥ᴱ B = ∥ A ⊎ B ∥ᴱ

-- Introduction rules.

∣inj₁∣ : A → A ∥⊎∥ᴱ B
∣inj₁∣ = ∣_∣ ∘ inj₁

∣inj₂∣ : B → A ∥⊎∥ᴱ B
∣inj₂∣ = ∣_∣ ∘ inj₂

-- In erased contexts _∥⊎∥ᴱ_ is pointwise propositional.

@0 ∥⊎∥ᴱ-propositional : Is-proposition (A ∥⊎∥ᴱ B)
∥⊎∥ᴱ-propositional = truncation-is-proposition

-- The _∥⊎∥ᴱ_ operator preserves "symmetric" functions.

infixr 1 _∥⊎∥ᴱ-cong_

_∥⊎∥ᴱ-cong_ :
  A₁ ↝[ ⌊ k ⌋-sym ] A₂ → B₁ ↝[ ⌊ k ⌋-sym ] B₂ →
  (A₁ ∥⊎∥ᴱ B₁) ↝[ ⌊ k ⌋-sym ] (A₂ ∥⊎∥ᴱ B₂)
A₁↝A₂ ∥⊎∥ᴱ-cong B₁↝B₂ = ∥∥ᴱ-cong (A₁↝A₂ ⊎-cong B₁↝B₂)

-- _∥⊎∥ᴱ_ is commutative.

∥⊎∥ᴱ-comm : A ∥⊎∥ᴱ B ↔ B ∥⊎∥ᴱ A
∥⊎∥ᴱ-comm = ∥∥ᴱ-cong ⊎-comm

-- If one truncates the types to the left or right of _∥⊎∥ᴱ_, then one
-- ends up with an isomorphic type.

truncate-left-∥⊎∥ᴱ : A ∥⊎∥ᴱ B ↔ ∥ A ∥ᴱ ∥⊎∥ᴱ B
truncate-left-∥⊎∥ᴱ =
  inverse $
  flatten′
    (λ F → F _ ⊎ _)
    (λ f → ⊎-map f id)
    P.[ ∥∥ᴱ-map inj₁ , ∣inj₂∣ ]
    P.[ (λ _ → refl _) , (λ _ → refl _) ]
    P.[ (elim λ where
           .∣∣ʳ _ → refl _
           .truncation-is-propositionʳ _ →
             mono₁ 1 ∥⊎∥ᴱ-propositional)
      , (λ _ → refl _)
      ]

truncate-right-∥⊎∥ᴱ : A ∥⊎∥ᴱ B ↔ A ∥⊎∥ᴱ ∥ B ∥ᴱ
truncate-right-∥⊎∥ᴱ {A = A} {B = B} =
  A ∥⊎∥ᴱ B       ↝⟨ ∥⊎∥ᴱ-comm ⟩
  B ∥⊎∥ᴱ A       ↝⟨ truncate-left-∥⊎∥ᴱ ⟩
  ∥ B ∥ᴱ ∥⊎∥ᴱ A  ↝⟨ ∥⊎∥ᴱ-comm ⟩□
  A ∥⊎∥ᴱ ∥ B ∥ᴱ  □

-- _∥⊎∥ᴱ_ is associative.

∥⊎∥ᴱ-assoc : A ∥⊎∥ᴱ (B ∥⊎∥ᴱ C) ↔ (A ∥⊎∥ᴱ B) ∥⊎∥ᴱ C
∥⊎∥ᴱ-assoc {A = A} {B = B} {C = C} =
  ∥ A ⊎ ∥ B ⊎ C ∥ᴱ ∥ᴱ  ↝⟨ inverse truncate-right-∥⊎∥ᴱ ⟩
  ∥ A ⊎ B ⊎ C ∥ᴱ       ↝⟨ ∥∥ᴱ-cong ⊎-assoc ⟩
  ∥ (A ⊎ B) ⊎ C ∥ᴱ     ↝⟨ truncate-left-∥⊎∥ᴱ ⟩□
  ∥ ∥ A ⊎ B ∥ᴱ ⊎ C ∥ᴱ  □

-- ⊥ is a left and right identity of _∥⊎∥ᴱ_ if the other argument is a
-- proposition.

∥⊎∥ᴱ-left-identity : @0 Is-proposition A → ⊥ {ℓ = ℓ} ∥⊎∥ᴱ A ↔ A
∥⊎∥ᴱ-left-identity {A = A} A-prop =
  ∥ ⊥ ⊎ A ∥ᴱ  ↝⟨ ∥∥ᴱ-cong ⊎-left-identity ⟩
  ∥ A ∥ᴱ      ↝⟨ ∥∥ᴱ↔ A-prop ⟩□
  A          □

∥⊎∥ᴱ-right-identity : @0 Is-proposition A → A ∥⊎∥ᴱ ⊥ {ℓ = ℓ} ↔ A
∥⊎∥ᴱ-right-identity {A = A} A-prop =
  A ∥⊎∥ᴱ ⊥  ↔⟨ ∥⊎∥ᴱ-comm ⟩
  ⊥ ∥⊎∥ᴱ A  ↔⟨ ∥⊎∥ᴱ-left-identity A-prop ⟩□
  A         □

-- _∥⊎∥ᴱ_ is idempotent for propositions (up to equivalences with
-- erased proofs).

∥⊎∥ᴱ-idempotent : @0 Is-proposition A → (A ∥⊎∥ᴱ A) ≃ᴱ A
∥⊎∥ᴱ-idempotent {A = A} A-prop =
  ∥ A ⊎ A ∥ᴱ  ↝⟨ idempotent ⟩
  ∥ A ∥ᴱ      ↔⟨ ∥∥ᴱ↔ A-prop ⟩□
  A           □

-- Sometimes a truncated binary sum is equivalent (with erased proofs)
-- to one of its summands.

drop-left-∥⊎∥ᴱ :
  @0 Is-proposition B → (A → B) → (A ∥⊎∥ᴱ B) ≃ᴱ B
drop-left-∥⊎∥ᴱ B-prop A→B = EEq.⇔→≃ᴱ
  ∥⊎∥ᴱ-propositional
  B-prop
  (rec λ where
     .∣∣ʳ → P.[ A→B , id ]
     .truncation-is-propositionʳ → B-prop)
  ∣inj₂∣

drop-right-∥⊎∥ᴱ :
  @0 Is-proposition A → (B → A) → (A ∥⊎∥ᴱ B) ≃ᴱ A
drop-right-∥⊎∥ᴱ {A = A} {B = B} A-prop B→A =
  A ∥⊎∥ᴱ B  ↔⟨ ∥⊎∥ᴱ-comm ⟩
  B ∥⊎∥ᴱ A  ↝⟨ drop-left-∥⊎∥ᴱ A-prop B→A ⟩□
  A        □

-- Sometimes a truncated binary sum is isomorphic to one of its
-- summands.

drop-⊥-right-∥⊎∥ᴱ :
  @0 Is-proposition A → ¬ B → A ∥⊎∥ᴱ B ↔ A
drop-⊥-right-∥⊎∥ᴱ A-prop ¬B = record
  { surjection = record
    { logical-equivalence = record
      { to = rec λ where
          .∣∣ʳ → P.[ id , ⊥-elim ∘ ¬B ]
          .truncation-is-propositionʳ → A-prop
      ; from = ∣inj₁∣
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = elim λ where
      .∣∣ʳ → P.[ (λ _ → refl _) , ⊥-elim ∘ ¬B ]
      .truncation-is-propositionʳ _ →
        mono₁ 1 ∥⊎∥ᴱ-propositional
  }

drop-⊥-left-∥⊎∥ᴱ :
  @0 Is-proposition B → ¬ A → A ∥⊎∥ᴱ B ↔ B
drop-⊥-left-∥⊎∥ᴱ B-prop ¬A = record
  { surjection = record
    { logical-equivalence = record
      { to = rec λ where
          .∣∣ʳ → P.[ ⊥-elim ∘ ¬A , id ]
          .truncation-is-propositionʳ → B-prop
      ; from = ∣inj₂∣
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = elim λ where
      .∣∣ʳ → P.[ ⊥-elim ∘ ¬A , (λ _ → refl _) ]
      .truncation-is-propositionʳ _ →
        mono₁ 1 ∥⊎∥ᴱ-propositional
  }

-- A type of functions from a truncated binary sum to a family of
-- propositions can be expressed as a binary product of function
-- types.

Π∥⊎∥ᴱ↔Π×Π :
  @0 (∀ x → Is-proposition (P x)) →
  ((x : A ∥⊎∥ᴱ B) → P x)
    ↔
  ((x : A) → P (∣inj₁∣ x)) × ((y : B) → P (∣inj₂∣ y))
Π∥⊎∥ᴱ↔Π×Π {A = A} {B = B} {P = P} P-prop =
  ((x : A ∥⊎∥ᴱ B) → P x)                               ↔⟨ universal-property-Π P-prop ⟩
  ((x : A ⊎ B) → P ∣ x ∣)                              ↝⟨ Π⊎↔Π×Π ext ⟩□
  ((x : A) → P (∣inj₁∣ x)) × ((y : B) → P (∣inj₂∣ y))  □

-- Two distributivity laws for Σ and _∥⊎∥ᴱ_.

Σ-∥⊎∥ᴱ-distrib-left :
  @0 Is-proposition A →
  Σ A (λ x → P x ∥⊎∥ᴱ Q x) ↔ Σ A P ∥⊎∥ᴱ Σ A Q
Σ-∥⊎∥ᴱ-distrib-left {P = P} {Q = Q} A-prop =
  (∃ λ x → ∥ P x ⊎ Q x ∥ᴱ)       ↝⟨ inverse $ ∥∥ᴱ↔ (Σ-closure 1 A-prop λ _ → ∥⊎∥ᴱ-propositional) ⟩
  ∥ (∃ λ x → ∥ P x ⊎ Q x ∥ᴱ) ∥ᴱ  ↝⟨ flatten′
                                      (λ F → (∃ λ x → F (P x ⊎ Q x)))
                                      (λ f → Σ-map id f)
                                      (uncurry λ x → ∥∥ᴱ-map (x ,_))
                                      (λ _ → refl _)
                                      (uncurry λ _ → elim λ where
                                         .∣∣ʳ _ → refl _
                                         .truncation-is-propositionʳ _ →
                                           mono₁ 1 truncation-is-proposition) ⟩
  ∥ (∃ λ x → P x ⊎ Q x) ∥ᴱ       ↝⟨ ∥∥ᴱ-cong ∃-⊎-distrib-left ⟩□
  ∥ ∃ P ⊎ ∃ Q ∥ᴱ                 □

Σ-∥⊎∥ᴱ-distrib-right :
  @0 (∀ x → Is-proposition (P x)) →
  Σ (A ∥⊎∥ᴱ B) P ↔ Σ A (P ∘ ∣inj₁∣) ∥⊎∥ᴱ Σ B (P ∘ ∣inj₂∣)
Σ-∥⊎∥ᴱ-distrib-right {A = A} {B = B} {P = P} P-prop = record
  { surjection = record
    { logical-equivalence = record
      { to = uncurry $ elim λ where
          .∣∣ʳ → curry (∣_∣ ∘ _↔_.to ∃-⊎-distrib-right)
          .truncation-is-propositionʳ _ →
            Π-closure ext 1 λ _ →
            ∥⊎∥ᴱ-propositional
      ; from = rec λ where
          .∣∣ʳ → Σ-map ∣_∣ id ∘ _↔_.from ∃-⊎-distrib-right
          .truncation-is-propositionʳ → prop
      }
    ; right-inverse-of = elim λ where
      .∣∣ʳ → P.[ (λ _ → refl _) , (λ _ → refl _) ]
      .truncation-is-propositionʳ _ →
        mono₁ 1 ∥⊎∥ᴱ-propositional
    }
  ; left-inverse-of = uncurry $ elim λ where
      .∣∣ʳ → P.[ (λ _ _ → refl _) , (λ _ _ → refl _) ]
      .truncation-is-propositionʳ _ →
        Π-closure ext 1 λ _ →
        mono₁ 1 prop
  }
  where
  @0 prop : _
  prop = Σ-closure 1 ∥⊎∥ᴱ-propositional P-prop

-- A variant of one of De Morgan's laws.

¬∥⊎∥ᴱ¬↔¬× :
  Dec (¬ A) → Dec (¬ B) →
  (¬ A ∥⊎∥ᴱ ¬ B) ≃ᴱ (¬ (A × B))
¬∥⊎∥ᴱ¬↔¬× {A = A} {B = B} dec-¬A dec-¬B = EEq.⇔→≃ᴱ
  ∥⊎∥ᴱ-propositional
  (¬-propositional ext)
  (rec λ where
     .∣∣ʳ → ¬⊎¬→×¬
     .truncation-is-propositionʳ → ¬-propositional ext)
  (∣_∣ ∘ _↠_.from (¬⊎¬↠¬× ext dec-¬A dec-¬B))

------------------------------------------------------------------------
-- Code related to Erased-singleton

-- A corollary of erased-singleton-with-erased-center-propositional.

↠→↠Erased-singleton :
  {@0 y : B}
  (A↠B : A ↠ B) →
  ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥ᴱ ↠ Erased-singleton y
↠→↠Erased-singleton {A = A} {y = y} A↠B =
  ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥ᴱ  ↝⟨ ∥∥ᴱ-cong-↠ (S.Σ-cong A↠B λ _ → F.id) ⟩
  ∥ Erased-singleton y ∥ᴱ                         ↔⟨ ∥∥ᴱ↔
                                                       (Er.erased-singleton-with-erased-center-propositional $
                                                        Er.Very-stable→Very-stableᴱ 1 $
                                                        Er.Very-stable→Very-stable-≡ 0 $
                                                        erased Er.Erased-Very-stable) ⟩□
  Erased-singleton y                              □

-- Another corollary of
-- erased-singleton-with-erased-center-propositional.

↠→≃ᴱErased-singleton :
  {@0 y : B}
  (A↠B : A ↠ B) →
  ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥ᴱ ≃ᴱ Erased-singleton y
↠→≃ᴱErased-singleton {A = A} {y = y} A↠B =
  ∥ (∃ λ (x : A) → Erased (_↠_.to A↠B x ≡ y)) ∥ᴱ  ↝⟨ ∥∥ᴱ-cong-⇔ (S.Σ-cong-⇔ A↠B λ _ → F.id) ⟩
  ∥ Erased-singleton y ∥ᴱ                         ↔⟨ ∥∥ᴱ↔
                                                       (Er.erased-singleton-with-erased-center-propositional $
                                                        Er.Very-stable→Very-stableᴱ 1 $
                                                        Er.Very-stable→Very-stable-≡ 0 $
                                                        erased Er.Erased-Very-stable) ⟩□
  Erased-singleton y                              □

-- A corollary of Σ-Erased-Erased-singleton↔ and ↠→≃ᴱErased-singleton.

Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ :
  (A↠B : A ↠ B) →
  (∃ λ (x : Erased B) →
     ∥ (∃ λ (y : A) → Erased (_↠_.to A↠B y ≡ erased x)) ∥ᴱ) ≃ᴱ
  B
Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ {A = A} {B = B} A↠B =
  (∃ λ (x : Erased B) →
     ∥ (∃ λ (y : A) → Erased (_↠_.to A↠B y ≡ erased x)) ∥ᴱ)  ↝⟨ (∃-cong λ _ → ↠→≃ᴱErased-singleton A↠B) ⟩

  (∃ λ (x : Erased B) → Erased-singleton (erased x))         ↔⟨ Er.Σ-Erased-Erased-singleton↔ ⟩□

  B                                                          □

-- In an erased context the left-to-right direction of
-- Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ returns the erased first component.

@0 to-Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ≡ :
  ∀ (A↠B : A ↠ B) x →
  _≃ᴱ_.to (Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ A↠B) x ≡ erased (proj₁ x)
to-Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ≡ A↠B ([ x ] , y) =
  _≃ᴱ_.to (Σ-Erased-∥-Σ-Erased-≡-∥≃ᴱ A↠B) ([ x ] , y)  ≡⟨⟩
  proj₁ (_≃ᴱ_.to (↠→≃ᴱErased-singleton A↠B) y)         ≡⟨ erased (proj₂ (_≃ᴱ_.to (↠→≃ᴱErased-singleton A↠B) y)) ⟩∎
  x                                                    ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

open import Categories.Category
open import Categories.Functor hiding (id)

module Categories.Diagram.Colimit.Properties
  {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where

private
    module F = Functor F
    module C = Category C
    open C

open import Categories.Diagram.Limit F.op
open import Categories.Diagram.Colimit F
open import Categories.Category.Construction.Cocones F
open import Categories.Diagram.Duality C

module _ (X : Obj) (coapex₁ : Coapex X) (coapex₂ : Coapex X) (L : Colimit) where
  private
    module coapex₁ = Coapex coapex₁
    module coapex₂ = Coapex coapex₂
    module L = Colimit L

    K₁ : Cocone
    K₁ = record { coapex = coapex₁ }
    module K₁ = Cocone K₁

    K₂ : Cocone
    K₂ = record { coapex = coapex₂ }
    module K₂ = Cocone K₂

  coψ-≈⇒rep-≈ : (∀ A → coapex₁.ψ A ≈ coapex₂.ψ A) → L.rep K₁ ≈ L.rep K₂
  coψ-≈⇒rep-≈ = ψ-≈⇒rep-≈ X (Coapex⇒coApex X coapex₁) (Coapex⇒coApex X coapex₂) (Colimit⇒coLimit L)

ext: agda

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

open import Cubical.Data.HomotopyGroup.Base public

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:
{-# OPTIONS --without-K #-}

open import lib.Basics
open import lib.types.Nat
open import lib.types.Group
open import lib.types.TLevel

module lib.types.Int where

data ℤ : Type₀ where
  O : ℤ
  pos : (n : ℕ) → ℤ
  neg : (n : ℕ) → ℤ

Int = ℤ

succ : ℤ → ℤ
succ O = pos O
succ (pos n) = pos (S n)
succ (neg O) = O
succ (neg (S n)) = neg n

pred : ℤ → ℤ
pred O = neg O
pred (pos O) = O
pred (pos (S n)) = pos n
pred (neg n) = neg (S n)

abstract
  succ-pred : (n : ℤ) → succ (pred n) == n
  succ-pred O = idp
  succ-pred (pos O) = idp
  succ-pred (pos (S n)) = idp
  succ-pred (neg n) = idp

  pred-succ : (n : ℤ) → pred (succ n) == n
  pred-succ O = idp
  pred-succ (pos n) = idp
  pred-succ (neg O) = idp
  pred-succ (neg (S n)) = idp

succ-equiv : ℤ ≃ ℤ
succ-equiv = equiv succ pred succ-pred pred-succ

pred-injective : (z₁ z₂ : ℤ) → pred z₁ == pred z₂ → z₁ == z₂
pred-injective z₁ z₂ p = ! (succ-pred z₁) ∙ ap succ p ∙ succ-pred z₂

succ-injective : (z₁ z₂ : ℤ) → succ z₁ == succ z₂ → z₁ == z₂
succ-injective z₁ z₂ p = ! (pred-succ z₁) ∙ ap pred p ∙ pred-succ z₂

{- Converting between ℤ, ℕ, and ℕ₋₂ -}

ℤ-to-ℕ₋₂ : ℤ → ℕ₋₂
ℤ-to-ℕ₋₂ O = ⟨0⟩
ℤ-to-ℕ₋₂ (pos m) = S ⟨ m ⟩
ℤ-to-ℕ₋₂ (neg O) = ⟨-1⟩
ℤ-to-ℕ₋₂ (neg _) = ⟨-2⟩

ℕ-to-ℤ : ℕ → ℤ
ℕ-to-ℤ n = pred (pos n)

{- Proof that [ℤ] has decidable equality and hence is a set -}

private
  ℤ-get-pos : ℤ → ℕ
  ℤ-get-pos O = 0
  ℤ-get-pos (pos n) = n
  ℤ-get-pos (neg n) = 0

  ℤ-get-neg : ℤ → ℕ
  ℤ-get-neg O = 0
  ℤ-get-neg (pos n) = 0
  ℤ-get-neg (neg n) = n

  ℤ-neg≠O≠pos-type : ℤ → Type₀
  ℤ-neg≠O≠pos-type O = Unit
  ℤ-neg≠O≠pos-type (pos n) = Empty
  ℤ-neg≠O≠pos-type (neg n) = Empty

  ℤ-neg≠pos-type : ℤ → Type₀
  ℤ-neg≠pos-type O = Unit
  ℤ-neg≠pos-type (pos n) = Empty
  ℤ-neg≠pos-type (neg n) = Unit

abstract
  pos-injective : (n m : ℕ) (p : pos n == pos m) → n == m
  pos-injective n m p = ap ℤ-get-pos p

  neg-injective : (n m : ℕ) (p : neg n == neg m) → n == m
  neg-injective n m p = ap ℤ-get-neg p

  ℤ-O≠pos : (n : ℕ) → O ≠ pos n
  ℤ-O≠pos n p = transport ℤ-neg≠O≠pos-type p unit

  ℤ-pos≠O : (n : ℕ) → pos n ≠ O
  ℤ-pos≠O n p = transport ℤ-neg≠O≠pos-type (! p) unit

  ℤ-O≠neg : (n : ℕ) → O ≠ neg n
  ℤ-O≠neg n p = transport ℤ-neg≠O≠pos-type p unit

  ℤ-neg≠O : (n : ℕ) → neg n ≠ O
  ℤ-neg≠O n p = transport ℤ-neg≠O≠pos-type (! p) unit

  ℤ-neg≠pos : (n m : ℕ) → neg n ≠ pos m
  ℤ-neg≠pos n m p = transport ℤ-neg≠pos-type p unit

  ℤ-pos≠neg : (n m : ℕ) → pos n ≠ neg m
  ℤ-pos≠neg n m p = transport ℤ-neg≠pos-type (! p) unit

  ℤ-has-dec-eq : has-dec-eq ℤ
  ℤ-has-dec-eq O O = inl idp
  ℤ-has-dec-eq O (pos n) = inr (ℤ-O≠pos n)
  ℤ-has-dec-eq O (neg n) = inr (ℤ-O≠neg n)
  ℤ-has-dec-eq (pos n) O = inr (ℤ-pos≠O n)
  ℤ-has-dec-eq (pos n) (pos m) with ℕ-has-dec-eq n m
  ℤ-has-dec-eq (pos n) (pos m) | inl p = inl (ap pos p)
  ℤ-has-dec-eq (pos n) (pos m) | inr p⊥ = inr (λ p → p⊥ (pos-injective n m p))
  ℤ-has-dec-eq (pos n) (neg m) = inr (ℤ-pos≠neg n m)
  ℤ-has-dec-eq (neg n) O = inr (ℤ-neg≠O n)
  ℤ-has-dec-eq (neg n) (pos m) = inr (ℤ-neg≠pos n m)
  ℤ-has-dec-eq (neg n) (neg m) with ℕ-has-dec-eq n m
  ℤ-has-dec-eq (neg n) (neg m) | inl p = inl (ap neg p)
  ℤ-has-dec-eq (neg n) (neg m) | inr p⊥ = inr (λ p → p⊥ (neg-injective n m p))

  ℤ-is-set : is-set ℤ
  ℤ-is-set = dec-eq-is-set ℤ-has-dec-eq

ℤ-level = ℤ-is-set

{-
  ℤ is also a group!
-}

-- inv
ℤ~ : ℤ → ℤ
ℤ~ O = O
ℤ~ (pos n) = neg n
ℤ~ (neg n) = pos n

-- comp
_ℤ+_ : ℤ → ℤ → ℤ
O         ℤ+ z = z
pos O     ℤ+ z = succ z
pos (S n) ℤ+ z = succ (pos n ℤ+ z)
neg O     ℤ+ z = pred z
neg (S n) ℤ+ z = pred (neg n ℤ+ z)

-- unit-l
ℤ+-unit-l : ∀ z → O ℤ+ z == z
ℤ+-unit-l _ = idp

-- unit-r
private
  ℤ+-unit-r-pos : ∀ n → pos n ℤ+ O == pos n
  ℤ+-unit-r-pos O     = idp
  ℤ+-unit-r-pos (S n) = ap succ $ ℤ+-unit-r-pos n

  ℤ+-unit-r-neg : ∀ n → neg n ℤ+ O == neg n
  ℤ+-unit-r-neg O     = idp
  ℤ+-unit-r-neg (S n) = ap pred $ ℤ+-unit-r-neg n

ℤ+-unit-r : ∀ z → z ℤ+ O == z
ℤ+-unit-r O = idp
ℤ+-unit-r (pos n) = ℤ+-unit-r-pos n
ℤ+-unit-r (neg n) = ℤ+-unit-r-neg n

-- assoc
succ-ℤ+ : ∀ z₁ z₂ → succ z₁ ℤ+ z₂ == succ (z₁ ℤ+ z₂)
succ-ℤ+ O _ = idp
succ-ℤ+ (pos n) _ = idp
succ-ℤ+ (neg O) _ = ! $ succ-pred _
succ-ℤ+ (neg (S n)) _ = ! $ succ-pred _

pred-ℤ+ : ∀ z₁ z₂ → pred z₁ ℤ+ z₂ == pred (z₁ ℤ+ z₂)
pred-ℤ+ O _ = idp
pred-ℤ+ (neg n) _ = idp
pred-ℤ+ (pos O) _ = ! $ pred-succ _
pred-ℤ+ (pos (S n)) _ = ! $ pred-succ _

private
  ℤ+-assoc-pos : ∀ n₁ z₂ z₃ → (pos n₁ ℤ+ z₂) ℤ+ z₃ == pos n₁ ℤ+ (z₂ ℤ+ z₃)
  ℤ+-assoc-pos O      z₂ z₃ = succ-ℤ+ z₂ z₃
  ℤ+-assoc-pos (S n₁) z₂ z₃ =
    succ (pos n₁ ℤ+ z₂) ℤ+ z₃     =⟨ succ-ℤ+ (pos n₁ ℤ+ z₂) z₃ ⟩
    succ ((pos n₁ ℤ+ z₂) ℤ+ z₃)   =⟨ ap succ $ ℤ+-assoc-pos n₁ z₂ z₃ ⟩
    succ (pos n₁ ℤ+ (z₂ ℤ+ z₃))   ∎

  ℤ+-assoc-neg : ∀ n₁ z₂ z₃ → (neg n₁ ℤ+ z₂) ℤ+ z₃ == neg n₁ ℤ+ (z₂ ℤ+ z₃)
  ℤ+-assoc-neg O      z₂ z₃ = pred-ℤ+ z₂ z₃
  ℤ+-assoc-neg (S n₁) z₂ z₃ =
    pred (neg n₁ ℤ+ z₂) ℤ+ z₃     =⟨ pred-ℤ+ (neg n₁ ℤ+ z₂) z₃ ⟩
    pred ((neg n₁ ℤ+ z₂) ℤ+ z₃)   =⟨ ap pred $ ℤ+-assoc-neg n₁ z₂ z₃ ⟩
    pred (neg n₁ ℤ+ (z₂ ℤ+ z₃))   ∎

ℤ+-assoc : ∀ z₁ z₂ z₃ → (z₁ ℤ+ z₂) ℤ+ z₃ == z₁ ℤ+ (z₂ ℤ+ z₃)
ℤ+-assoc O        _ _ = idp
ℤ+-assoc (pos n₁) _ _ = ℤ+-assoc-pos n₁ _ _
ℤ+-assoc (neg n₁) _ _ = ℤ+-assoc-neg n₁ _ _

private
  pos-S-ℤ+-neg-S : ∀ n₁ n₂ → pos (S n₁) ℤ+ neg (S n₂) == pos n₁ ℤ+ neg n₂
  pos-S-ℤ+-neg-S O      n₂ = idp
  pos-S-ℤ+-neg-S (S n₁) n₂ = ap succ $ pos-S-ℤ+-neg-S n₁ n₂

  neg-S-ℤ+-pos-S : ∀ n₁ n₂ → neg (S n₁) ℤ+ pos (S n₂) == neg n₁ ℤ+ pos n₂
  neg-S-ℤ+-pos-S O      n₂ = idp
  neg-S-ℤ+-pos-S (S n₁) n₂ = ap pred $ neg-S-ℤ+-pos-S n₁ n₂

  ℤ~-inv-r-pos : ∀ n → pos n ℤ+ neg n == O
  ℤ~-inv-r-pos O     = idp
  ℤ~-inv-r-pos (S n) =
    pos (S n) ℤ+ neg (S n)  =⟨ pos-S-ℤ+-neg-S n n ⟩
    pos n ℤ+ neg n          =⟨ ℤ~-inv-r-pos n ⟩
    O                       ∎

  ℤ~-inv-r-neg : ∀ n → neg n ℤ+ pos n == O
  ℤ~-inv-r-neg O     = idp
  ℤ~-inv-r-neg (S n) =
    neg (S n) ℤ+ pos (S n)  =⟨ neg-S-ℤ+-pos-S n n ⟩
    neg n ℤ+ pos n          =⟨ ℤ~-inv-r-neg n ⟩
    O                       ∎

ℤ~-inv-r : ∀ z → z ℤ+ ℤ~ z == O
ℤ~-inv-r O       = idp
ℤ~-inv-r (pos n) = ℤ~-inv-r-pos n
ℤ~-inv-r (neg n) = ℤ~-inv-r-neg n

ℤ~-inv-l : ∀ z → ℤ~ z ℤ+ z == O
ℤ~-inv-l O       = idp
ℤ~-inv-l (pos n) = ℤ~-inv-r-neg n
ℤ~-inv-l (neg n) = ℤ~-inv-r-pos n

ℤ-group-structure : GroupStructure ℤ
ℤ-group-structure = record
  { ident = O
  ; inv = ℤ~
  ; comp = _ℤ+_
  ; unitl = ℤ+-unit-l
  ; unitr = ℤ+-unit-r
  ; assoc = ℤ+-assoc
  ; invr = ℤ~-inv-r
  ; invl = ℤ~-inv-l
  }

ℤ-group : Group₀
ℤ-group = group _ ℤ-is-set ℤ-group-structure

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text: module Numeral.Sign.Oper.Proofs where

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --cubical #-}
module _ where
open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub
open import Agda.Primitive renaming (_⊔_ to ℓ-max)
open import Agda.Builtin.Sigma

private
  internalFiber : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (y : B) → Set (ℓ-max ℓ ℓ')
  internalFiber {A = A} f y = Σ A \ x → y ≡ f x

infix 4 _≃_

postulate
  _≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ-max ℓ ℓ')
  equivFun : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A ≃ B → A → B
  equivProof : ∀ {la lt} (T : Set la) (A : Set lt) → (w : T ≃ A) → (a : A)
               → ∀ ψ → (Partial ψ (internalFiber (equivFun w) a)) → internalFiber (equivFun w) a

{-# BUILTIN EQUIV _≃_ #-}
{-# BUILTIN EQUIVFUN  equivFun #-}
{-# BUILTIN EQUIVPROOF equivProof #-}

-- This is a module so we can easily rename the primitives.
module GluePrims where
  primitive
    primGlue    : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
      → (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A))
      → Set ℓ'
    prim^glue   : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
      → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
      → PartialP φ T → A → primGlue A T e
    prim^unglue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
      → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
      → primGlue A T e → A

    -- Needed for transp in Glue.
    primFaceForall : (I → I) → I

open GluePrims public
  renaming ( prim^glue to glue
           ; prim^unglue to unglue)

-- We uncurry Glue to make it a bit more pleasant to use
Glue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
       → (Te : Partial φ (Σ (Set ℓ') \ T →  T ≃ A))
       → Set ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

module _ {ℓ ℓ'} (A : Set ℓ) {φ : I} (Te : Partial φ (Σ (Set ℓ') \ T →  T ≃ A))
         (ψ : I) (u : I → Partial ψ (Glue A Te)) (u0 : Sub (Glue A Te) ψ (u i0) ) where
  result : Glue A Te
  result = glue {φ = φ} (\ { (φ = i1) → primHComp {A = Te itIsOne .fst} u (primSubOut u0) })
                        (primHComp {A = A} (\ i → \ { (ψ = i1) → unglue {φ = φ} (u i itIsOne)
                                                    ; (φ = i1) → equivFun (Te itIsOne .snd)
                                                                          (primHComp (\ j → \ { (ψ = i1) → u (primIMin i j) itIsOne
                                                                                ; (i = i0) → primSubOut u0 })
                                                                                (primSubOut u0)) })
                                           (unglue {φ = φ} (primSubOut u0)))

  test : primHComp {A = Glue A Te} {ψ} u (primSubOut u0) ≡ result
  test i = primHComp {A = Glue A Te} {ψ} u (primSubOut u0)

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
open import Structures
open import Data.String using (String)
open import Data.Nat
open import Data.Nat.Show renaming (show to showNat)
open import Data.Vec as V using (Vec; []; _∷_)
open import Data.List as L using (List; []; _∷_)
open import Data.Sum
open import Data.Product
open import Relation.Nullary
open import Function using (_$_)

data Nesting : Set where
  hom : Nesting
  nes : Nesting

data SacTy : Set where
  unit  : SacTy
  int   : SacTy
  float : SacTy
  bool  : SacTy
  char  : SacTy
          -- Nested `n`-dimensional array is isomorphic to Listⁿ
          -- Homogeneous `n`-dimensional array is isomorphic to Vecⁿ
          -- The first argument does not tell whether the entire array needs
          -- to be implemented as nested or not (just an annotation), e.g:
          --    akd hom (akd nest nat 3)
          --    akd nes nat 2
          --    akd nes (akd nes nat 1)
          -- and so on.  In actual sac (with no support for nested arrays)
          -- it all collapses to three cases, but it is convenient to keep
          -- this distinction in the model.
  aud   : Nesting → SacTy → (sh : Prog) → SacTy
  akd   : Nesting → SacTy → (sh : Prog) → ℕ → SacTy
  aks   : Nesting → SacTy → (sh : Prog) → (n : ℕ) → Vec ℕ n → SacTy

data SacBase : SacTy → Set where
  unit  : SacBase unit
  int   : SacBase int
  float : SacBase float
  bool  : SacBase bool
  char  : SacBase char

data SacArray : SacTy → Set where
  aud : ∀ {n? τ es} → SacArray (aud n? τ es)
  akd : ∀ {n? τ es n} → SacArray (akd n? τ es n)
  aks : ∀ {n? τ es n s} → SacArray (aks n? τ es n s)

array-or-base : ∀ τ → SacBase τ ⊎ SacArray τ
array-or-base unit = inj₁ unit
array-or-base int = inj₁ int
array-or-base float = inj₁ float
array-or-base bool = inj₁ bool
array-or-base char = inj₁ char
array-or-base (aud x τ es) = inj₂ aud
array-or-base (akd x τ es x₁) = inj₂ akd
array-or-base (aks x τ es n x₁) = inj₂ aks

is-base : ∀ τ → Dec (SacBase τ)
is-base τ with array-or-base τ
... | inj₁ bt = yes bt
... | inj₂ aud = no λ ()
... | inj₂ akd = no λ ()
... | inj₂ aks = no λ ()

is-array : ∀ τ → Dec (SacArray τ)
is-array τ with array-or-base τ
... | inj₂ ar = yes ar
... | inj₁ unit = no λ ()
... | inj₁ int = no λ ()
... | inj₁ float = no λ ()
... | inj₁ bool = no λ ()
... | inj₁ char = no λ ()

-- Is it the case that the entire array can be implemented
-- as a flattened homogeneous (multi-dimensional) array.
nested? : SacTy → Nesting
nested? unit = hom
nested? int = hom
nested? float = hom
nested? bool = hom
nested? char = hom
nested? (aud hom τ _) = nested? τ
nested? (aud nes _ _) = nes
nested? (akd hom τ _ _) = nested? τ
nested? (akd nes _ _ _) = nes
nested? (aks hom τ _ _ _) = nested? τ
nested? (aks nes _ _ _ _) = nes

get-base : SacTy → Σ[ τ ∈ SacTy ] SacBase τ
get-base unit = unit , unit
get-base int = int , int
get-base float = float , float
get-base bool = bool , bool
get-base char = char , char
get-base (aud x τ es) = get-base τ
get-base (akd x τ es x₁) = get-base τ
get-base (aks x τ es n x₁) = get-base τ

bt-tostring : ∀ {τ} → SacBase τ → String
bt-tostring unit = "unit"
bt-tostring int = "int"
bt-tostring float = "float"
bt-tostring bool = "bool"
bt-tostring char = "char"

postfix-aud = "[*]"

postfix-akd : ℕ → String
postfix-akd n = "[" ++ ("," ++/ L.replicate n ".") ++ "]"

postfix-aks : (n : ℕ) → Vec ℕ n → String
postfix-aks n s = "[" ++ ("," ++/ L.map showNat (V.toList s)) ++ "]"

bt : SacTy → String
bt τ = bt-tostring (proj₂ $ get-base τ)

sacty-to-string : SacTy → String
sacty-to-string σ with array-or-base σ
sacty-to-string σ | inj₁ bt = bt-tostring bt
sacty-to-string σ | inj₂ (aud {nes} {τ}) = sacty-to-string τ ++ postfix-aud
sacty-to-string σ | inj₂ (aud {hom} {τ}) with nested? τ
... | hom = bt τ  ++ postfix-aud
... | nes = sacty-to-string τ ++ postfix-aud

sacty-to-string σ | inj₂ (akd {nes} {τ} {_} {n}) = sacty-to-string τ ++ postfix-akd n
sacty-to-string σ | inj₂ (akd {hom} {τ} {_} {n}) with nested? τ
... | nes = sacty-to-string τ ++ postfix-akd n
... | hom with array-or-base τ
... | inj₁ bt =
           bt-tostring bt ++ postfix-akd n
... | inj₂ aud =
           --(τ[*])[.,.,.]   → τ([.,.,.] ++ [*])   = τ[*]
           bt τ ++ postfix-aud
... | inj₂ (akd {n = m}) =
           --(τ[.,.])[.,.,.] → τ([.,.,.] ++ [.,.]) = τ[.,.,., .,.]
           bt τ ++ postfix-akd (n + m)
... | inj₂ (aks {n = m}) =
           --(τ[5,6])[.,.,.] → τ([.,.,.] ++ [5,6]) = τ[.,.,., .,.]
           bt τ ++ postfix-akd (n + m)

sacty-to-string σ | inj₂ (aks {nes} {τ} {_} {n} {s}) = sacty-to-string τ ++ postfix-aks n s
sacty-to-string σ | inj₂ (aks {hom} {τ} {_} {n} {s}) with nested? τ
... | nes = sacty-to-string τ ++ postfix-aks n s
... | hom with array-or-base τ
... | inj₁ bt =
           bt-tostring bt ++ postfix-aks n s
... | inj₂ aud =
           -- (τ[*])[5,6]  → τ([5,6] ++ [*]) = τ[*]
           bt τ ++ postfix-aud
... | inj₂ (akd {n = m}) =
           --(τ[.,.])[5,6] → τ([5,6] ++ [.,.]) = τ[.,.,.,.]
           bt τ ++ postfix-akd (n + m)
... | inj₂ (aks {s = s′}) =
           --(τ[7,8])[5,6] → τ([5,6] ++ [7,8]) = τ[5,6,7,8]
           bt τ ++ postfix-aks _ (s V.++ s′)

-- For some rare cases we can eliminate nesting
-- Note that this function does not recurse, as:
--    a: List (hom X)         ~  Vec (hom X) (length a)
-- but
--    a: List (List (hom X))  ≁  Vec (Vec X _) _
sacty-normalise : SacTy → SacTy
sacty-normalise τ with array-or-base τ
sacty-normalise τ | inj₁ bt  = τ
sacty-normalise τ | inj₂ aud = τ
sacty-normalise τ | inj₂ (akd {hom}) = τ
sacty-normalise τ | inj₂ (akd {nes} {σ} {es} {0}) = -- There is no need to nest a 0-dimensional array
                                               akd hom σ es 0
sacty-normalise τ | inj₂ (akd {nes} {σ} {es} {1}) = -- Nested array of depth 1 of homogeneous elements
                                               -- is the same as homogeneous of dimension 1.
                                               akd hom σ es 1
sacty-normalise τ | inj₂ (akd {nes} {_} {_}) = τ
sacty-normalise τ | inj₂ (aks {hom}) = τ
sacty-normalise τ | inj₂ (aks {nes} {σ} {es} {n} {s}) = aks hom σ es n s

sacty-shape : SacTy → Prog
sacty-shape τ with array-or-base τ
... | inj₁ bt = ok $ "[]"
... | inj₂ (aud {hom} {σ} {s}) = s ⊕ " ++ "  ⊕ sacty-shape σ
... | inj₂ (aud {nes} {σ} {s}) = error $ "sacty-shape: nested-array `" ++ sacty-to-string τ ++ "`"
... | inj₂ (akd {hom} {σ} {s}) = s ⊕ " ++ "  ⊕ sacty-shape σ
... | inj₂ (akd {nes} {σ} {s}) = error $ "sacty-shape: nested-array `" ++ sacty-to-string τ ++ "`"
... | inj₂ (aks {hom} {σ} {s}) = s ⊕ " ++ "  ⊕ sacty-shape σ
... | inj₂ (aks {nes} {σ} {s}) = error $ "sacty-shape: nested-array `" ++ sacty-to-string τ ++ "`"

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
------------------------------------------------------------------------
-- The delay monad, defined coinductively, with a sized type parameter
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

module Delay-monad.Sized where

open import Equality.Propositional
open import Prelude
open import Prelude.Size

open import Bijection equality-with-J using (_↔_)

-- The delay monad.

mutual

  data Delay {a} (A : Size → Type a) (i : Size) : Type a where
    now   : A i        → Delay A i
    later : Delay′ A i → Delay A i

  record Delay′ {a} (A : Size → Type a) (i : Size) : Type a where
    coinductive
    field
      force : {j : Size< i} → Delay A j

open Delay′ public

module _ {a} {A : Size → Type a} where

  mutual

    -- A non-terminating computation.

    never : ∀ {i} → Delay A i
    never = later never′

    never′ : ∀ {i} → Delay′ A i
    force never′ = never

  -- Removes a later constructor, if possible.

  drop-later : Delay A ∞ → Delay A ∞
  drop-later (now   x) = now x
  drop-later (later x) = force x

  -- An unfolding lemma for Delay.

  Delay↔ : ∀ {i} → Delay A i ↔ A i ⊎ Delay′ A i
  Delay↔ = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ { (now x) → inj₁ x; (later x) → inj₂ x }
        ; from = [ now , later ]
        }
      ; right-inverse-of = [ (λ _ → refl) , (λ _ → refl) ]
      }
    ; left-inverse-of = λ { (now _) → refl; (later _) → refl }
    }

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
{-# OPTIONS -v term.with.inline:20 -v term.with.call:30 #-}

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero + m = m
suc n + m = suc (n + m)

data [_] : Nat → Set where
  ⟨_⟩ : ∀ n → [ n ]

f : Nat → Nat
g : Nat → Nat
h : ∀ n → [ f n ]

f zero = zero
f (suc n) with f n
f (suc n) | zero  = zero
f (suc n) | suc m = f n + m

-- f's with-function should not get inlined into the clauses of g!
g zero = zero
g (suc n) = _   -- f (suc n) | f n

h zero = ⟨ zero ⟩
h (suc n) = ⟨ g (suc n) ⟩

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --without-K #-}

open import HoTT
open import cohomology.SuspAdjointLoopIso
open import cohomology.WithCoefficients
open import cohomology.Theory
open import cohomology.Exactness
open import cohomology.Choice

module cohomology.SpectrumModel
  {i} (E : ℤ → Ptd i) (spectrum : (n : ℤ) → ⊙Ω (E (succ n)) == E n) where

module SpectrumModel where

  {- Definition of cohomology group C -}
  module _ (n : ℤ) (X : Ptd i) where
    C : Group i
    C = →Ω-Group X (E (succ n))

    {- convenient abbreviations -}
    CEl = Group.El C
    ⊙CEl = Group.⊙El C
    Cid = Group.ident C

    {- before truncation -}
    ⊙uCEl : Ptd i
    ⊙uCEl = X ⊙→ ⊙Ω (E (succ n))

    uCEl = fst ⊙uCEl
    uCid = snd ⊙uCEl

  {- Cⁿ(X) is an abelian group -}
  C-abelian : (n : ℤ) (X : Ptd i) → is-abelian (C n X)
  C-abelian n X =
    transport (is-abelian ∘ →Ω-Group X) (spectrum (succ n)) C-abelian-lemma
    where
    pt-lemma : ∀ {i} {X : Ptd i} {α β : Ω^ 2 X}
      (γ : α == idp^ 2) (δ : β == idp^ 2)
      → ap2 _∙_ γ δ == conc^2-comm α β ∙ ap2 _∙_ δ γ
    pt-lemma idp idp = idp

    C-abelian-lemma = Trunc-elim
      (λ _ → Π-level (λ _ → =-preserves-level _ Trunc-level))
      (λ {(f , fpt) → Trunc-elim
        (λ _ → =-preserves-level _ Trunc-level)
        (λ {(g , gpt) → ap [_] $ ⊙λ=
          (λ x → conc^2-comm (f x) (g x))
          (pt-lemma fpt gpt)})})

  {- CF, the functorial action of C:
   - contravariant functor from pointed spaces to abelian groups -}
  module _ (n : ℤ) {X Y : Ptd i} where

    {- before truncation - from pointed spaces to pointed spaces -}
    uCF : fst (X ⊙→ Y) → fst (⊙uCEl n Y ⊙→ ⊙uCEl n X)
    uCF f =
      ((λ g → g ⊙∘ f) ,
       pair= idp (∙-unit-r _ ∙ ap-cst idp (snd f)))

    CF-hom : fst (X ⊙→ Y) → (C n Y →ᴳ C n X)
    CF-hom f = record {
      f = Trunc-fmap {n = ⟨0⟩} (fst (uCF f));
      pres-comp = Trunc-elim
        (λ _ → Π-level (λ _ → =-preserves-level _ Trunc-level))
        (λ g → Trunc-elim
          (λ _ → =-preserves-level _ Trunc-level)
          (λ h → ap [_] $ pair= idp (comp-snd _∙_ f g h)))}
      where
      comp-snd : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {C : Type k}
        {c₁ c₂ : C} (_⊕_ : C → C → C) (f : fst (X ⊙→ Y))
        (g : fst (Y ⊙→ ⊙[ C , c₁ ])) (h : fst (Y ⊙→ ⊙[ C , c₂ ]))
        → ap (λ x → fst g x ⊕ fst h x) (snd f) ∙ ap2 _⊕_ (snd g) (snd h)
          == ap2 _⊕_ (ap (fst g) (snd f) ∙ snd g) (ap (fst h) (snd f) ∙ snd h)
      comp-snd _⊕_ (_ , idp) (_ , idp) (_ , idp) = idp

    CF : fst (X ⊙→ Y) → fst (⊙CEl n Y ⊙→ ⊙CEl n X)
    CF F = GroupHom.⊙f (CF-hom F)

  {- CF-hom is a functor from pointed spaces to abelian groups -}
  module _ (n : ℤ) {X : Ptd i} where

    CF-ident : CF-hom n {X} {X} (⊙idf X) == idhom (C n X)
    CF-ident = hom= _ _ $ λ= $ Trunc-elim
      (λ _ → =-preserves-level _ Trunc-level)
      (λ _ → idp)

    CF-comp : {Y Z : Ptd i} (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
      → CF-hom n (g ⊙∘ f) == CF-hom n f ∘ᴳ CF-hom n g
    CF-comp g f = hom= _ _ $ λ= $ Trunc-elim
      (λ _ → =-preserves-level _ Trunc-level)
      (λ h → ap [_] (! (⊙∘-assoc h g f)))

  {- Eilenberg-Steenrod Axioms -}

  {- Suspension Axiom -}
  C-Susp : (n : ℤ) (X : Ptd i) → C (succ n) (⊙Susp X) == C n X
  C-Susp n X =
    group-ua (SuspAdjointLoopIso.iso X (E (succ (succ n))))
    ∙ ap (→Ω-Group X) (spectrum (succ n))

  {- Non-truncated Exactness Axiom -}
  module _ (n : ℤ) {X Y : Ptd i} where

    {- [uCF n (⊙cfcod f) ∘ uCF n f] is constant -}
    uC-exact-itok-lemma : (f : fst (X ⊙→ Y)) (g : uCEl n (⊙Cof f))
      → fst (uCF n f) (fst (uCF n (⊙cfcod f)) g) == uCid n X
    uC-exact-itok-lemma (f , fpt) (g , gpt) = ⊙λ=
      (λ x → ap g (! (cfglue f x)) ∙ gpt)
      (ap (g ∘ cfcod f) fpt
       ∙ ap g (ap (cfcod f) (! fpt) ∙ ! (cfglue f (snd X))) ∙ gpt
         =⟨ lemma (cfcod f) g fpt (! (cfglue f (snd X))) gpt ⟩
       ap g (! (cfglue f (snd X))) ∙ gpt
         =⟨ ! (∙-unit-r _) ⟩
       (ap g (! (cfglue f (snd X))) ∙ gpt) ∙ idp ∎)
      where
      lemma : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
        {a₁ a₂ : A} {b : B} {c : C} (f : A → B) (g : B → C)
        (p : a₁ == a₂) (q : f a₁ == b) (r : g b == c)
        → ap (g ∘ f) p ∙ ap g (ap f (! p) ∙ q) ∙ r == ap g q ∙ r
      lemma f g idp idp idp = idp

    {- in kernel of [uCF n f] ⇒ in image of [uCF n (⊙cfcod f)] -}
    uC-exact-ktoi-lemma : (f : fst (X ⊙→ Y)) (g : uCEl n Y)
      → fst (uCF n f) g == uCid n X
      → Σ (uCEl n (⊙Cof f)) (λ h → fst (uCF n (⊙cfcod f)) h == g)
    uC-exact-ktoi-lemma (f , fpt) (h , hpt) p =
      ((g , ! q ∙ hpt) ,
       pair= idp (! (∙-assoc q (! q) hpt) ∙ ap (λ w → w ∙ hpt) (!-inv-r q)))
      where
      g : Cofiber f → Ω (E (succ n))
      g = CofiberRec.f f idp h (! ∘ app= (ap fst p))

      q : h (snd Y) == g (cfbase f)
      q = ap g (snd (⊙cfcod (f , fpt)))

  {- Truncated Exactness Axiom -}
  module _ (n : ℤ) {X Y : Ptd i} where

    {- in image of (CF n (⊙cfcod f)) ⇒ in kernel of (CF n f) -}
    abstract
      C-exact-itok : (f : fst (X ⊙→ Y))
        → is-exact-itok (CF n (⊙cfcod f)) (CF n f)
      C-exact-itok f =
        itok-alt-in (CF n (⊙cfcod f)) (CF n f) (Trunc-level {n = ⟨0⟩}) $
          Trunc-elim (λ _ → =-preserves-level _ (Trunc-level {n = ⟨0⟩}))
            (ap [_] ∘ uC-exact-itok-lemma n f)

    {- in kernel of (CF n f) ⇒ in image of (CF n (⊙cfcod f)) -}
    abstract
      C-exact-ktoi : (f : fst (X ⊙→ Y))
        → is-exact-ktoi (CF n (⊙cfcod f)) (CF n f)
      C-exact-ktoi f =
        Trunc-elim
          (λ _ → Π-level (λ _ → raise-level _ Trunc-level))
          (λ h tp → Trunc-rec Trunc-level (lemma h) (–> (Trunc=-equiv _ _) tp))
        where
        lemma : (h : uCEl n Y)
          → fst (uCF n f) h == uCid n X
          → Trunc ⟨-1⟩ (Σ (CEl n (⊙Cof f))
                          (λ tk → fst (CF n (⊙cfcod f)) tk == [ h ]))
        lemma h p = [ [ fst wit ] , ap [_] (snd wit) ]
          where
          wit : Σ (uCEl n (⊙Cof f)) (λ k → fst (uCF n (⊙cfcod f)) k == h)
          wit = uC-exact-ktoi-lemma n f h p

    C-exact : (f : fst (X ⊙→ Y)) → is-exact (CF n (⊙cfcod f)) (CF n f)
    C-exact f = record {itok = C-exact-itok f; ktoi = C-exact-ktoi f}

  {- Additivity Axiom -}
  module _ (n : ℤ) {A : Type i} (X : A → Ptd i)
    (ac : (W : A → Type i) → has-choice ⟨0⟩ A W)
    where

    uie : has-choice ⟨0⟩ A (uCEl n ∘ X)
    uie = ac (uCEl n ∘ X)

    R' : CEl n (⊙BigWedge X) → Trunc ⟨0⟩ (Π A (uCEl n ∘ X))
    R' = Trunc-rec Trunc-level (λ H → [ (λ a → H ⊙∘ ⊙bwin a) ])

    L' : Trunc ⟨0⟩ (Π A (uCEl n ∘ X)) → CEl n (⊙BigWedge X)
    L' = Trunc-rec Trunc-level
      (λ k → [ BigWedgeRec.f idp (fst ∘ k) (! ∘ snd ∘ k) , idp ])

    R = unchoose ∘ R'
    L = L' ∘ (is-equiv.g uie)

    R'-L' : ∀ y → R' (L' y) == y
    R'-L' = Trunc-elim
      (λ _ → =-preserves-level _ Trunc-level)
      (λ K → ap [_] (λ= (λ a → pair= idp $
        ap (BigWedgeRec.f idp (fst ∘ K) (! ∘ snd ∘ K)) (! (bwglue a)) ∙ idp
          =⟨ ∙-unit-r _ ⟩
        ap (BigWedgeRec.f idp (fst ∘ K) (! ∘ snd ∘ K)) (! (bwglue a))
          =⟨ ap-! (BigWedgeRec.f idp (fst ∘ K) (! ∘ snd ∘ K)) (bwglue a) ⟩
        ! (ap (BigWedgeRec.f idp (fst ∘ K) (! ∘ snd ∘ K)) (bwglue a))
          =⟨ ap ! (BigWedgeRec.glue-β idp (fst ∘ K) (! ∘ snd ∘ K) a) ⟩
        ! (! (snd (K a)))
          =⟨ !-! (snd (K a)) ⟩
        snd (K a) ∎)))

    L'-R' : ∀ x → L' (R' x) == x
    L'-R' = Trunc-elim
      {P = λ tH → L' (R' tH) == tH}
      (λ _ → =-preserves-level _ Trunc-level)
      (λ {(h , hpt) → ap [_] (pair=
         (λ= (L-R-fst (h , hpt)))
         (↓-app=cst-in $ ! $
            ap (λ w → w ∙ hpt) (app=-β (L-R-fst (h , hpt)) bwbase)
            ∙ !-inv-l hpt))})
      where
      lemma : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
        {a₁ a₂ : A} {b : B} (p : a₁ == a₂) (q : f a₁ == b)
        → ! q ∙ ap f p == ! (ap f (! p) ∙ q)
      lemma f idp idp = idp

      l∘r : fst (⊙BigWedge X ⊙→ ⊙Ω (E (succ n)))
        → (BigWedge X → Ω (E (succ n)))
      l∘r (h , hpt) =
        BigWedgeRec.f idp (λ a → h ∘ bwin a)
          (λ a → ! (ap h (! (bwglue a)) ∙ hpt))

      L-R-fst : (h : fst (⊙BigWedge X ⊙→ ⊙Ω (E (succ n))))
        → ∀ w → (l∘r h) w == fst h w
      L-R-fst (h , hpt) = BigWedge-elim
        (! hpt)
        (λ _ _ → idp)
        (λ a → ↓-='-in $
           ! hpt ∙ ap h (bwglue a)
             =⟨ lemma h (bwglue a) hpt ⟩
           ! (ap h (! (bwglue a)) ∙ hpt)
             =⟨ ! (BigWedgeRec.glue-β idp (λ a → h ∘ bwin a)
                     (λ a → ! (ap h (! (bwglue a)) ∙ hpt)) a) ⟩
           ap (l∘r (h , hpt)) (bwglue a) ∎)

    R-is-equiv : is-equiv R
    R-is-equiv = uie ∘ise (is-eq R' L' R'-L' L'-R')

    pres-comp : (tf tg : CEl n (⊙BigWedge X))
      → R (Group.comp (C n (⊙BigWedge X)) tf tg)
        == Group.comp (Πᴳ A (C n ∘ X)) (R tf) (R tg)
    pres-comp = Trunc-elim
      (λ _ → Π-level (λ _ → =-preserves-level _ (Π-level (λ _ → Trunc-level))))
      (λ {(f , fpt) → Trunc-elim
        (λ _ → =-preserves-level _ (Π-level (λ _ → Trunc-level)))
        (λ {(g , gpt) → λ= $ λ a → ap [_] $
          pair= idp (comp-snd f g (! (bwglue a)) fpt gpt)})})
      where
      comp-snd : ∀ {i j} {A : Type i} {B : Type j} {a₁ a₂ : A} {b₀ : B}
        {p q : b₀ == b₀} (f : A → b₀ == b₀) (g : A → b₀ == b₀)
        (r : a₁ == a₂) (α : f a₂ == p) (β : g a₂ == q)
        → ap (λ x → f x ∙ g x) r ∙ ap2 _∙_ α β
          == ap2 _∙_ (ap f r ∙ α) (ap g r ∙ β)
      comp-snd f g idp idp idp = idp

    abstract
      C-additive : C n (⊙BigWedge X) == Πᴳ A (C n ∘ X)
      C-additive = group-ua (group-hom R pres-comp , R-is-equiv)

open SpectrumModel

spectrum-cohomology : CohomologyTheory i
spectrum-cohomology = record {
  C = C;
  CF-hom = CF-hom;
  CF-ident = CF-ident;
  CF-comp = CF-comp;
  C-abelian = C-abelian;
  C-Susp = C-Susp;
  C-exact = C-exact;
  C-additive = C-additive}

spectrum-C-S⁰ : (n : ℤ) → C n (⊙Sphere O) == π 1 (ℕ-S≠O _) (E (succ n))
spectrum-C-S⁰ n = Bool⊙→Ω-is-π₁ (E (succ n))


text:
{-# OPTIONS --without-K #-}

open import Prelude
import GSeTT.Syntax
import GSeTT.Rules
open import CaTT.Ps-contexts
open import CaTT.Relation
open import CaTT.Uniqueness-Derivations-Ps
open import CaTT.Decidability-ps
open import CaTT.Fullness
import GSeTT.Typed-Syntax

module CaTT.CaTT where
   J : Set₁
   J = Σ (ps-ctx × Ty) λ {(Γ , A) → A is-full-in Γ }

   open import Globular-TT.Syntax J

   Ty→Pre-Ty : Ty → Pre-Ty
   Tm→Pre-Tm : Tm → Pre-Tm
   Sub→Pre-Sub : Sub → Pre-Sub

   Ty→Pre-Ty ∗ = ∗
   Ty→Pre-Ty (⇒ A t u) = ⇒ (Ty→Pre-Ty A) (Tm→Pre-Tm t) (Tm→Pre-Tm u)

   Tm→Pre-Tm (v x) = Var x
   Tm→Pre-Tm (coh Γ A Afull γ) = Tm-constructor (((Γ , A)) , Afull) (Sub→Pre-Sub γ)

   Sub→Pre-Sub <> = <>
   Sub→Pre-Sub < γ , x ↦ t > = < Sub→Pre-Sub γ , x ↦ Tm→Pre-Tm t >

   _[_]Ty : Ty → Sub → Ty
   _[_]Tm : Tm → Sub → Tm
   _∘ₛ_ : Sub → Sub → Sub

   ∗ [ σ ]Ty = ∗
   ⇒ A t u [ σ ]Ty = ⇒ (A [ σ ]Ty) (t [ σ ]Tm) (u [ σ ]Tm)
   v x [ <> ]Tm = v x
   v x [ < σ , y ↦ t > ]Tm = if x ≡ y then t else ((v x) [ σ ]Tm)
   coh Γ A full γ [ σ ]Tm = coh Γ A full (γ ∘ₛ σ)
   <> ∘ₛ γ = <>
   < γ , x ↦ t > ∘ₛ δ = < γ ∘ₛ δ , x ↦ t [ δ ]Tm >

   GPre-Ty→Ty : GSeTT.Syntax.Pre-Ty → Ty
   GPre-Ty→Ty GSeTT.Syntax.∗ = ∗
   GPre-Ty→Ty (GSeTT.Syntax.⇒ A (GSeTT.Syntax.Var x) (GSeTT.Syntax.Var y)) = ⇒ (GPre-Ty→Ty A) (v x) (v y)

   Ty→Pre-Ty[] : ∀ {A γ} → ((GPre-Ty A) [ Sub→Pre-Sub γ ]Pre-Ty) == Ty→Pre-Ty ((GPre-Ty→Ty A) [ γ ]Ty)
   Tm→Pre-Tm[] : ∀ {x γ} → ((Var x) [ Sub→Pre-Sub γ ]Pre-Tm) == Tm→Pre-Tm ((v x) [ γ ]Tm)
   Ty→Pre-Ty[] {GSeTT.Syntax.∗} {γ} = idp
   Ty→Pre-Ty[] {GSeTT.Syntax.⇒ A (GSeTT.Syntax.Var x) (GSeTT.Syntax.Var y)} {γ} = ap³ ⇒ Ty→Pre-Ty[] (Tm→Pre-Tm[] {x} {γ}) (Tm→Pre-Tm[] {y} {γ})
   Tm→Pre-Tm[] {x} {<>} = idp
   Tm→Pre-Tm[] {x} {< γ , y ↦ t >} with eqdecℕ x y
   ... | inl idp = idp
   ... | inr _ = Tm→Pre-Tm[] {x} {γ}

   dim-Pre-Ty[] : ∀ {A γ} → dim (Ty→Pre-Ty ((GPre-Ty→Ty A) [ γ ]Ty)) == dim (GPre-Ty A)
   dim-Pre-Ty[] {GSeTT.Syntax.∗} {γ} = idp
   dim-Pre-Ty[] {GSeTT.Syntax.⇒ A (GSeTT.Syntax.Var _) (GSeTT.Syntax.Var _)} {γ} = ap S dim-Pre-Ty[]

   rule : J → GSeTT.Typed-Syntax.Ctx × Pre-Ty
   rule ((Γ , A) , _) = (fst Γ , Γ⊢ps→Γ⊢ (snd Γ)) , Ty→Pre-Ty A

   open GSeTT.Typed-Syntax
   open import Sets ℕ eqdecℕ

   open import Globular-TT.Rules J rule
   open import Globular-TT.CwF-Structure J rule

   eqdecJ : eqdec J
   eqdecJ ((Γ , A) , Afull) ((Γ' , A') , A'full) with eqdec-ps Γ Γ' | CaTT.Fullness.eqdec-Ty A A'
   ...                                           | inl idp | inl idp = inl (ap (λ X → ((Γ , A) , X)) (is-prop-has-all-paths (is-prop-full Γ A) Afull A'full))
   ...                                           | inr Γ≠Γ' | _ = inr λ{idp → Γ≠Γ' idp}
   ...                                           | inl idp | inr A≠A' = inr λ{A=A' → A≠A' (snd (=, (fst-is-inj A=A')))}

   open import Globular-TT.Uniqueness-Derivations J rule eqdecJ
   open import Globular-TT.Disks J rule eqdecJ

   dim-tm : ∀ {Γ x A} → Γ ⊢t Var x # A → ℕ
   dim-tm {Γ} {x} {A} _ = dim A

   GdimT : ∀ {A} → GSeTT.Syntax.dim A == dim (GPre-Ty A)
   GdimT {GSeTT.Syntax.∗} = idp
   GdimT {GSeTT.Syntax.⇒ A _ _} = ap S GdimT

   GdimC : ∀ {Γ} → GSeTT.Syntax.dimC Γ == dimC (GPre-Ctx Γ)
   GdimC {nil} = idp
   GdimC {Γ :: (x , A)} = ap² max (GdimC {Γ}) GdimT

   G#∈ : ∀ {Γ x A} → x GSeTT.Syntax.# A ∈ Γ → x # (GPre-Ty A) ∈ (GPre-Ctx Γ)
   G#∈ {Γ :: a} (inl x∈Γ) = inl (G#∈ x∈Γ)
   G#∈ {Γ :: a} (inr (idp , idp)) = inr (idp , idp)

   G∈ : ∀ {Γ x} → x GSeTT.Syntax.∈ Γ → x ∈-set (varC Γ)
   G∈ {Γ :: (a , _)} (inl x∈Γ) = ∈-∪₁ {A = varC Γ} {B = singleton a} (G∈ x∈Γ)
   G∈ {Γ :: (x , _)} (inr idp) = ∈-∪₂ {A = varC Γ} {B = singleton x} (∈-singleton x)

   private
     every-term-has-variables : ∀ {Γ t A} → Γ ⊢t (Tm→Pre-Tm t) # A → Σ ℕ λ x → x ∈-set vart t
     every-term-has-variables {Γ} {v x} {A} Γ⊢t = x , ∈-singleton x
     every-term-has-variables {Γ} {coh (nil , (ps Δ⊢ps)) _ _ γ} {A} (tm _ Γ⊢γ idp) = ⊥-elim (∅-is-not-ps _ _ Δ⊢ps)
     every-term-has-variables {Γ} {coh ((_ :: _) , Δ⊢ps) _ _ <>} {A} (tm _ () idp)
     every-term-has-variables {Γ} {coh ((_ :: _) , Δ⊢ps) _ _ < γ , _ ↦ u >} {A} (tm _ (sc _ _ Γ⊢u _) idp) with every-term-has-variables Γ⊢u
     ... | (x , x∈) = x , ∈-∪₂ {A = varS γ} {B = vart u} x∈

     side-cond₁-not𝔻0 : ∀ Γ Γ⊢ps A t → (GPre-Ctx Γ) ⊢t (Tm→Pre-Tm t) # (Ty→Pre-Ty A) → ((varT A) ∪-set (vart t)) ⊂ (src-var (Γ , Γ⊢ps)) → Γ ≠ (nil :: (0 , GSeTT.Syntax.∗))
     side-cond₁-not𝔻0 .(nil :: (0 , GSeTT.Syntax.∗)) (ps pss) A t Γ⊢t incl idp with every-term-has-variables Γ⊢t | dec-≤ 0 0
     ... | x , x∈A | inl _ = incl _ (∈-∪₂ {A = varT A} {B = vart t} x∈A)
     ... | x , x∈A | inr _ = incl _ (∈-∪₂ {A = varT A} {B = vart t} x∈A)
     side-cond₁-not𝔻0 .(nil :: (0 , GSeTT.Syntax.∗)) (ps (psd Γ⊢psf)) A t Γ⊢t incl idp = ⇒≠∗ (𝔻0-type _ _ (psvar Γ⊢psf))

   max-srcᵢ-var-def : ∀ {Γ x A i} → (Γ⊢psx : Γ ⊢ps x # A) → 0 < i → ℕ × Pre-Ty
   max-srcᵢ-var-def pss _ = 0 , ∗
   max-srcᵢ-var-def (psd Γ⊢psx) 0<i = max-srcᵢ-var-def Γ⊢psx 0<i
   max-srcᵢ-var-def {_} {x} {A} {i} (pse Γ⊢psx idp idp idp idp idp) 0<i  with dec-≤ i (GSeTT.Syntax.dim A)
   ... | inl i≤dA = max-srcᵢ-var-def Γ⊢psx 0<i
   ... | inr dA<i with dec-≤ (GSeTT.Syntax.dim A) (dim (snd (max-srcᵢ-var-def Γ⊢psx 0<i)))
   ... | inl _ = max-srcᵢ-var-def Γ⊢psx 0<i
   ... | inr _ = x , GPre-Ty A

   max-srcᵢ-var-∈ : ∀ {Γ x A i} → (Γ⊢psx : Γ ⊢ps x # A) → (0<i : 0 < i) → fst (max-srcᵢ-var-def Γ⊢psx 0<i) ∈-list (srcᵢ-var i Γ⊢psx)
   max-srcᵢ-var-∈ pss 0<i = transport {B = 0 ∈-list_} (simplify-if 0<i ^) (inr idp)
   max-srcᵢ-var-∈ (psd Γ⊢psx) 0<i = max-srcᵢ-var-∈ Γ⊢psx 0<i
   max-srcᵢ-var-∈ {Γ} {x} {A} {i} (pse Γ⊢psx idp idp idp idp idp) 0<i with dec-≤ i (GSeTT.Syntax.dim A)
   ... | inl _ = max-srcᵢ-var-∈ Γ⊢psx 0<i
   ... | inr _  with dec-≤ (GSeTT.Syntax.dim A) (dim (snd (max-srcᵢ-var-def Γ⊢psx 0<i)))
   ... | inl _ = inl (inl (max-srcᵢ-var-∈ Γ⊢psx 0<i))
   ... | inr _ = inr idp

   max-srcᵢ-var-⊢ : ∀ {Γ x A i} → (Γ⊢psx : Γ ⊢ps x # A) → (0<i : 0 < i) → GPre-Ctx Γ ⊢t Var (fst (max-srcᵢ-var-def Γ⊢psx 0<i)) # snd (max-srcᵢ-var-def Γ⊢psx 0<i)
   max-srcᵢ-var-⊢ pss 0<i = var (cc ec (ob ec) idp) (inr (idp , idp))
   max-srcᵢ-var-⊢ (psd Γ⊢psx) 0<i = max-srcᵢ-var-⊢ Γ⊢psx 0<i
   max-srcᵢ-var-⊢ {Γ} {x} {A} {i} Γ+⊢ps@(pse Γ⊢psx idp idp idp idp idp) 0<i with dec-≤ i (GSeTT.Syntax.dim A)
   ... | inl _ = wkt (wkt (max-srcᵢ-var-⊢ Γ⊢psx 0<i) ((GCtx _ (GSeTT.Rules.Γ,x:A⊢→Γ⊢ (psv Γ+⊢ps))))) (GCtx _ (psv Γ+⊢ps))
   ... | inr _  with dec-≤ (GSeTT.Syntax.dim A) (dim (snd (max-srcᵢ-var-def Γ⊢psx 0<i)))
   ... | inl _ = wkt (wkt (max-srcᵢ-var-⊢ Γ⊢psx 0<i) ((GCtx _ (GSeTT.Rules.Γ,x:A⊢→Γ⊢ (psv Γ+⊢ps))))) (GCtx _ (psv Γ+⊢ps))
   ... | inr _ = var (GCtx _ (psv Γ+⊢ps)) (inr (idp , idp))

   max-srcᵢ-var-dim : ∀ {Γ x A i} → (Γ⊢psx : Γ ⊢ps x # A) → (0<i : 0 < i) →  min i (S (dimC (GPre-Ctx Γ))) == S (dim (snd (max-srcᵢ-var-def Γ⊢psx 0<i)))
   max-srcᵢ-var-dim pss 0<i = simplify-min-r 0<i
   max-srcᵢ-var-dim (psd Γ⊢psx) 0<i = max-srcᵢ-var-dim Γ⊢psx 0<i
   max-srcᵢ-var-dim {Γ} {x} {A} {i} (pse {Γ = Δ} Γ⊢psx idp idp idp idp idp) 0<i with dec-≤ i (GSeTT.Syntax.dim A)
   ... | inl i≤dA = simplify-min-l (n≤m→n≤Sm (≤T (≤-= i≤dA (GdimT {A})) (m≤max (max (dimC (GPre-Ctx Δ)) _) (dim (GPre-Ty A))) )) >> (simplify-min-l (≤T i≤dA (≤-= (S≤ (dim-dangling Γ⊢psx)) (ap S (GdimC {Δ})))) ^) >> max-srcᵢ-var-dim Γ⊢psx 0<i
   max-srcᵢ-var-dim {Γ} {x} {A} {i} (pse {Γ = Δ} Γ⊢psx idp idp idp idp idp) 0<i | inr dA<i with dec-≤ (GSeTT.Syntax.dim A) (dim (snd (max-srcᵢ-var-def Γ⊢psx 0<i)))
   ... | inl dA≤m = let dA<dΔ = (S≤S (≤T (=-≤-= (ap S (GdimT {A} ^)) (S≤ dA≤m) (max-srcᵢ-var-dim Γ⊢psx 0<i ^)) (min≤m i (S (dimC (GPre-Ctx Δ)))))) in
                    ap (min i)
                    (ap S (simplify-max-l {max (dimC (GPre-Ctx Δ)) _} {dim (GPre-Ty A)} (≤T dA<dΔ (n≤max _ _))
                           >> simplify-max-l {dimC (GPre-Ctx Δ)} {_} (Sn≤m→n≤m dA<dΔ)))
                    >> max-srcᵢ-var-dim Γ⊢psx 0<i
   ... | inr m<dA = simplify-min-r {i} {S (max (max (dimC (GPre-Ctx Δ)) _) (dim (GPre-Ty A)))}
                      (up-maxS {max (dimC (GPre-Ctx Δ)) _} {dim (GPre-Ty A)}
                               (up-maxS {dimC (GPre-Ctx Δ)} {_}
                                  (min<l (=-≤ (ap S (max-srcᵢ-var-dim Γ⊢psx 0<i)) (≤T (S≤ (≰ m<dA)) (≰ dA<i))))
                                  (=-≤ (GdimT {A} ^) (≤T (n≤Sn _) (≰ dA<i))))
                               (=-≤ (ap S (GdimT {A}) ^) (≰ dA<i)))
                    >> ap S (simplify-max-r {max (dimC (GPre-Ctx Δ)) _} {dim (GPre-Ty A)}
                            (up-max {dimC (GPre-Ctx Δ)} {_} (≤-= (Sn≤m→n≤m (greater-than-min-r (≰ dA<i) (=-≤ (max-srcᵢ-var-dim Γ⊢psx 0<i) (≰ m<dA)))) (ap S GdimT)) (n≤Sn _)))

   max-srcᵢ-var : ∀ {Γ x A i} → (Γ⊢psx : Γ ⊢ps x # A) → 0 < i → Σ (Σ (ℕ × Pre-Ty) (λ {(x , B) → GPre-Ctx Γ ⊢t Var x # B})) (λ {((x , B) , Γ⊢x) → (x ∈-list (srcᵢ-var i Γ⊢psx)) × (min i (S (dimC (GPre-Ctx Γ))) == S (dim-tm Γ⊢x))})
   max-srcᵢ-var Γ⊢psx 0<i = (max-srcᵢ-var-def Γ⊢psx 0<i , max-srcᵢ-var-⊢ Γ⊢psx 0<i) , (max-srcᵢ-var-∈ Γ⊢psx 0<i , max-srcᵢ-var-dim Γ⊢psx 0<i)

   max-src-var : ∀ Γ → (Γ⊢ps : Γ ⊢ps) → (Γ ≠ (nil :: (0 , GSeTT.Syntax.∗))) → Σ (Σ (ℕ × Pre-Ty) (λ {(x , B) → GPre-Ctx Γ ⊢t Var x # B})) (λ {((x , B) , Γ⊢x) → (x ∈-set (src-var (Γ , Γ⊢ps))) × (dimC (GPre-Ctx Γ) == S (dim-tm Γ⊢x))})
   max-src-var Γ Γ⊢ps@(ps Γ⊢psx) Γ≠𝔻0 with max-srcᵢ-var {i = GSeTT.Syntax.dimC Γ} Γ⊢psx (dim-ps-not-𝔻0 Γ⊢ps Γ≠𝔻0)
   ... | ((x , B) , (x∈ , p)) = (x , B) , (∈-list-∈-set _ _ x∈ , (ap (λ n → min n (S (dimC (GPre-Ctx Γ)))) (GdimC {Γ}) >> simplify-min-l (n≤Sn _) ^ >> p) )

   full-term-have-max-variables : ∀ {Γ A Γ⊢ps} → GPre-Ctx Γ ⊢T (Ty→Pre-Ty A) → A is-full-in ((Γ , Γ⊢ps)) →
     Σ (Σ (ℕ × Pre-Ty) (λ {(x , B) → GPre-Ctx Γ ⊢t Var x # B})) (λ {((x , B) , Γ⊢x) → (x ∈-set varT A) × (dimC (GPre-Ctx Γ) ≤ S (dim-tm Γ⊢x))})
   full-term-have-max-variables {Γ} {_} {Γ⊢ps} Γ⊢A (side-cond₁ .(_ , _) A t u (incl , incl₂) _) with max-src-var Γ Γ⊢ps (side-cond₁-not𝔻0 _ Γ⊢ps A t (Γ⊢src Γ⊢A) incl₂)
   ... | ((x , B) , Γ⊢x) , (x∈src , dimΓ=Sdimx) = ((x , B) , Γ⊢x) , (A∪B⊂A∪B∪C (varT A) (vart t) (vart u) _ (incl _ x∈src) , transport {B = λ x → (dimC (GPre-Ctx Γ)) ≤ x} dimΓ=Sdimx (n≤n _))
   full-term-have-max-variables {Γ} {_} {Γ⊢ps@(ps Γ⊢psx)} _ (side-cond₂ .(_ , _) _ (incl , _)) with max-var {Γ} Γ⊢ps
   ... | (x , B) , (x∈Γ , dimx) = ((x , (GPre-Ty B)) , var (GCtx Γ (psv Γ⊢psx)) (G#∈ x∈Γ)) , (incl _ (G∈ (x#A∈Γ→x∈Γ x∈Γ)) , ≤-= (=-≤ ((GdimC {Γ} ^) >> dimx) (n≤Sn _)) (ap S GdimT))

   dim-∈-var : ∀ {Γ A x B} → Γ ⊢t Var x # B → Γ ⊢T (Ty→Pre-Ty A) → x ∈-set varT A → dim B < dim (Ty→Pre-Ty A)
   dim-∈-var-t : ∀ {Γ t A x B} → Γ ⊢t Var x # B → Γ ⊢t (Tm→Pre-Tm t) # (Ty→Pre-Ty A) → x ∈-set vart t → dim B ≤ dim (Ty→Pre-Ty A)
   dim-∈-var-S : ∀ {Δ γ Γ x B} → Δ ⊢t Var x # B → Δ ⊢S (Sub→Pre-Sub γ) > (GPre-Ctx Γ) → x ∈-set varS γ → dim B ≤ dimC (GPre-Ctx Γ)
   dim-full-ty : ∀ {Γ A} → (Γ⊢ps : Γ ⊢ps) → (GPre-Ctx Γ) ⊢T (Ty→Pre-Ty A) → A is-full-in (Γ , Γ⊢ps) → dimC (GPre-Ctx Γ) ≤ dim (Ty→Pre-Ty A)

   dim-∈-var {Γ} {A⇒@(⇒ A t u)} {x} {B} Γ⊢x (ar Γ⊢A Γ⊢t Γ⊢u) x∈A⇒ with ∈-∪ {varT A} {vart t ∪-set vart u} x∈A⇒
   ... | inl x∈A = n≤m→n≤Sm (dim-∈-var Γ⊢x Γ⊢A x∈A)
   ... | inr x∈t∪u with ∈-∪ {vart t} {vart u} x∈t∪u
   ... | inl x∈t = S≤ (dim-∈-var-t Γ⊢x Γ⊢t x∈t)
   ... | inr x∈u = S≤ (dim-∈-var-t Γ⊢x Γ⊢u x∈u)
   dim-∈-var-t {t = v x} Γ⊢x Γ⊢t (inr idp) with unique-type Γ⊢x Γ⊢t (ap Var idp)
   ... | idp = n≤n _
   dim-∈-var-t {t = coh Γ A Afull γ} Γ⊢x (tm Γ⊢A Δ⊢γ:Γ p) x∈t = ≤-= (≤T (dim-∈-var-S Γ⊢x Δ⊢γ:Γ x∈t) (dim-full-ty (snd Γ) Γ⊢A Afull) ) ((dim[] _ _ ^) >> ap dim (p ^))
   dim-∈-var-S {Δ} {< γ , y ↦ t >} {Γ :: (_ , A)} {x} {B} Δ⊢x (sc Δ⊢γ:Γ Γ+⊢ Δ⊢t idp) x∈γ+ with ∈-∪ {varS γ} {vart t} x∈γ+
   ... | inl x∈γ = ≤T (dim-∈-var-S Δ⊢x Δ⊢γ:Γ x∈γ) (n≤max _ _)
   ... | inr x∈t = ≤T (dim-∈-var-t Δ⊢x (transport {B = Δ ⊢t (Tm→Pre-Tm t) #_} Ty→Pre-Ty[] Δ⊢t) x∈t) (=-≤ (dim-Pre-Ty[]) (m≤max (dimC (GPre-Ctx Γ)) (dim (GPre-Ty A))))
   dim-full-ty Γ⊢ps Γ⊢A Afull with full-term-have-max-variables Γ⊢A Afull
   ... | ((x , B) , Γ⊢x) , (x∈A , dimx) = ≤T dimx (dim-∈-var Γ⊢x Γ⊢A x∈A)

   well-foundedness : well-founded
   well-foundedness ((Γ , A) , Afull) Γ⊢A with full-term-have-max-variables Γ⊢A Afull
   ... |((x , B) , Γ⊢x) , (x∈Γ , dimΓ≤Sdimx) = ≤T dimΓ≤Sdimx (dim-∈-var Γ⊢x Γ⊢A x∈Γ)

   open import Globular-TT.Dec-Type-Checking J rule well-foundedness eqdecJ

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
module Issue1494 where

open import Issue1494.Helper

module M (r : Record) where

  open Module r

  postulate
    A   : Set
    a b : A

  Foo : a ≡ b
  Foo = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}

open import M-types.Base.Core

module M-types.Base.Sum  where
    infixr 4 _,_
    record ∑ (X : Ty ℓ₀) (Y : X → Ty ℓ₁) : Ty (ℓ-max ℓ₀ ℓ₁) where
        constructor _,_
        field
            pr₀ : X
            pr₁ : Y pr₀
    open ∑ public
    {-# BUILTIN SIGMA ∑ #-}

    ∑-syntax : (X : Ty ℓ₀) → (Y : X → Ty ℓ₁) → Ty (ℓ-max ℓ₀ ℓ₁)
    ∑-syntax = ∑
    infix 2 ∑-syntax
    syntax ∑-syntax X (λ x → Y) = ∑[ x ∈ X ] Y

    infixr 2 _×_
    _×_ : (X : Ty ℓ₀) → (Y : Ty ℓ₁) → Ty (ℓ-max ℓ₀ ℓ₁)
    X × Y = ∑[ x ∈ X ] Y

    ty = pr₀
    fun = pr₀

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
module WellTypedTerms where

open import Library
open import Categories
open import Functors
open import RMonads
open import FunctorCat
open import Categories.Sets
open import Categories.Families

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty

data Con : Set where
  ε   : Con
  _<_ : Con → Ty → Con

data Var : Con → Ty → Set where
  vz : ∀{Γ σ} → Var (Γ < σ) σ
  vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ

data Tm : Con → Ty → Set where
  var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
  app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
  lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)

Ren : Con → Con → Set
Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ

renId : ∀{Γ} → Ren Γ Γ
renId = id

renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
renComp f g = f ∘ g

ConCat : Cat
ConCat = record{
  Obj  = Con;
  Hom  = Ren;
  iden = renId;
  comp = renComp;
  idl  = iext λ _ → refl;
  idr  = iext λ _ → refl;
  ass  = iext λ _ → refl}

wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ < σ) (Δ < σ)
wk f vz     = vz
wk f (vs i) = vs (f i)

ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
ren f (var x)   = var (f x)
ren f (app t u) = app (ren f t) (ren f u)
ren f (lam t)   = lam (ren (wk f) t)

wkid : ∀{Γ σ τ}(x : Var (Γ < τ) σ) → wk renId x ≅ renId x
wkid vz     = refl
wkid (vs x) = refl

renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
renid (var x)   = refl
renid (app t u) =
  proof
  app (ren renId t) (ren renId u)
  ≅⟨ cong₂ app (renid t) (renid u) ⟩
  app t u
  ∎
renid (lam t)   =
  proof lam (ren (wk renId) t)
  ≅⟨ cong (λ (f : Ren _ _) → lam (ren f t)) (iext λ _ → ext wkid) ⟩
  lam (ren renId t)
  ≅⟨ cong lam (renid t) ⟩
  lam t
  ∎

wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
            wk (renComp f g) x ≅ renComp (wk f) (wk g) x
wkcomp f g vz     = refl
wkcomp f g (vs i) = refl

rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
            ren (renComp f g) t ≅ (ren f ∘ ren g) t
rencomp f g (var x)   = refl
rencomp f g (app t u) =
  proof
  app (ren (renComp f g) t) (ren (renComp f g) u)
  ≅⟨ cong₂ app (rencomp f g t) (rencomp f g u) ⟩
  app (ren f (ren g t)) (ren f (ren g u))
  ∎
rencomp f g (lam t)   =
  proof
  lam (ren (wk (renComp f g)) t)
  ≅⟨ cong (λ (f : Ren _ _) → lam (ren f t)) (iext λ _ → ext (wkcomp f g)) ⟩
  lam (ren (renComp (wk f) (wk g)) t)
  ≅⟨ cong lam (rencomp (wk f) (wk g) t) ⟩
  lam (ren (wk f) (ren (wk g) t))
  ∎

Sub : Con → Con → Set
Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ

lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ < σ) (Δ < σ)
lift f vz     = var vz
lift f (vs x) = ren vs (f x)

sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
sub f (var x)   = f x
sub f (app t u) = app (sub f t) (sub f u)
sub f (lam t)   = lam (sub (lift f) t)

subId : ∀{Γ} → Sub Γ Γ
subId = var

subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
subComp f g = sub f ∘ g

liftid : ∀{Γ σ τ}(x : Var (Γ < σ) τ) → lift subId x ≅ subId x
liftid vz     = refl
liftid (vs x) = refl

subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
subid (var x)   = refl
subid (app t u) =
  proof
  app (sub subId t) (sub subId u)
  ≅⟨ cong₂ app (subid t) (subid u) ⟩
  app t u
  ∎
subid (lam t)   =
  proof
  lam (sub (lift subId) t)
  ≅⟨ cong (λ (f : Sub _ _) → lam (sub f t)) (iext λ _ → ext liftid) ⟩
  lam (sub subId t)
  ≅⟨ cong lam (subid t) ⟩
  lam t
  ∎

-- time for the mysterious four lemmas:
liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
            (lift f ∘ wk g) x ≅ lift (f ∘ g) x
liftwk f g vz     = refl
liftwk f g (vs x) = refl

subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
         (sub f ∘ ren g) t ≅ sub (f ∘ g) t
subren f g (var x)   = refl
subren f g (app t u) =
  proof
  app (sub f (ren g t)) (sub f (ren g u))
  ≅⟨ cong₂ app (subren f g t) (subren f g u) ⟩
  app (sub (f ∘ g) t) (sub (f ∘ g) u)
  ∎
subren f g (lam t)   =
  proof
  lam (sub (lift f) (ren (wk g) t))
  ≅⟨ cong lam (subren (lift f) (wk g) t) ⟩
  lam (sub (lift f ∘ wk g) t)
  ≅⟨ cong (λ (f : Sub _ _) → lam (sub f t)) (iext (λ _ → ext (liftwk f g))) ⟩
  lam (sub (lift (f ∘ g)) t) ∎

renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
               (ren (wk f) ∘ lift g) x ≅ lift (ren f ∘ g) x
renwklift f g vz     = refl
renwklift f g (vs x) =
  proof
  ren (wk f) (ren vs (g x))
  ≅⟨ sym (rencomp (wk f) vs (g x)) ⟩
  ren (wk f ∘ vs) (g x)
  ≅⟨ rencomp vs f (g x) ⟩
  ren vs (ren f (g x))
  ∎

rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
         (ren f ∘ sub g) t ≅ sub (ren f ∘ g) t
rensub f g (var x)   = refl
rensub f g (app t u) =
  proof
  app (ren f (sub g t)) (ren f (sub g u))
  ≅⟨ cong₂ app (rensub f g t) (rensub f g u) ⟩
  app (sub (ren f ∘ g) t) (sub (ren f ∘ g) u)
  ∎
rensub f g (lam t)   =
  proof
  lam (ren (wk f) (sub (lift g) t))
  ≅⟨ cong lam (rensub (wk f) (lift g) t) ⟩
  lam (sub (ren (wk f) ∘ lift g) t)
  ≅⟨ cong (λ (f₁ : Sub _ _) → lam (sub f₁ t))
          (iext (λ _ → ext (renwklift f g))) ⟩
  lam (sub (lift (ren f ∘ g)) t)
  ∎

liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
           lift (subComp f g) x ≅ subComp (lift f) (lift g) x
liftcomp f g vz     = refl
liftcomp f g (vs x) =
  proof
  ren vs (sub f (g x))
  ≅⟨ rensub vs f (g x) ⟩
  sub (ren vs ∘ f) (g x)
  ≅⟨ sym (subren (lift f) vs (g x)) ⟩
  sub (lift f) (ren vs (g x))
  ∎

subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
          sub (subComp f g) t ≅ (sub f ∘ sub g) t
subcomp f g (var x)   = refl
subcomp f g (app t u) =
  proof
  app (sub (subComp f g) t) (sub (subComp f g) u)
  ≅⟨ cong₂ app (subcomp f g t) (subcomp f g u) ⟩
  app (sub f (sub g t)) (sub f (sub g u))
  ∎
subcomp f g (lam t)   =
  proof
  lam (sub (lift (subComp f g)) t)
  ≅⟨ cong (λ (f : Sub _ _) → lam (sub f t))
          (iext λ _ → ext (liftcomp f g)) ⟩
  lam (sub (subComp (lift f) (lift g)) t)
  ≅⟨ cong lam (subcomp (lift f) (lift g) t) ⟩
  lam (sub (lift f) (sub (lift g) t)) ∎

VarF : Fun ConCat (Fam Ty)
VarF = record {
  OMap  = Var;
  HMap  = id;
  fid   = refl;
  fcomp = refl }

TmRMonad : RMonad VarF
TmRMonad = record {
  T    = Tm;
  η    = var;
  bind = sub;
  law1 = iext λ _ → ext subid ;
  law2 = refl;
  law3 = λ{_ _ _ f g} → iext λ σ → ext (subcomp g f)}

-- not needed here
sub<< : ∀{Γ Δ σ}(f : Sub Γ Δ)(t : Tm Δ σ) → Sub (Γ < σ) Δ
sub<< f t vz     = t
sub<< f t (vs x) = f x

lem1 : ∀{B Γ Δ σ}{f : Sub Γ Δ}{g : Ren B Γ}{t : Tm Δ σ}{τ}(x : Var (B < σ) τ) →
        (sub<< f t ∘ wk g) x ≅ (sub<< (f ∘ g) t) x
lem1 vz     = refl
lem1 (vs x) = refl

lem2 : ∀{B Γ Δ σ}{f : Sub Γ Δ}{g : Sub B Γ}{t : Tm Δ σ}{τ}(x : Var (B < σ) τ) →
       (subComp (sub<< f t) (lift g)) x ≅ (sub<< (subComp f g) t) x
lem2 vz     = refl
lem2 {f = f}{g = g}{t = t} (vs x) = subren (sub<< f t) vs (g x)

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module Ag04 where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

infix 4 _≡_

≡-sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
≡-sym refl = refl

trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
  → u ≡ x → v ≡ y → f u v ≡ f x y
cong₂ f refl refl = refl

cong-app : ∀ {A B : Set} {f g : A → B} → f ≡ g → ∀ (x : A) → f x ≡ g x
cong-app refl x = refl

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + m = m
(suc n) + m = suc (n + m)

postulate
  +-identity : ∀ (m : ℕ) → m + zero ≡ m
  +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
  +-comm : ∀ (m n : ℕ) → m + n ≡ n + m

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

refl-≐ : ∀ {A : Set} {x : A} → x ≐ x
refl-≐ P Px = Px

trans-≐ : ∀ {A : Set} {x y z : A} → x ≐ y → y ≐ z → x ≐ z
trans-≐ x≐y y≐z P Px = y≐z P (x≐y P Px)

sym-≐ : ∀ {A : Set} {x y : A} → x ≐ y → y ≐ x
sym-≐ {A} {x} {y} x≐y P = Qy
  where
    Q : A → Set
    Q z = P z → P x
    Qx : Q x
    Qx = refl-≐ P
    Qy : Q y
    Qy = x≐y Q Qx

subst : ∀ {A : Set} {x y : A} (P : A → Set)
  → x ≡ y
    ---------
  → P x → P y
subst P refl px = px

≡-implies-≐ : ∀ {A : Set} {x y : A} → x ≡ y → x ≐ y
≡-implies-≐ x≡y P = subst P x≡y

≐-implies-≡ : ∀ {A : Set} {x y : A} → x ≐ y → x ≡ y
≐-implies-≡ {A} {x} {y} x≐y = Qy
  where
    Q : A → Set
    Q z = x ≡ z
    Qx : Q x
    Qx = refl
    Qy : Q y
    Qy = x≐y Q Qx

open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

data _≡'_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl' : x ≡' x

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
------------------------------------------------------------------------------
-- Definition of FOTC Conat using Agda's co-inductive combinators
------------------------------------------------------------------------------

{-# OPTIONS --allow-unsolved-metas     #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOT.FOTC.Data.Conat.TypeSL where

open import Codata.Musical.Notation
open import FOTC.Base

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

data Conat : D → Set where
  cozero : Conat zero
  cosucc : ∀ {n} → ∞ (Conat n) → Conat (succ₁ n)

Conat-out : ∀ {n} → Conat n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n')
Conat-out cozero          = inj₁ refl
Conat-out (cosucc {n} Cn) = inj₂ (n , refl , ♭ Cn)

Conat-in : ∀ {n} →
           n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ Conat n') →
           Conat n
Conat-in (inj₁ n≡0)              = subst Conat (sym n≡0) cozero
Conat-in (inj₂ (n' , prf , Cn')) = subst Conat (sym prf) (cosucc (♯ Cn'))

-- TODO (2019-01-04): Agda doesn't accept this definition which was
-- accepted by a previous version.
{-# TERMINATING #-}
Conat-coind : (A : D → Set) →
              (∀ {n} → A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) →
              ∀ {n} → A n → Conat n
Conat-coind A h An with h An
... | inj₁ refl = cozero
... | inj₂ (n' , refl , An') = cosucc (♯ (Conat-coind A h An'))

-- TODO (07 January 2014): We couldn't prove Conat-stronger-coind.
Conat-stronger-coind :
  ∀ (A : D → Set) {n} →
  (A n → n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ A n')) →
  A n → Conat n
Conat-stronger-coind A h An with h An
... | inj₁ n≡0 = subst Conat (sym n≡0) cozero
... | inj₂ (n' , prf , An') =
  subst Conat (sym prf) (cosucc (♯ (Conat-coind A {!!} An')))

postulate
  ∞D    : D
  ∞-eq : ∞D ≡ succ₁ ∞D

-- TODO (06 January 2014): Agda doesn't accept the proof of Conat ∞D.
{-# TERMINATING #-}
∞-Conat : Conat ∞D
∞-Conat = subst Conat (sym ∞-eq) (cosucc (♯ ∞-Conat))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module DuplicateBuiltinBinding where

{-# BUILTIN STRING String #-}
{-# BUILTIN STRING String #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
data Nat : Set where
  succ : Nat → Nat

data Fin : Nat → Set where
  zero : (n : Nat) → Fin (succ n)

data Tm (n : Nat) : Set where
  var : Fin n → Tm n
  piv : Fin (succ n) → Tm n

data Cx : Nat → Set where
  succ : (n : Nat) → Tm n → Cx (succ n)

data CxChk : ∀ n → Cx n → Set where
  succ : (n : Nat) (T : Tm n) → CxChk (succ n) (succ n T)

data TmChk (n : Nat) : Cx n → Tm n → Set where
  vtyp : (g : Cx n) (v : Fin n) → CxChk n g → TmChk n g (var v)

error : ∀ n g s → TmChk n g s → Set
error n g s (vtyp g' (zero x) (succ n' (piv (zero y)))) =  Nat -- Internal error here.
error _ _ _ (vtyp g' (zero n) (succ n (var x))) = Nat -- This clause added to pass 2.5.3.

max_stars_repo_name: Forty-Bot/agda

max_issues_repo_name: Forty-Bot/agda

max_forks_repo_name: Forty-Bot/agda


text:
module Common.Coinduction where

open import Common.Level

infix 1000 ♯_

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

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

private

  my-♯ : ∀ {a} {A : Set a} → A → ∞ A
  my-♯ x = ♯ x

max_stars_repo_name: asr/agda-kanso


text:
{-# OPTIONS --without-K #-}

open import HoTT

module cw.Attached {i j k : ULevel} where

-- The type of attaching maps.
-- In intended uses, [B] is the type of cells and [C] is the [Sphere]s.
Attaching : (A : Type i) (B : Type j) (C : Type k) → Type (lmax i (lmax j k))
Attaching A B C = B → C → A

module _ {A : Type i} {B : Type j} {C : Type k} where

  -- [Attached] is the type with all the cells attached.

  Attached-span : Attaching A B C → Span {i} {j} {lmax j k}
  Attached-span attaching = span A B (B × C) (uncurry attaching) fst

  Attached : Attaching A B C → Type (lmax i (lmax j k))
  Attached attaching = Pushout (Attached-span attaching)

module _ {A : Type i} {B : Type j} {C : Type k} {attaching : Attaching A B C} where

  incl : A → Attached attaching
  incl = left

  hub : B → Attached attaching
  hub = right

  spoke : ∀ b c → incl (attaching b c) == hub b
  spoke = curry glue

  module AttachedElim {l} {P : Attached attaching → Type l}
    (incl* : (a : A) → P (incl a))
    (hub* : (b : B) → P (hub b))
    (spoke* : (b : B) (c : C)
      → incl* (attaching b c) == hub* b [ P ↓ spoke b c ]) where

    module P = PushoutElim
      {d = Attached-span attaching} {P = P}
      incl* hub* (uncurry spoke*)

    f = P.f
    spoke-β = curry P.glue-β

  open AttachedElim public using () renaming (f to Attached-elim)

  module AttachedRec {l} {D : Type l}
    (incl* : (a : A) → D)
    (hub* : (b : B) → D)
    (spoke* : (b : B) (c : C) → incl* (attaching b c) == hub* b) where

    module P = PushoutRec
      {d = Attached-span attaching} {D = D}
      incl* hub* (uncurry spoke*)

    f = P.f
    spoke-β = curry P.glue-β

  open AttachedRec public using () renaming (f to Attached-rec)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda