text:
------------------------------------------------------------------------
-- A large(r) class of algebraic structures satisfies the property
-- that isomorphic instances of a structure are equal (assuming
-- univalence)
------------------------------------------------------------------------

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

-- Note that this module uses ordinary propositional equality, with a
-- computing J rule.

-- This module has been developed in collaboration with Thierry
-- Coquand.

module Univalence-axiom.Isomorphism-is-equality.More where

open import Equality.Propositional
  hiding (refl) renaming (equality-with-J to eq)
open import Equality
open Derived-definitions-and-properties eq using (refl)

open import Bijection eq hiding (id; _∘_; inverse; step-↔; finally-↔)
open import Equivalence eq as Eq hiding (id; _∘_; inverse)
open import Function-universe eq hiding (id; _∘_)
open import H-level eq as H-level hiding (Proposition)
open import H-level.Closure eq
open import Logical-equivalence using (_⇔_)
open import Preimage eq
open import Prelude as P hiding (Type)
open import Univalence-axiom eq

------------------------------------------------------------------------
-- A record packing up certain assumptions

-- Use of these or similar assumptions is usually not documented in
-- comments below (with remarks like "assuming univalence").

record Assumptions : P.Type₂ where
  field
    ext₁  : Extensionality (# 1) (# 1)
    univ  : Univalence (# 0)
    univ₁ : Univalence (# 1)

  abstract

    ext : Extensionality (# 0) (# 0)
    ext = lower-extensionality (# 1) (# 1) ext₁

------------------------------------------------------------------------
-- A class of algebraic structures

-- An algebraic structure universe.

mutual

  -- Codes for structures.

  infixl 5 _▻_

  data Code : P.Type₂ where
    ε   : Code
    _▻_ : (c : Code) → Extension c → Code

  -- Structures can contain arbitrary "extensions".

  record Extension (c : Code) : P.Type₂ where
    field

      -- An instance-indexed type.

      Ext : ⟦ c ⟧ → P.Type₁

      -- A predicate specifying when two elements are isomorphic with
      -- respect to an isomorphism.

      Iso : (ass : Assumptions) →
            {I J : ⟦ c ⟧} → Isomorphic ass c I J →
            Ext I → Ext J → P.Type₁

    -- An alternative definition of Iso.

    Iso′ : (ass : Assumptions) →
           ∀ {I J} → Isomorphic ass c I J →
           Ext I → Ext J → P.Type₁
    Iso′ ass I≅J x y =
      subst Ext (_≃_.to (isomorphism≃equality ass c) I≅J) x ≡ y

    field

      -- Iso and Iso′ are equivalent.

      Iso≃Iso′ :
        (ass : Assumptions) →
        ∀ {I J} (I≅J : Isomorphic ass c I J) {x y} →
        Iso ass I≅J x y ≃ Iso′ ass I≅J x y

  -- Interpretation of the codes. The elements of ⟦ c ⟧ are instances
  -- of the structure encoded by c.

  ⟦_⟧ : Code → P.Type₁
  ⟦ ε     ⟧ = ↑ _ ⊤
  ⟦ c ▻ e ⟧ = Σ ⟦ c ⟧ (Extension.Ext e)

  -- Isomorphisms.

  Isomorphic : Assumptions → (c : Code) → ⟦ c ⟧ → ⟦ c ⟧ → P.Type₁
  Isomorphic _   ε       _       _       = ↑ _ ⊤
  Isomorphic ass (c ▻ e) (I , x) (J , y) =
    Σ (Isomorphic ass c I J) λ I≅J → Extension.Iso e ass I≅J x y

  -- Isomorphism is equivalent to equality.

  isomorphism≃equality : (ass : Assumptions) →
                         (c : Code) {I J : ⟦ c ⟧} →
                         Isomorphic ass c I J ≃ (I ≡ J)

  isomorphism≃equality _ ε =

      ↑ _ ⊤              ↔⟨ contractible-isomorphic (↑-closure 0 ⊤-contractible)
                                                    (⇒≡ 0 $ ↑-closure 0 ⊤-contractible) ⟩□
      lift tt ≡ lift tt  □

  isomorphism≃equality ass (c ▻ e) {I , x} {J , y} =

    (Σ (Isomorphic ass c I J) λ I≅J → Iso e ass I≅J x y)  ↝⟨ Σ-cong (isomorphism≃equality ass c)
                                                                    (λ I≅J → Iso≃Iso′ e ass I≅J) ⟩
    (Σ (I ≡ J) λ I≡J → subst (Ext e) I≡J x ≡ y)           ↔⟨ Σ-≡,≡↔≡ ⟩□

    ((I , x) ≡ (J , y))                                   □

    where open Extension

-- Isomorphism is equal to equality (assuming /only/ univalence).

isomorphism≡equality :
  (univ  : Univalence (# 0))
  (univ₁ : Univalence (# 1))
  (univ₂ : Univalence (# 2)) →

  let ass = record
        { ext₁  = dependent-extensionality univ₂ univ₁
        ; univ  = univ
        ; univ₁ = univ₁
        } in

  (c : Code) {I J : ⟦ c ⟧} →
  Isomorphic ass c I J ≡ (I ≡ J)
isomorphism≡equality univ univ₁ univ₂ c =
  ≃⇒≡ univ₁ $ isomorphism≃equality _ c

------------------------------------------------------------------------
-- Reflexivity

-- The isomorphism relation is reflexive.

reflexivity : (ass : Assumptions) → ∀ c I → Isomorphic ass c I I
reflexivity ass c I =
  _≃_.from (isomorphism≃equality ass c) (refl I)

-- Reflexivity relates an element to itself.

reflexivityE :
  (ass : Assumptions) →
  ∀ c e I x →
  Extension.Iso e ass (reflexivity ass c I) x x
reflexivityE ass c e I x =
  _≃_.from (Iso≃Iso′ ass (reflexivity ass c I)) (
    subst Ext (to (from (refl I))) x  ≡⟨ subst (λ eq → subst Ext eq x ≡ x)
                                               (sym $ right-inverse-of (refl I))
                                               (refl x) ⟩∎
    x                                 ∎)
  where
  open Extension e
  open _≃_ (isomorphism≃equality ass c)

-- Unfolding lemma (definitional) for reflexivity.

reflexivity-▻ :
  ∀ {ass c e I x} →
  reflexivity ass (c ▻ e) (I , x) ≡
  (reflexivity ass c I , reflexivityE ass c e I x)
reflexivity-▻ = refl _

------------------------------------------------------------------------
-- Recipe for defining extensions

-- Another kind of extension.

record Extension-with-resp (c : Code) : P.Type₂ where
  field

    -- An instance-indexed type.

    Ext : ⟦ c ⟧ → P.Type₁

    -- A predicate specifying when two elements are isomorphic with
    -- respect to an isomorphism.

    Iso : (ass : Assumptions) →
          {I J : ⟦ c ⟧} → Isomorphic ass c I J →
          Ext I → Ext J → P.Type₁

    -- Ext, seen as a predicate, respects isomorphisms.

    resp : (ass : Assumptions) →
           ∀ {I J} → Isomorphic ass c I J →
           Ext I → Ext J

    -- The resp function respects reflexivity.

    resp-refl : (ass : Assumptions) →
                ∀ {I} (x : Ext I) →
                resp ass (reflexivity ass c I) x ≡ x

  -- An alternative definition of Iso.

  Iso″ : (ass : Assumptions) →
         {I J : ⟦ c ⟧} → Isomorphic ass c I J →
         Ext I → Ext J → P.Type₁
  Iso″ ass I≅J x y = resp ass I≅J x ≡ y

  field

    -- Iso and Iso″ are equivalent.

    Iso≃Iso″ :
      (ass : Assumptions) →
      ∀ {I J} (I≅J : Isomorphic ass c I J) {x y} →
      Iso ass I≅J x y ≃ Iso″ ass I≅J x y

  -- Another alternative definition of Iso.

  Iso′ : (ass : Assumptions) →
         ∀ {I J} → Isomorphic ass c I J →
         Ext I → Ext J → P.Type₁
  Iso′ ass I≅J x y =
    subst Ext (_≃_.to (isomorphism≃equality ass c) I≅J) x ≡ y

  abstract

    -- Every element is isomorphic to itself, transported along the
    -- "outer" isomorphism.

    isomorphic-to-itself″ :
      (ass : Assumptions) →
      ∀ {I J} (I≅J : Isomorphic ass c I J) {x} →
      Iso″ ass I≅J x
           (subst Ext (_≃_.to (isomorphism≃equality ass c) I≅J) x)
    isomorphic-to-itself″ ass I≅J {x} = transport-theorem′
      Ext
      (Isomorphic ass c)
      (_≃_.surjection $ inverse $ isomorphism≃equality ass c)
      (resp ass)
      (λ _ → resp-refl ass)
      I≅J
      x

  -- Iso and Iso′ are equivalent.

  Iso≃Iso′ :
    (ass : Assumptions) →
    ∀ {I J} (I≅J : Isomorphic ass c I J) {x y} →
    Iso ass I≅J x y ≃ Iso′ ass I≅J x y
  Iso≃Iso′ ass I≅J {x} {y} = record
    { to             = to
    ; is-equivalence =
        _⇔_.from (Is-equivalence≃Is-equivalence-CP _) λ y →
          (from y , right-inverse-of y) , irrelevance y
    }
    where
    -- This is the core of the definition. I could have defined
    -- Iso≃Iso′ ... = I≃I′. The rest is only included in order to
    -- control how much Agda unfolds the code.
    I≃I′ =
      Iso  ass I≅J x y  ↝⟨ Iso≃Iso″ ass I≅J ⟩
      Iso″ ass I≅J x y  ↝⟨ ≡⇒≃ $ cong (λ z → z ≡ y) $ isomorphic-to-itself″ ass I≅J ⟩□
      Iso′ ass I≅J x y  □

    to   = _≃_.to   I≃I′
    from = _≃_.from I≃I′

    abstract
      right-inverse-of : ∀ x → to (from x) ≡ x
      right-inverse-of = _≃_.right-inverse-of I≃I′

      irrelevance : ∀ y (p : to ⁻¹ y) → (from y , right-inverse-of y) ≡ p
      irrelevance = _≃_.irrelevance I≃I′

  -- An extension constructed from the fields above.

  extension : Extension c
  extension = record { Ext = Ext; Iso = Iso; Iso≃Iso′ = Iso≃Iso′ }

  -- Every element is isomorphic to itself, transported (in another
  -- way) along the "outer" isomorphism.

  isomorphic-to-itself :
    (ass : Assumptions) →
    ∀ {I J} (I≅J : Isomorphic ass c I J) x →
    Iso ass I≅J x (resp ass I≅J x)
  isomorphic-to-itself ass I≅J x =
    _≃_.from (Iso≃Iso″ ass I≅J) (refl (resp ass I≅J x))

  abstract

    -- Simplification lemmas.

    resp-refl-lemma :
      (ass : Assumptions) →
      ∀ I x →
      resp-refl ass x ≡
      _≃_.from (≡⇒≃ $ cong (λ z → z ≡ x) $
                      isomorphic-to-itself″ ass (reflexivity ass c I))
               (subst (λ eq → subst Ext eq x ≡ x)
                      (sym $ _≃_.right-inverse-of
                               (isomorphism≃equality ass c)
                               (refl I))
                      (refl x))
    resp-refl-lemma ass I x =
      let rfl    = reflexivity ass c I
          iso≃eq = λ {I J} → isomorphism≃equality ass c {I = I} {J = J}
          rio    = right-inverse-of iso≃eq (refl I)
          lio    = left-inverse-of (inverse iso≃eq) (refl I)
          sx≡x   = subst (λ eq → subst Ext eq x ≡ x) (sym rio) (refl x)

          sx≡x-lemma =
            cong (λ eq → subst Ext eq x) rio                      ≡⟨ sym $ trans-reflʳ _ ⟩

            trans (cong (λ eq → subst Ext eq x) rio)
                  (refl x)                                        ≡⟨ sym $ subst-trans (cong (λ eq → subst Ext eq x) rio) ⟩

            subst (λ z → z ≡ x)
                  (sym $ cong (λ eq → subst Ext eq x) rio)
                  (refl x)                                        ≡⟨ cong (λ eq → subst (λ z → z ≡ x) eq (refl x)) $ sym $
                                                                          cong-sym (λ eq → subst Ext eq x) rio ⟩
            subst (λ z → z ≡ x)
                  (cong (λ eq → subst Ext eq x) $ sym rio)
                  (refl x)                                        ≡⟨ sym $ subst-∘ (λ z → z ≡ x) (λ eq → subst Ext eq x) (sym rio) ⟩∎

            subst (λ eq → subst Ext eq x ≡ x) (sym rio) (refl x)  ∎

          lemma₁ =
            trans (sym lio) rio  ≡⟨ cong (λ eq → trans (sym eq) rio) $ left-inverse-of∘inverse iso≃eq ⟩

            trans (sym rio) rio  ≡⟨ trans-symˡ rio ⟩∎

            refl (refl I)        ∎

          lemma₂ =
            elim-refl (λ {I J} _ → Ext I → Ext J) (λ _ e → e)  ≡⟨⟩

            cong (subst Ext) (refl (refl I))                   ≡⟨ cong (cong (subst Ext)) $ sym lemma₁ ⟩∎

            cong (subst Ext) (trans (sym lio) rio)             ∎

          lemma₃ =
            cong (λ r → r x)
                 (elim-refl (λ {I J} _ → Ext I → Ext J) (λ _ e → e))   ≡⟨ cong (cong (λ r → r x)) lemma₂ ⟩

            cong (λ r → r x) (cong (subst Ext) (trans (sym lio) rio))  ≡⟨ cong-∘ (λ r → r x) (subst Ext) (trans (sym lio) rio) ⟩

            cong (λ eq → subst Ext eq x) (trans (sym lio) rio)         ≡⟨ cong-trans (λ eq → subst Ext eq x) (sym lio) rio ⟩

            trans (cong (λ eq → subst Ext eq x) (sym lio))
                  (cong (λ eq → subst Ext eq x) rio)                   ≡⟨ cong (λ eq → trans eq (cong (λ eq → subst Ext eq x) rio)) $
                                                                               cong-sym (λ eq → subst Ext eq x) lio ⟩∎
            trans (sym (cong (λ eq → subst Ext eq x) lio))
                  (cong (λ eq → subst Ext eq x) rio)                   ∎
      in

      resp-refl ass x                                                  ≡⟨ sym $ trans-reflʳ _ ⟩

      trans (resp-refl ass x) (refl x)                                 ≡⟨ cong (trans (resp-refl ass x)) $ trans-symˡ (subst-refl Ext x) ⟩

      trans (resp-refl ass x)
            (trans (sym $ subst-refl Ext x) (subst-refl Ext x))        ≡⟨ sym $ trans-assoc _ (sym $ subst-refl Ext x) (subst-refl Ext x) ⟩

      trans (trans (resp-refl ass x) (sym $ subst-refl Ext x))
            (subst-refl Ext x)                                         ≡⟨ cong (trans (trans (resp-refl ass x) (sym $ subst-refl Ext x)))
                                                                               lemma₃ ⟩
      trans (trans (resp-refl ass x) (sym $ subst-refl Ext x))
            (trans (sym (cong (λ eq → subst Ext eq x) lio))
                   (cong (λ eq → subst Ext eq x) rio))                 ≡⟨ sym $ trans-assoc _ _ (cong (λ eq → subst Ext eq x) rio) ⟩

      trans (trans (trans (resp-refl ass x) (sym $ subst-refl Ext x))
                   (sym (cong (λ eq → subst Ext eq x) lio)))
            (cong (λ eq → subst Ext eq x) rio)                         ≡⟨ cong₂ trans
                                                                            (sym $ transport-theorem′-refl Ext (Isomorphic ass c) (inverse iso≃eq)
                                                                                (resp ass) (λ _ → resp-refl ass) x)
                                                                            sx≡x-lemma ⟩
      trans (isomorphic-to-itself″ ass rfl) sx≡x                       ≡⟨ sym $ subst-trans (isomorphic-to-itself″ ass rfl) ⟩

      subst (λ z → z ≡ x) (sym $ isomorphic-to-itself″ ass rfl) sx≡x   ≡⟨ subst-in-terms-of-inverse∘≡⇒↝ equivalence
                                                                            (isomorphic-to-itself″ ass rfl) (λ z → z ≡ x) _ ⟩∎
      from (≡⇒≃ $ cong (λ z → z ≡ x) $ isomorphic-to-itself″ ass rfl)
           sx≡x                                                        ∎

      where open _≃_

    isomorphic-to-itself-reflexivity :
      (ass : Assumptions) →
      ∀ I x →
      isomorphic-to-itself ass (reflexivity ass c I) x ≡
      subst (Iso ass (reflexivity ass c I) x)
            (sym $ resp-refl ass x)
            (reflexivityE ass c extension I x)
    isomorphic-to-itself-reflexivity ass I x =
      let rfl = reflexivity ass c I
          r-r = resp-refl ass x in

      from (Iso≃Iso″ ass rfl) (refl (resp ass rfl x))                  ≡⟨ elim¹ (λ {y} resp-x≡y → from (Iso≃Iso″ ass rfl) (refl (resp ass rfl x)) ≡
                                                                                subst (Iso ass rfl x) (sym resp-x≡y)
                                                                                (from (Iso≃Iso″ ass rfl) resp-x≡y))
                                                                                (refl _) r-r ⟩
      subst (Iso ass rfl x) (sym r-r) (from (Iso≃Iso″ ass rfl) r-r)    ≡⟨ cong (subst (Iso ass rfl x) (sym r-r) ∘ from (Iso≃Iso″ ass rfl))
                                                                               (resp-refl-lemma ass I x) ⟩∎
      subst (Iso ass rfl x) (sym r-r)
        (from (Iso≃Iso″ ass rfl)
           (from
              (≡⇒≃ $ cong (λ z → z ≡ x)
                          (isomorphic-to-itself″ ass rfl))
              (subst (λ eq → subst Ext eq x ≡ x)
                 (sym $ right-inverse-of (isomorphism≃equality ass c)
                                         (refl I)) (refl x))))         ∎

      where open _≃_

------------------------------------------------------------------------
-- Type extractors

record Extractor (c : Code) : P.Type₂ where
  field

    -- Extracts a type from an instance.

    Type : ⟦ c ⟧ → P.Type₁

    -- Extracts an equivalence relating types extracted from
    -- isomorphic instances.
    --
    -- Perhaps one could have a variant of Type-cong that is not based
    -- on any "Assumptions", and produces logical equivalences (_⇔_)
    -- instead of equivalences (_≃_). Then one could (hopefully)
    -- define isomorphism without using any assumptions.

    Type-cong : (ass : Assumptions) →
                ∀ {I J} → Isomorphic ass c I J → Type I ≃ Type J

    -- Reflexivity is mapped to the identity equivalence.

    Type-cong-reflexivity :
      (ass : Assumptions) →
      ∀ I → Type-cong ass (reflexivity ass c I) ≡ Eq.id

-- Constant type extractor.

[_] : ∀ {c} → P.Type₁ → Extractor c
[_] {c} A = record
  { Type                  = λ _ → A
  ; Type-cong             = λ _ _ → Eq.id
  ; Type-cong-reflexivity = λ _ _ → refl _
  }

-- Successor type extractor.

infix 6 1+_

1+_ : ∀ {c e} → Extractor c → Extractor (c ▻ e)
1+_ {c} {e} extractor = record
  { Type                  = Type ∘ proj₁
  ; Type-cong             = λ ass → Type-cong ass ∘ proj₁
  ; Type-cong-reflexivity = λ { ass (I , x) →
      Type-cong ass (reflexivity ass c I)  ≡⟨ Type-cong-reflexivity ass I ⟩∎
      Eq.id                                ∎ }
  }
  where
  open Extractor extractor

------------------------------------------------------------------------
-- An extension: types

-- Extends a structure with a type.

A-type : ∀ {c} → Extension c
A-type {c} = record
  { Ext      = λ _ → P.Type
  ; Iso      = λ _ _ A B → ↑ _ (A ≃ B)
  ; Iso≃Iso′ = λ ass I≅J {A B} →
                 let I≡J = _≃_.to (isomorphism≃equality ass c) I≅J in

                 ↑ _ (A ≃ B)                       ↔⟨ ↑↔ ⟩
                 (A ≃ B)                           ↝⟨ inverse $ ≡≃≃ (Assumptions.univ ass) ⟩
                 (A ≡ B)                           ↝⟨ ≡⇒≃ $ cong (λ C → C ≡ B) $ sym (subst-const I≡J) ⟩
                 (subst (λ _ → P.Type) I≡J A ≡ B)  □
  }

-- A corresponding type extractor.

[0] : ∀ {c} → Extractor (c ▻ A-type)
[0] {c} = record
  { Type                  = λ { (_ , A) → ↑ _ A }
  ; Type-cong             = λ { _ (_ , lift A≃B) → ↑-cong A≃B }
  ; Type-cong-reflexivity = λ { ass (I , A) → elim₁
      (λ {p} q →
         ↑-cong (≡⇒≃
           (from (≡⇒≃ (cong (λ C → C ≡ A) (sym (subst-const p))))
                 (subst (λ eq → subst Ext eq A ≡ A)
                        (sym q) (refl A)))) ≡
         Eq.id)
      (lift-equality (Assumptions.ext₁ ass) (refl _))
      (right-inverse-of (isomorphism≃equality ass c) (refl I)) }
  }
  where
  open Extension A-type
  open _≃_

------------------------------------------------------------------------
-- An extension: propositions

-- Extends a structure with a proposition.

Proposition : ∀ {c} →

              -- The proposition.
              (P : ⟦ c ⟧ → P.Type₁) →

              -- The proposition must be propositional (given some
              -- assumptions).
              (Assumptions → ∀ I → Is-proposition (P I)) →

              Extension c
Proposition {c} P prop = record
  { Ext      = P
  ; Iso      = λ _ _ _ _ → ↑ _ ⊤
  ; Iso≃Iso′ = λ ass I≅J {_ p} →
                 ↑ _ ⊤    ↔⟨ contractible-isomorphic
                               (↑-closure 0 ⊤-contractible)
                               (⇒≡ 0 $ propositional⇒inhabited⇒contractible (prop ass _) p) ⟩□
                 (_ ≡ _)  □
  }

-- The proposition stating that a given type is a set.

Is-a-set : ∀ {c} → Extractor c → Extension c
Is-a-set extractor =
  Proposition (Is-set ∘ Type)
              (λ ass _ → H-level-propositional (Assumptions.ext₁ ass) 2)
  where open Extractor extractor

------------------------------------------------------------------------
-- An extension: n-ary functions

-- N-ary functions.

_^_⟶_ : P.Type₁ → ℕ → P.Type₁ → P.Type₁
A ^ zero  ⟶ B = B
A ^ suc n ⟶ B = A → A ^ n ⟶ B

-- N-ary function morphisms.

Is-_-ary-morphism :
  ∀ (n : ℕ) {A B} → (A ^ n ⟶ A) → (B ^ n ⟶ B) → (A → B) → P.Type₁
Is- zero  -ary-morphism x y m = m x ≡ y
Is- suc n -ary-morphism f g m =
  ∀ x → Is- n -ary-morphism (f x) (g (m x)) m

-- An n-ary function extension.

N-ary : ∀ {c} →

        -- Extracts the underlying type.
        Extractor c →

        -- The function's arity.
        ℕ →

        Extension c
N-ary {c} extractor n = Extension-with-resp.extension record
  { Ext       = λ I → Type I ^ n ⟶ Type I
  ; Iso       = λ ass I≅J f g →
                    Is- n -ary-morphism f g (_≃_.to (Type-cong ass I≅J))
  ; resp      = λ ass I≅J → cast n (Type-cong ass I≅J)
  ; resp-refl = λ ass f →
                    cast n (Type-cong ass (reflexivity ass c _)) f  ≡⟨ cong (λ eq → cast n eq f) $ Type-cong-reflexivity ass _ ⟩
                    cast n Eq.id f                                  ≡⟨ cast-id (Assumptions.ext₁ ass) n f ⟩∎
                    f                                               ∎
  ; Iso≃Iso″  = λ ass I≅J {f g} →
      Iso≃Iso″ (Assumptions.ext₁ ass) (Type-cong ass I≅J) n f g
  }
  where
  open Extractor extractor

  -- Changes the type of an n-ary function.

  cast : ∀ n {A B} → A ≃ B → A ^ n ⟶ A → B ^ n ⟶ B
  cast zero    A≃B = _≃_.to A≃B
  cast (suc n) A≃B = λ f x → cast n A≃B (f (_≃_.from A≃B x))

  -- Cast simplification lemma.

  cast-id : Extensionality (# 1) (# 1) →
            ∀ {A} n (f : A ^ n ⟶ A) → cast n Eq.id f ≡ f
  cast-id ext zero    x = refl x
  cast-id ext (suc n) f = apply-ext ext λ x → cast-id ext n (f x)

  -- Two definitions of isomorphism are equivalent.

  Iso≃Iso″ :
    Extensionality (# 1) (# 1) →
    ∀ {A B} (A≃B : A ≃ B)
    (n : ℕ) (f : A ^ n ⟶ A) (g : B ^ n ⟶ B) →
    Is- n -ary-morphism f g (_≃_.to A≃B) ≃ (cast n A≃B f ≡ g)

  Iso≃Iso″ ext A≃B zero x y =

    (_≃_.to A≃B x ≡ y)  □

  Iso≃Iso″ ext A≃B (suc n) f g =

    (∀ x → Is- n -ary-morphism (f x) (g (_≃_.to A≃B x)) (_≃_.to A≃B))  ↝⟨ ∀-cong ext (λ x →
                                                                            Iso≃Iso″ ext A≃B n (f x) (g (_≃_.to A≃B x))) ⟩
    (∀ x → cast n A≃B (f x) ≡ g (_≃_.to A≃B x))                        ↝⟨ Eq.extensionality-isomorphism ext ⟩

    (cast n A≃B ∘ f ≡ g ∘ _≃_.to A≃B)                                  ↔⟨ inverse $ ∘from≡↔≡∘to ext A≃B ⟩□

    (cast n A≃B ∘ f ∘ _≃_.from A≃B ≡ g)                                □

------------------------------------------------------------------------
-- An extension: simply typed functions

-- This section contains a generalisation of the development for n-ary
-- functions above.

-- Simple types.

data Simple-type (c : Code) : P.Type₂ where
  base : Extractor c → Simple-type c
  _⟶_  : Simple-type c → Simple-type c → Simple-type c

-- Interpretation of a simple type.

⟦_⟧⟶ : ∀ {c} → Simple-type c → ⟦ c ⟧ → P.Type₁
⟦ base A ⟧⟶ I = Extractor.Type A I
⟦ σ ⟶ τ  ⟧⟶ I = ⟦ σ ⟧⟶ I → ⟦ τ ⟧⟶ I

-- A simply typed function extension.

Simple : ∀ {c} → Simple-type c → Extension c
Simple {c} σ = Extension-with-resp.extension record
  { Ext       = ⟦ σ ⟧⟶
  ; Iso       = λ ass → Iso ass σ
  ; resp      = λ ass I≅J → _≃_.to (cast ass σ I≅J)
  ; resp-refl = λ ass f → cong (λ eq → _≃_.to eq f) $ cast-refl ass σ
  ; Iso≃Iso″  = λ ass → Iso≃Iso″ ass σ
  }
  where
  open Extractor

  -- Isomorphisms between simply typed values.

  Iso : (ass : Assumptions) →
        (σ : Simple-type c) →
        ∀ {I J} → Isomorphic ass c I J → ⟦ σ ⟧⟶ I → ⟦ σ ⟧⟶ J → P.Type₁
  Iso ass (base A) I≅J x y = _≃_.to (Type-cong A ass I≅J) x ≡ y
  Iso ass (σ ⟶ τ)  I≅J f g =
    ∀ x y → Iso ass σ I≅J x y → Iso ass τ I≅J (f x) (g y)

  -- Cast.

  cast : (ass : Assumptions) →
         (σ : Simple-type c) →
         ∀ {I J} → Isomorphic ass c I J → ⟦ σ ⟧⟶ I ≃ ⟦ σ ⟧⟶ J
  cast ass (base A) I≅J = Type-cong A ass I≅J
  cast ass (σ ⟶ τ)  I≅J = →-cong ext₁ (cast ass σ I≅J) (cast ass τ I≅J)
    where open Assumptions ass

  -- Cast simplification lemma.

  cast-refl : (ass : Assumptions) →
              ∀ σ {I} → cast ass σ (reflexivity ass c I) ≡ Eq.id
  cast-refl ass (base A) {I} =
    Type-cong A ass (reflexivity ass c I)  ≡⟨ Type-cong-reflexivity A ass I ⟩∎
    Eq.id                                  ∎

  cast-refl ass (σ ⟶ τ) {I} =
    cast ass (σ ⟶ τ) (reflexivity ass c I)  ≡⟨ lift-equality ext₁ $ cong _≃_.to $
                                                 cong₂ (→-cong ext₁) (cast-refl ass σ) (cast-refl ass τ) ⟩∎
    Eq.id                                   ∎
    where open Assumptions ass

  -- Two definitions of isomorphism are equivalent.

  Iso≃Iso″ :
    (ass : Assumptions) →
    (σ : Simple-type c) →
    ∀ {I J} (I≅J : Isomorphic ass c I J) {f g} →
    Iso ass σ I≅J f g ≃ (_≃_.to (cast ass σ I≅J) f ≡ g)
  Iso≃Iso″ ass (base A) I≅J {x} {y} =

    (_≃_.to (Type-cong A ass I≅J) x ≡ y)  □

  Iso≃Iso″ ass (σ ⟶ τ) I≅J {f} {g} =

    (∀ x y → Iso ass σ I≅J x y → Iso ass τ I≅J (f x) (g y))        ↝⟨ ∀-cong ext₁ (λ _ → ∀-cong ext₁ λ _ →
                                                                        →-cong ext₁ (Iso≃Iso″ ass σ I≅J) (Iso≃Iso″ ass τ I≅J)) ⟩
    (∀ x y → to (cast ass σ I≅J) x ≡ y →
             to (cast ass τ I≅J) (f x) ≡ g y)                      ↝⟨ inverse $ ∀-cong ext₁ (λ x →
                                                                        ∀-intro (λ y _ → to (cast ass τ I≅J) (f x) ≡ g y) ext₁) ⟩
    (∀ x → to (cast ass τ I≅J) (f x) ≡ g (to (cast ass σ I≅J) x))  ↝⟨ extensionality-isomorphism ext₁ ⟩

    (to (cast ass τ I≅J) ∘ f ≡ g ∘ to (cast ass σ I≅J))            ↔⟨ inverse $ ∘from≡↔≡∘to ext₁ (cast ass σ I≅J) ⟩□

    (to (cast ass τ I≅J) ∘ f ∘ from (cast ass σ I≅J) ≡ g)          □

    where
    open _≃_
    open Assumptions ass

------------------------------------------------------------------------
-- An unfinished extension: dependent types

-- The extension currently supports polymorphic types.

module Dependent where

  open Extractor

  ----------------------------------------------------------------------
  -- The extension

  -- Dependent types.

  data Ty (c : Code) : P.Type₂

  -- Extension: Dependently-typed functions.

  ext-with-resp : ∀ {c} → Ty c → Extension-with-resp c

  private
    open module E {c} (σ : Ty c) =
      Extension-with-resp (ext-with-resp σ)
      hiding (Iso; Iso≃Iso″; extension)
  open E public using () renaming (extension to Dep)

  data Ty c where
    set  : Ty c
    base : Extractor c → Ty c
    Π    : (σ : Ty c) → Ty (c ▻ Dep σ) → Ty c

  -- Interpretation of a dependent type.

  ⟦_⟧Π : ∀ {c} → Ty c → ⟦ c ⟧ → P.Type₁

  -- Isomorphisms between dependently typed functions.

  Iso :
    (ass : Assumptions) →
    ∀ {c} (σ : Ty c) →
    ∀ {I J} → Isomorphic ass c I J → ⟦ σ ⟧Π I → ⟦ σ ⟧Π J → P.Type₁

  -- A cast function.

  cast : (ass : Assumptions) →
         ∀ {c} (σ : Ty c) {I J} →
         Isomorphic ass c I J → ⟦ σ ⟧Π I ≃ ⟦ σ ⟧Π J

  -- Reflexivity is mapped to identity.

  cast-refl : (ass : Assumptions) →
              ∀ {c} (σ : Ty c) {I} →
              cast ass σ (reflexivity ass c I) ≡ Eq.id

  -- Two definitions of isomorphism are equivalent.

  Iso≃Iso″ : (ass : Assumptions) →
             ∀ {c} (σ : Ty c) {I J} (I≅J : Isomorphic ass c I J) {f g} →
             Iso ass σ I≅J f g ≃ (_≃_.to (cast ass σ I≅J) f ≡ g)

  -- Extension: Dependently-typed functions.

  ext-with-resp {c} σ = record
    { Ext       = ⟦ σ ⟧Π
    ; Iso       = λ ass → Iso ass σ
    ; resp      = λ ass I≅J → _≃_.to (cast ass σ I≅J)
    ; resp-refl = λ ass f → cong (λ eq → _≃_.to eq f) $ cast-refl ass σ
    ; Iso≃Iso″  = λ ass → Iso≃Iso″ ass σ
    }

  -- Interpretation of a dependent type.

  ⟦ set    ⟧Π _ = P.Type
  ⟦ base A ⟧Π I = Type A I
  ⟦ Π σ τ  ⟧Π I = (x : ⟦ σ ⟧Π I) → ⟦ τ ⟧Π (I , x)

  -- Isomorphisms between dependently typed functions.

  Iso _   set      _   A B = ↑ _ (A ≃ B)
  Iso ass (base A) I≅J x y = x ≡ _≃_.from (Type-cong A ass I≅J) y
  Iso ass (Π σ τ)  I≅J f g = ∀ x y →
    (x≅y : Iso ass σ I≅J x y) → Iso ass τ (I≅J , x≅y) (f x) (g y)

  -- A cast function.

  cast ass set      I≅J = Eq.id
  cast ass (base A) I≅J = Type-cong A ass I≅J
  cast ass (Π σ τ)  I≅J = Π-cong ext₁
    (cast ass σ I≅J)
    (λ x → cast ass τ (I≅J , isomorphic-to-itself σ ass I≅J x))
    where open Assumptions ass

  abstract

    -- Reflexivity is mapped to identity.

    cast-refl ass     set          = refl Eq.id
    cast-refl ass {c} (base A) {I} =

      Type-cong A ass (reflexivity ass c I)  ≡⟨ Type-cong-reflexivity A ass I ⟩∎

      Eq.id                                  ∎

    cast-refl ass {c} (Π σ τ) {I} =
      let rfl   = reflexivity ass c I
          rflE  = reflexivityE ass c (Dep σ) I in

      lift-equality-inverse ext₁ $
      apply-ext ext₁ λ f →
      apply-ext ext₁ λ x →

        from (cast ass τ (rfl , isomorphic-to-itself σ ass rfl x))
             (f (resp σ ass rfl x))                                 ≡⟨ cong (λ iso → from (cast ass τ (rfl , iso)) (f (resp σ ass rfl x))) $
                                                                            isomorphic-to-itself-reflexivity σ ass I x ⟩
        from (cast ass τ (rfl , subst (Iso ass σ rfl x)
                                      (sym $ resp-refl σ ass x)
                                      (rflE x)))
             (f (resp σ ass rfl x))                                 ≡⟨ elim¹ (λ {y} x≡y →
                                                                                from (cast ass τ (rfl , subst (Iso ass σ rfl x)
                                                                                x≡y (rflE x)))
                                                                                (f y) ≡
                                                                                f x)
                                                                             (cong (λ h → _≃_.from h (f x)) $ cast-refl ass τ)
                                                                             (sym $ resp-refl σ ass x) ⟩∎
        f x                                                         ∎

      where
      open _≃_
      open Assumptions ass

  -- Two definitions of isomorphism are equivalent.

  Iso≃Iso‴ :
    (ass : Assumptions) →
    ∀ {c} (σ : Ty c) {I J} (I≅J : Isomorphic ass c I J) {f g} →
    Iso ass σ I≅J f g ≃ (f ≡ _≃_.from (cast ass σ I≅J) g)

  Iso≃Iso‴ ass set I≅J {A} {B} =

    ↑ _ (A ≃ B)  ↔⟨ ↑↔ ⟩

    (A ≃ B)      ↝⟨ inverse $ ≡≃≃ (Assumptions.univ ass) ⟩□

    (A ≡ B)      □

  Iso≃Iso‴ ass (base A) I≅J {x} {y} =

    (x ≡ _≃_.from (Type-cong A ass I≅J) y)  □

  Iso≃Iso‴ ass (Π σ τ) I≅J {f} {g} =
    let iso-to-itself = isomorphic-to-itself σ ass I≅J in

    (∀ x y (x≅y : Iso ass σ I≅J x y) →
           Iso ass τ (I≅J , x≅y) (f x) (g y))                        ↝⟨ ∀-cong ext₁ (λ x → ∀-cong ext₁ λ y →
                                                                          Π-cong ext₁ (Iso≃Iso″ ass σ I≅J) (λ x≅y →
           Iso ass τ (I≅J , x≅y) (f x) (g y)                                ↝⟨ Iso≃Iso″ ass τ (I≅J , x≅y) ⟩
           (resp τ ass (I≅J , x≅y) (f x) ≡ g y)                             ↝⟨ ≡⇒≃ $ cong (λ x≅y → resp τ ass (I≅J , x≅y) (f x) ≡ g y) $
                                                                                sym $ left-inverse-of (Iso≃Iso″ ass σ I≅J) _ ⟩□
           (resp τ ass (I≅J , from (Iso≃Iso″ ass σ I≅J)
                                   (to (Iso≃Iso″ ass σ I≅J) x≅y))
               (f x) ≡ g y)                                                 □)) ⟩

    (∀ x y (x≡y : to (cast ass σ I≅J) x ≡ y) →
           resp τ ass (I≅J , from (Iso≃Iso″ ass σ I≅J) x≡y) (f x) ≡
           g y)                                                      ↝⟨ ∀-cong ext₁ (λ x → inverse $
                                                                          ∀-intro (λ y x≡y → _ ≡ _) ext₁) ⟩
    (∀ x → resp τ ass (I≅J , iso-to-itself x) (f x) ≡
           g (resp σ ass I≅J x))                                     ↔⟨ extensionality-isomorphism ext₁ ⟩

    (resp τ ass (I≅J , iso-to-itself _) ∘ f ≡ g ∘ resp σ ass I≅J)    ↔⟨ to∘≡↔≡from∘ ext₁ (cast ass τ (I≅J , iso-to-itself _)) ⟩

    (f ≡ from (cast ass τ (I≅J , iso-to-itself _)) ∘
         g ∘ resp σ ass I≅J)                                         □

    where
    open _≃_
    open Assumptions ass

  abstract

    -- Two definitions of isomorphism are equivalent.

    Iso≃Iso″ ass σ I≅J {f} {g} =
      Iso ass σ I≅J f g                  ↝⟨ Iso≃Iso‴ ass σ I≅J ⟩

      (f ≡ _≃_.from (cast ass σ I≅J) g)  ↔⟨ inverse $ from≡↔≡to (inverse $ cast ass σ I≅J) ⟩□

      (_≃_.to (cast ass σ I≅J) f ≡ g)    □

  ----------------------------------------------------------------------
  -- An instantiation of the type extractor mechanism that gives us
  -- support for polymorphic types

  abstract

    reflexivityE-set :
      (ass : Assumptions) →
      ∀ {c} {I : ⟦ c ⟧} {A} →
      reflexivityE ass c (Dep set) I A ≡ lift Eq.id
    reflexivityE-set ass {c} {I} {A} =
      let ≡⇒→′ = _↔_.to ∘ ≡⇒↝ _ in

      reflexivityE ass c (Dep set) I A                                ≡⟨⟩

      lift (≡⇒≃ (to (from≡↔≡to (inverse Eq.id))
              (from (≡⇒≃ $ cong (λ B → B ≡ A) $
                       isomorphic-to-itself″ set ass
                         (reflexivity ass c I))
                    (subst (λ eq → subst (λ _ → P.Type) eq A ≡ A)
                           (sym $ right-inverse-of
                                    (isomorphism≃equality ass c)
                                    (refl I))
                           (refl A)))))                               ≡⟨ cong (λ eq → lift (≡⇒≃ (to (from≡↔≡to (inverse Eq.id)) eq))) $ sym $
                                                                           resp-refl-lemma set ass I A ⟩
      lift (≡⇒≃ (to (from≡↔≡to (inverse Eq.id))
                    (resp-refl set ass {I = I} A)))                   ≡⟨⟩

      lift (≡⇒≃ (to (from≡↔≡to (inverse Eq.id)) (refl A)))            ≡⟨⟩

      lift (≡⇒≃ (≡⇒→′ (cong (λ B → B ≡ A)
                            (right-inverse-of (inverse Eq.id) A))
                      (cong id (refl A))))                            ≡⟨⟩

      lift (≡⇒≃ (≡⇒→′ (cong (λ B → B ≡ A) (left-inverse-of Eq.id A))
                      (cong id (refl A))))                            ≡⟨ cong (λ eq → lift (≡⇒≃ (≡⇒→′ (cong (λ B → B ≡ A) eq) (refl A))))
                                                                         left-inverse-of-id  ⟩
      lift (≡⇒≃ (≡⇒→′ (cong (λ B → B ≡ A) (refl A)) (refl A)))        ≡⟨⟩

      lift (≡⇒≃ (≡⇒→′ (refl (A ≡ A)) (refl A)))                       ≡⟨⟩

      lift (≡⇒≃ (refl A))                                             ≡⟨ refl _ ⟩∎

      lift Eq.id                                                      ∎

      where
      open _↔_ using  (to)
      open _≃_ hiding (to)

  ⟨0⟩ : ∀ {c} → Extractor (c ▻ Dep set)
  ⟨0⟩ {c} = record
    { Type                  = λ { (_ , A) → ↑ _ A }
    ; Type-cong             = λ { _ (_ , lift A≃B) → ↑-cong A≃B }
    ; Type-cong-reflexivity = λ { ass (I , A) →
        let open Assumptions ass; open _≃_ in

        lift-equality ext₁ (apply-ext ext₁ λ { (lift x) → cong lift (

          to (lower (reflexivityE ass c (Dep set) I A)) x  ≡⟨ cong (λ eq → to (lower eq) x) $ reflexivityE-set ass ⟩∎

          x                                                ∎ )})}
    }

------------------------------------------------------------------------
-- Examples

-- For examples, see
-- Univalence-axiom.Isomorphism-is-equality.More.Examples.

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

open import HoTT
open import homotopy.CoHSpace
open import homotopy.Cogroup

module groups.FromSusp where

module _ {i} (X : Ptd i) where
  private
    A = de⊙ X
    e = pt X

  module Pinch = SuspRec (winl north) (winr south)
    (λ a → ap winl (σloop X a) ∙ wglue ∙ ap winr (merid a))

  pinch : Susp A → ⊙Susp X ∨ ⊙Susp X
  pinch = Pinch.f

  ⊙pinch : ⊙Susp X ⊙→ ⊙Susp X ⊙∨ ⊙Susp X
  ⊙pinch = pinch , idp

  private
    abstract
      unit-r : ∀ x → projl (pinch x) == x
      unit-r = Susp-elim idp (merid e) λ x → ↓-∘=idf-in' projl pinch $
        ap projl (ap pinch (merid x)) ∙' merid e
          =⟨ ∙'=∙ (ap projl (ap pinch (merid x))) (merid e) ⟩
        ap projl (ap pinch (merid x)) ∙ merid e
          =⟨ ap (_∙ merid e) $
            ap projl (ap pinch (merid x))
              =⟨ ap (ap projl) $ Pinch.merid-β x ⟩
            ap projl (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x))
              =⟨ ap-∙∙ projl (ap winl (σloop X x)) wglue (ap winr (merid x)) ⟩
            ap projl (ap winl (σloop X x)) ∙ ap projl wglue ∙ ap projl (ap winr (merid x))
              =⟨ ap3 (λ p q r → p ∙ q ∙ r)
                  (∘-ap projl winl (σloop X x) ∙ ap-idf (σloop X x))
                  Projl.glue-β
                  (∘-ap projl winr (merid x) ∙ ap-cst north (merid x)) ⟩
            σloop X x ∙ idp
              =⟨ ∙-unit-r (σloop X x) ⟩
            σloop X x
              =∎ ⟩
        σloop X x ∙ merid e
          =⟨ ∙-assoc (merid x) (! (merid e)) (merid e) ⟩
        merid x ∙ ! (merid e) ∙ merid e
          =⟨ ap (merid x ∙_) (!-inv-l (merid e)) ∙ ∙-unit-r (merid x) ⟩
        merid x
          =∎

      ⊙unit-r : ⊙projl ⊙∘ ⊙pinch ⊙∼ ⊙idf (⊙Susp X)
      ⊙unit-r = unit-r , idp

      unit-l : ∀ x → projr (pinch x) == x
      unit-l = Susp-elim idp idp λ x → ↓-∘=idf-in' projr pinch $
        ap projr (ap pinch (merid x))
          =⟨ ap (ap projr) $ Pinch.merid-β x ⟩
        ap projr (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x))
          =⟨ ap-∙∙ projr (ap winl (σloop X x)) wglue (ap winr (merid x)) ⟩
        ap projr (ap winl (σloop X x)) ∙ ap projr wglue ∙ ap projr (ap winr (merid x))
          =⟨ ap3 (λ p q r → p ∙ q ∙ r)
              (∘-ap projr winl (σloop X x) ∙ ap-cst north (σloop X x))
              Projr.glue-β
              (∘-ap projr winr (merid x) ∙ ap-idf (merid x)) ⟩
        merid x
          =∎

      ⊙unit-l : ⊙projr ⊙∘ ⊙pinch ⊙∼ ⊙idf (⊙Susp X)
      ⊙unit-l = unit-l , idp

  Susp-co-h-space-structure : CoHSpaceStructure (⊙Susp X)
  Susp-co-h-space-structure = record {
    ⊙coμ = ⊙pinch;
    ⊙unit-l = ⊙unit-l;
    ⊙unit-r = ⊙unit-r}

  private
    ⊙inv = ⊙Susp-flip X

    abstract
      inv-l : ∀ σ → ⊙WedgeRec.f (⊙Susp-flip X) (⊙idf (⊙Susp X)) (pinch σ) == north
      inv-l = Susp-elim (! (merid (pt X))) (! (merid (pt X))) λ x →
        ↓-app=cst-in $ ! $ ap (_∙ ! (merid (pt X))) $
          ap (W.f ∘ pinch) (merid x)
            =⟨ ap-∘ W.f pinch (merid x) ⟩
          ap W.f (ap pinch (merid x))
            =⟨ ap (ap W.f) (Pinch.merid-β x) ⟩
          ap W.f (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x))
            =⟨ ap-∙∙ W.f (ap winl (σloop X x)) wglue (ap winr (merid x)) ⟩
          ap W.f (ap winl (σloop X x)) ∙ ap W.f wglue ∙ ap W.f (ap winr (merid x))
            =⟨ ap3 (λ p q r → p ∙ q ∙ r)
                ( ∘-ap W.f winl (σloop X x)
                ∙ ap-∙ Susp-flip (merid x) (! (merid (pt X)))
                ∙ (SuspFlip.merid-β x ∙2 (ap-! Susp-flip (merid (pt X)) ∙ ap ! (SuspFlip.merid-β (pt X)))))
                (W.glue-β ∙ ∙-unit-r (! (merid (pt X))))
                (∘-ap W.f winr (merid x) ∙ ap-idf (merid x)) ⟩
          (! (merid x) ∙ ! (! (merid (pt X)))) ∙ (! (merid (pt X)) ∙ merid x)
            =⟨ ap (_∙ (! (merid (pt X)) ∙ merid x)) (∙-! (merid x) (! (merid (pt X)))) ⟩
          ! (! (merid (pt X)) ∙ merid x) ∙ (! (merid (pt X)) ∙ merid x)
            =⟨ !-inv-l (! (merid (pt X)) ∙ merid x) ⟩
          idp
            =∎
        where module W = ⊙WedgeRec (⊙Susp-flip X) (⊙idf (⊙Susp X))

      ⊙inv-l : ⊙Wedge-rec (⊙Susp-flip X) (⊙idf (⊙Susp X)) ⊙∘ ⊙pinch ⊙∼ ⊙cst
      ⊙inv-l = inv-l , ↓-idf=cst-in' idp

      assoc : ∀ σ
        → fst (⊙–> (⊙∨-assoc (⊙Susp X) (⊙Susp X) (⊙Susp X)))
            (∨-fmap ⊙pinch (⊙idf (⊙Susp X)) (pinch σ))
        == ∨-fmap (⊙idf (⊙Susp X)) ⊙pinch (pinch σ)
      assoc = Susp-elim idp idp λ x → ↓-='-in' $ ! $
        ap (Assoc.f ∘ FmapL.f ∘ pinch) (merid x)
          =⟨ ap-∘ (Assoc.f ∘ FmapL.f) pinch (merid x) ⟩
        ap (Assoc.f ∘ FmapL.f) (ap pinch (merid x))
          =⟨ ap (ap (Assoc.f ∘ FmapL.f)) (Pinch.merid-β x) ⟩
        ap (Assoc.f ∘ FmapL.f) (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x))
          =⟨ ap-∘ Assoc.f FmapL.f (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x)) ⟩
        ap Assoc.f (ap FmapL.f (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x)))
          =⟨ ap (ap Assoc.f) $
                ap FmapL.f (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x))
                  =⟨ ap-∙∙ FmapL.f (ap winl (σloop X x)) wglue (ap winr (merid x)) ⟩
                ap FmapL.f (ap winl (σloop X x)) ∙ ap FmapL.f wglue ∙ ap FmapL.f (ap winr (merid x))
                  =⟨ ap3 (λ p q r → p ∙ q ∙ r)
                      ( ∘-ap FmapL.f winl (σloop X x)
                      ∙ ap-∘ winl pinch (σloop X x)
                      ∙ ap (ap winl) (lemma₀ x)
                      ∙ ap-∙∙∙ winl (ap winl (σloop X x)) wglue (ap winr (σloop X x)) (! wglue)
                      ∙ ap3 (λ p q r → p ∙ ap winl wglue ∙ q ∙ r)
                          (∘-ap winl winl (σloop X x))
                          (∘-ap winl winr (σloop X x))
                          (ap-! winl wglue))
                      FmapL.glue-β
                      (∘-ap FmapL.f winr (merid x)) ⟩
                ( ap (winl ∘ winl) (σloop X x) ∙ ap winl wglue ∙ ap (winl ∘ winr) (σloop X x) ∙ ! (ap winl wglue))
                ∙ wglue ∙ ap winr (merid x)
                  =∎ ⟩
        ap Assoc.f
          ((ap (winl ∘ winl) (σloop X x) ∙ ap winl wglue ∙ ap (winl ∘ winr) (σloop X x) ∙ ! (ap winl wglue))
           ∙ wglue ∙ ap winr (merid x))
          =⟨ ap-∙∙ Assoc.f
              (ap (winl ∘ winl) (σloop X x) ∙ ap winl wglue ∙ ap (winl ∘ winr) (σloop X x) ∙ ! (ap winl wglue))
              wglue (ap winr (merid x))
           ∙ ap (λ p → p ∙ ap Assoc.f wglue ∙ ap Assoc.f (ap winr (merid x)))
              (ap-∙∙∙ Assoc.f
                (ap (winl ∘ winl) (σloop X x))
                (ap winl wglue)
                (ap (winl ∘ winr) (σloop X x))
                (! (ap winl wglue))) ⟩
        ( ap Assoc.f (ap (winl ∘ winl) (σloop X x))
        ∙ ap Assoc.f (ap winl wglue)
        ∙ ap Assoc.f (ap (winl ∘ winr) (σloop X x))
        ∙ ap Assoc.f (! (ap winl wglue)))
          ∙ ap Assoc.f wglue ∙ ap Assoc.f (ap winr (merid x))
          =⟨ ap6 (λ p₀ p₁ p₂ p₃ p₄ p₅ → (p₀ ∙ p₁ ∙ p₂ ∙ p₃) ∙ p₄ ∙ p₅)
              (∘-ap Assoc.f (winl ∘ winl) (σloop X x))
              (∘-ap Assoc.f winl wglue ∙ AssocInl.glue-β)
              (∘-ap Assoc.f (winl ∘ winr) (σloop X x) ∙ ap-∘ winr winl (σloop X x))
              (ap-! Assoc.f (ap winl wglue) ∙ ap ! (∘-ap Assoc.f winl wglue ∙ AssocInl.glue-β))
              Assoc.glue-β
              (∘-ap Assoc.f winr (merid x) ∙ ap-∘ winr winr (merid x)) ⟩
        (ap winl (σloop X x) ∙ wglue ∙ ap winr (ap winl (σloop X x)) ∙ ! wglue)
        ∙ (wglue ∙ ap winr wglue) ∙ ap winr (ap winr (merid x))
          =⟨ lemma₁ (ap winl (σloop X x)) wglue (ap winr (ap winl (σloop X x))) (ap winr wglue) (ap winr (ap winr (merid x))) ⟩
        ap winl (σloop X x) ∙ wglue ∙ ap winr (ap winl (σloop X x)) ∙ ap winr wglue ∙ ap winr (ap winr (merid x))
          =⟨ ap3 (λ p q r → p ∙ q ∙ r)
              (ap-∘ FmapR.f winl (σloop X x))
              (! FmapR.glue-β)
              ( ∙∙-ap winr (ap winl (σloop X x)) wglue (ap winr (merid x))
              ∙ ap (ap winr) (! (Pinch.merid-β x))
              ∙ ∘-ap winr pinch (merid x)
              ∙ ap-∘ FmapR.f winr (merid x)) ⟩
        ap FmapR.f (ap winl (σloop X x)) ∙ ap FmapR.f wglue ∙ ap FmapR.f (ap winr (merid x))
          =⟨ ∙∙-ap FmapR.f (ap winl (σloop X x)) wglue (ap winr (merid x)) ⟩
        ap FmapR.f (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x))
          =⟨ ! $ ap (ap FmapR.f) (Pinch.merid-β x) ⟩
        ap FmapR.f (ap pinch (merid x))
          =⟨ ∘-ap FmapR.f pinch (merid x) ⟩
        ap (FmapR.f ∘ pinch) (merid x)
          =∎
        where
          module Assoc = WedgeAssoc (⊙Susp X) (⊙Susp X) (⊙Susp X)
          module AssocInl = WedgeAssocInl (⊙Susp X) (⊙Susp X) (⊙Susp X)
          module FmapL = WedgeFmap ⊙pinch (⊙idf (⊙Susp X))
          module FmapR = WedgeFmap (⊙idf (⊙Susp X)) ⊙pinch

          lemma₀ : ∀ x → ap pinch (σloop X x)
            == ap winl (σloop X x) ∙ wglue ∙ ap winr (σloop X x) ∙ ! wglue
          lemma₀ x =
            ap pinch (σloop X x)
              =⟨ ap-∙ pinch (merid x) (! (merid (pt X))) ⟩
            ap pinch (merid x) ∙ ap pinch (! (merid (pt X)))
              =⟨ Pinch.merid-β x ∙2 (ap-! pinch (merid (pt X)) ∙ ap ! (Pinch.merid-β (pt X))) ⟩
            (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x)) ∙ ! (ap winl (σloop X (pt X)) ∙ wglue ∙ ap winr (merid (pt X)))
              =⟨ ap (λ p → (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x))
                           ∙ ! (ap winl p ∙ wglue ∙ ap winr (merid (pt X))))
                    σloop-pt ⟩
            (ap winl (σloop X x) ∙ wglue ∙ ap winr (merid x)) ∙ ! (wglue ∙ ap winr (merid (pt X)))
              =⟨ lemma₀₁ winr (ap winl (σloop X x)) wglue (merid x) (merid (pt X)) ⟩
            ap winl (σloop X x) ∙ wglue ∙ ap winr (σloop X x) ∙ ! wglue
              =∎
            where
              lemma₀₁ : ∀ {i j} {A : Type i} {B : Type j} {b₀ b₁ : B} {a₂ a₃ : A}
                → (f : A → B)
                → (p₀ : b₀ == b₁) (p₁ : b₁ == f a₂) (p₂ : a₂ == a₃) (p₃ : a₂ == a₃)
                → (p₀ ∙ p₁ ∙ ap f p₂) ∙ ! (p₁ ∙ ap f p₃)
                == p₀ ∙ p₁ ∙ ap f (p₂ ∙ ! p₃) ∙ ! p₁
              lemma₀₁ f idp idp idp p₃ = !-ap f p₃ ∙ ! (∙-unit-r (ap f (! p₃)))

          lemma₁ : ∀ {i} {A : Type i} {a₀ a₁ a₂ a₃ a₄ : A}
            → (p₀ : a₀ == a₁) (p₁ : a₁ == a₂) (p₂ : a₂ == a₂) (p₃ : a₂ == a₃) (p₄ : a₃ == a₄)
            → (p₀ ∙ p₁ ∙ p₂ ∙ ! p₁) ∙ (p₁ ∙ p₃) ∙ p₄
            == p₀ ∙ p₁ ∙ (p₂ ∙ p₃ ∙ p₄)
          lemma₁ idp idp p₂ idp idp = ∙-unit-r (p₂ ∙ idp)

      ⊙assoc :
           ⊙–> (⊙∨-assoc (⊙Susp X) (⊙Susp X) (⊙Susp X)) ⊙∘
           ⊙∨-fmap ⊙pinch (⊙idf (⊙Susp X)) ⊙∘ ⊙pinch
        ⊙∼ ⊙∨-fmap (⊙idf (⊙Susp X)) ⊙pinch ⊙∘ ⊙pinch
      ⊙assoc = assoc , idp

  Susp-cogroup-structure : CogroupStructure (⊙Susp X)
  Susp-cogroup-structure = record {
    co-h-struct = Susp-co-h-space-structure;
    ⊙inv = ⊙Susp-flip X;
    ⊙inv-l = ⊙inv-l;
    ⊙assoc = ⊙assoc}

  Susp⊙→-group-structure : ∀ {j} (Y : Ptd j) → GroupStructure (⊙Susp X ⊙→ Y)
  Susp⊙→-group-structure Y = cogroup⊙→-group-structure Susp-cogroup-structure Y

  Trunc-Susp⊙→-group : ∀ {j} (Y : Ptd j) → Group (lmax i j)
  Trunc-Susp⊙→-group Y = Trunc-group (Susp⊙→-group-structure Y)

{-
module _ {i j} (X : Ptd i) where

  Lift-Susp-co-h-space-structure : CoHSpaceStructure (⊙Lift {j = j} (⊙Susp X))
  Lift-Susp-co-h-space-structure =
    Lift-co-h-space-structure {j = j} (Susp-co-h-space-structure X)

  Lift-Susp-cogroup-structure : CogroupStructure (⊙Lift {j = j} (⊙Susp X))
  Lift-Susp-cogroup-structure =
    Lift-cogroup-structure {j = j} (Susp-cogroup-structure X)

  LiftSusp⊙→-group-structure : ∀ {k} (Y : Ptd k) → GroupStructure (⊙Lift {j = j} (⊙Susp X) ⊙→ Y)
  LiftSusp⊙→-group-structure Y = cogroup⊙→-group-structure Lift-Susp-cogroup-structure Y

  Trunc-LiftSusp⊙→-group : ∀ {k} (Y : Ptd k) → Group (lmax (lmax i j) k)
  Trunc-LiftSusp⊙→-group Y = Trunc-group (LiftSusp⊙→-group-structure Y)
-}

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module Issue1105 where

module So.Bad where

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import FRP.JS.Nat using ( ℕ ; suc ; _+_ ; _≟_ )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing ; _≟[_]_ )
open import FRP.JS.Bool using ( Bool ; not )
open import FRP.JS.QUnit using ( TestSuite ; ok ; ok! ; test ; _,_ )

module FRP.JS.Test.Maybe where

_≟¹_ : Maybe ℕ → Maybe ℕ → Bool
xs ≟¹ ys = xs ≟[ _≟_ ] ys

Maybe² : Set → Set
Maybe² A = Maybe (Maybe A)

_≟²_ : Maybe² ℕ → Maybe² ℕ → Bool
xs ≟² ys = xs ≟[ _≟¹_ ] ys

just² : ∀ {A : Set} → A → Maybe² A
just² a = just (just a)

Maybe³ : Set → Set
Maybe³ A = Maybe (Maybe² A)

_≟³_ : Maybe³ ℕ → Maybe³ ℕ → Bool
xs ≟³ ys = xs ≟[ _≟²_ ] ys

just³ : ∀ {A} → A → Maybe³ A
just³ a = just (just² a)

tests : TestSuite
tests =
  ( test "≟"
    ( ok "nothing ≟ nothing" (nothing ≟¹ nothing)
    , ok "just 0 ≟ just 0"   (just 0 ≟¹ just 0)
    , ok "nothing ≟ just 1"  (not (nothing ≟¹ just 1))
    , ok "just 0 ≟ nothing"  (not (just 0 ≟¹ nothing))
    , ok "just 0 ≟ just 1"   (not (just 0 ≟¹ just 1)) )
  , test "≟²"
    ( ok "nothing ≟² nothing"           (nothing ≟² nothing)
    , ok "just nothing ≟² just nothing" (just nothing ≟² just nothing)
    , ok "just² 0 ≟² just² 0"           (just² 0 ≟² just² 0)
    , ok "nothing ≟² just nothing"      (not (nothing ≟² just nothing))
    , ok "nothing ≟² just² 1"           (not (nothing ≟² just² 1))
    , ok "just nothing ≟² just² 1"      (not (just nothing ≟² just² 1))
    , ok "just² 0 ≟² just² 1"           (not (just² 0 ≟² just² 1)) )
  , test "≟³"
    ( ok "nothing ≟³ nothing"             (nothing ≟³ nothing)
    , ok "just nothing ≟³ just nothing"   (just nothing ≟³ just nothing)
    , ok "just² nothing ≟³ just² nothing" (just² nothing ≟³ just² nothing)
    , ok "just³ 0 ≟³ just³ 0"             (just³ 0 ≟³ just³ 0)
    , ok "nothing ≟³ just nothing"        (not (nothing ≟³ just nothing))
    , ok "nothing ≟³ just² nothing"       (not (nothing ≟³ just² nothing))
    , ok "nothing ≟³ just³ 1"             (not (nothing ≟³ just³ 1))
    , ok "just nothing ≟³ just² nothing"  (not (just nothing ≟³ just² nothing))
    , ok "just nothing ≟³ just³ 1"        (not (just nothing ≟³ just³ 1))
    , ok "just³ 0 ≟³ just³ 1"             (not (just³ 0 ≟³ just³ 1)) ) )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module Homogenous.Nat where

import PolyDepPrelude
open PolyDepPrelude using (zero; one; _::_; nil; right; left; pair; unit)

import Homogenous.Base

open Homogenous.Base using (Sig; T; Intro)

-- The code for natural numbers is [0 1]

codeNat : Sig
codeNat = zero :: (one :: nil)

iNat : Set
iNat = T codeNat

-- Short-hand notation for the normal Nat constructors

izero : iNat
izero = Intro (left unit)

isucc : iNat -> iNat
isucc = \(h : iNat) -> Intro (right (left (pair h unit)))
-- the pair with the dummy unit component comes from the 1-tuple
--   representation as A*()

ione : iNat
ione = isucc izero

{-
main : Set
main = {!!}
-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Cubical.Algebra.Base public
open import Cubical.Algebra.Definitions public

open import Cubical.Algebra.Structures public using (IsMagma; ismagma)
open import Cubical.Algebra.Bundles public using (Magma; mkmagma; MagmaCarrier)
open import Cubical.Structures.Carrier public

open import Cubical.Algebra.Magma.Properties public
open import Cubical.Algebra.Magma.Morphism public
open import Cubical.Algebra.Magma.MorphismProperties public


text:
module CaseSplit1 where

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

f0 : ℕ → ℕ
f0 = λ { x → {!   !} ; y → {!   !} }

f1 : ℕ → ℕ
f1 = λ
  { x → {!   !}
  ; y → {!   !}
  }

g0 : ℕ → ℕ
g0 = λ where x → {!   !}
             y → {!   !}

g1 : ℕ → ℕ
g1 = λ where
  x → {!   !}
  y → {!   !}

issue16 : ℕ → ℕ
issue16 = λ {x → {!   !} }

max_stars_repo_name: EdNutting/agda-mode-vscode


text:
------------------------------------------------------------------------------
-- ABP auxiliary lemma
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.ABP.StrongerInductionPrinciple.LemmaI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Base.List
open import FOTC.Base.Loop
open import FOTC.Base.List.PropertiesI
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesI
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Program.ABP.ABP
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Fair.PropertiesI
open import FOTC.Program.ABP.PropertiesI
open import FOTC.Program.ABP.Terms

------------------------------------------------------------------------------
-- Helper function for the auxiliary lemma

module Helper where

  helper : ∀ {b i' is' os₁ os₂ as bs cs ds js} →
           Bit b →
           Fair os₂ →
           S b (i' ∷ is') os₁ os₂ as bs cs ds js →
           ∀ ft₁ os₁' → F*T ft₁ → Fair os₁' → os₁ ≡ ft₁ ++ os₁' →
           ∃[ js' ] js ≡ i' ∷ js'
  helper {b} {i'} {is'} {os₁} {os₂} {as} {bs} {cs} {ds} {js} Bb Fos₂
         (asS , bsS , csS , dsS , jsS)
         .(T ∷ []) os₁' f*tnil Fos₁' os₁-eq = js' , js-eq
    where
    os₁-eq-helper : os₁ ≡ T ∷ os₁'
    os₁-eq-helper = os₁              ≡⟨ os₁-eq ⟩
                    (T ∷ []) ++ os₁' ≡⟨ ++-∷ T [] os₁' ⟩
                    T ∷ ([] ++ os₁') ≡⟨ ∷-rightCong (++-leftIdentity os₁') ⟩
                    T ∷ os₁'         ∎

    as' : D
    as' = await b i' is' ds

    as-eq : as ≡ < i' , b > ∷ as'
    as-eq = trans asS (send-eq b i' is' ds)

    bs' : D
    bs' = corrupt os₁' · as'

    bs-eq : bs ≡ ok < i' , b > ∷ bs'
    bs-eq =
     bs ≡⟨ bsS ⟩
      corrupt os₁ · as
        ≡⟨ ·-rightCong as-eq ⟩
      corrupt os₁ · (< i' , b > ∷ as')
        ≡⟨ ·-leftCong (corruptCong os₁-eq-helper) ⟩
      corrupt (T ∷ os₁') · (< i' , b > ∷ as')
        ≡⟨ corrupt-T os₁' < i' , b > as' ⟩
      ok < i' , b > ∷ corrupt os₁' · as'
        ≡⟨ refl ⟩
      ok < i' , b > ∷ bs' ∎

    cs' : D
    cs' = ack (not b) · bs'

    js' : D
    js' = out (not b) · bs'

    js-eq : js ≡ i' ∷ js'
    js-eq = js                            ≡⟨ jsS ⟩
            out b · bs                    ≡⟨ ·-rightCong bs-eq ⟩
            out b · (ok < i' , b > ∷ bs') ≡⟨ out-ok≡ b b i' bs' refl ⟩
            i' ∷ out (not b) · bs'        ≡⟨ refl ⟩
            i' ∷ js'                      ∎

    ds' : D
    ds' = ds

  helper {b} {i'} {is'} {os₁} {os₂} {as} {bs} {cs} {ds} {js}
         Bb Fos₂ (asS , bsS , csS , dsS , jsS)
         .(F ∷ ft₁^) os₁' (f*tcons {ft₁^} FTft₁^) Fos₁' os₁-eq =
         helper Bb (tail-Fair Fos₂) ihS ft₁^ os₁' FTft₁^ Fos₁' refl

    where
    os₁^ : D
    os₁^ = ft₁^ ++ os₁'

    os₂^ : D
    os₂^ = tail₁ os₂

    os₁-eq-helper : os₁ ≡ F ∷ os₁^
    os₁-eq-helper = os₁                ≡⟨ os₁-eq ⟩
                    (F ∷ ft₁^) ++ os₁' ≡⟨ ++-∷ F ft₁^ os₁' ⟩
                    F ∷ ft₁^ ++ os₁'   ≡⟨ refl ⟩
                    F ∷ os₁^           ∎

    as^ : D
    as^ = await b i' is' ds

    as-eq : as ≡ < i' , b > ∷ as^
    as-eq = trans asS (send-eq b i' is' ds)

    bs^ : D
    bs^ = corrupt os₁^ · as^

    bs-eq : bs ≡ error ∷ bs^
    bs-eq =
      bs
        ≡⟨ bsS ⟩
      corrupt os₁ · as
        ≡⟨ ·-rightCong as-eq ⟩
      corrupt os₁ · (< i' , b > ∷ as^)
        ≡⟨ ·-leftCong (corruptCong os₁-eq-helper) ⟩
      corrupt (F ∷ os₁^) · (< i' , b > ∷ as^)
        ≡⟨ corrupt-F os₁^ < i' , b > as^ ⟩
      error ∷ corrupt os₁^ · as^
        ≡⟨ refl ⟩
      error ∷ bs^ ∎

    cs^ : D
    cs^ = ack b · bs^

    cs-eq : cs ≡ not b ∷ cs^
    cs-eq = cs                    ≡⟨ csS ⟩
            ack b · bs            ≡⟨ ·-rightCong bs-eq ⟩
            ack b · (error ∷ bs^) ≡⟨ ack-error b bs^ ⟩
            not b ∷ ack b · bs^   ≡⟨ refl ⟩
            not b ∷ cs^           ∎

    ds^ : D
    ds^ = corrupt os₂^ · cs^

    ds-eq-helper₁ : os₂ ≡ T ∷ tail₁ os₂ → ds ≡ ok (not b) ∷ ds^
    ds-eq-helper₁ h =
      ds                                 ≡⟨ dsS ⟩
      corrupt os₂ · cs                   ≡⟨ ·-rightCong cs-eq ⟩
      corrupt os₂ · (not b ∷ cs^)        ≡⟨ ·-leftCong (corruptCong h) ⟩
      corrupt (T ∷ os₂^) · (not b ∷ cs^) ≡⟨ corrupt-T os₂^ (not b) cs^ ⟩
      ok (not b) ∷ corrupt os₂^ · cs^    ≡⟨ refl ⟩
      ok (not b) ∷ ds^                   ∎

    ds-eq-helper₂ : os₂ ≡ F ∷ tail₁ os₂ → ds ≡ error ∷ ds^
    ds-eq-helper₂ h =
      ds                                 ≡⟨ dsS ⟩
      corrupt os₂ · cs                   ≡⟨ ·-rightCong cs-eq ⟩
      corrupt os₂ · (not b ∷ cs^)        ≡⟨ ·-leftCong (corruptCong h) ⟩
      corrupt (F ∷ os₂^) · (not b ∷ cs^) ≡⟨ corrupt-F os₂^ (not b) cs^ ⟩
      error ∷ corrupt os₂^ · cs^         ≡⟨ refl ⟩
      error ∷ ds^                        ∎

    ds-eq : ds ≡ ok (not b) ∷ ds^ ∨ ds ≡ error ∷ ds^
    ds-eq = case (λ h → inj₁ (ds-eq-helper₁ h))
                 (λ h → inj₂ (ds-eq-helper₂ h))
                 (head-tail-Fair Fos₂)

    as^-eq-helper₁ : ds ≡ ok (not b) ∷ ds^ → as^ ≡ send b · (i' ∷ is') · ds^
    as^-eq-helper₁ h =
      await b i' is' ds
        ≡⟨ awaitCong₄ h ⟩
      await b i' is' (ok (not b) ∷ ds^)
        ≡⟨ await-ok≢ b (not b) i' is' ds^ (x≢not-x Bb) ⟩
      < i' , b > ∷ await b i' is' ds^
        ≡⟨ sym (send-eq b i' is' ds^) ⟩
      send b · (i' ∷ is') · ds^ ∎

    as^-eq-helper₂ : ds ≡ error ∷ ds^ → as^ ≡ send b · (i' ∷ is') · ds^
    as^-eq-helper₂ h =
      await b i' is' ds               ≡⟨ awaitCong₄ h ⟩
      await b i' is' (error ∷ ds^)    ≡⟨ await-error b i' is' ds^ ⟩
      < i' , b > ∷ await b i' is' ds^ ≡⟨ sym (send-eq b i' is' ds^) ⟩
      send b · (i' ∷ is') · ds^     ∎

    as^-eq : as^ ≡ send b · (i' ∷ is') · ds^
    as^-eq = case as^-eq-helper₁ as^-eq-helper₂ ds-eq

    js-eq : js ≡ out b · bs^
    js-eq = js                    ≡⟨ jsS ⟩
            out b · bs            ≡⟨ ·-rightCong bs-eq ⟩
            out b · (error ∷ bs^) ≡⟨ out-error b bs^ ⟩
            out b · bs^ ∎

    ihS : S b (i' ∷ is') os₁^ os₂^ as^ bs^ cs^ ds^ js
    ihS = as^-eq , refl , refl , refl , js-eq

------------------------------------------------------------------------------
-- From Dybjer and Sander's paper: From the assumption that os₁ ∈ Fair
-- and hence by unfolding Fair, we conclude that there are ft₁ :  F*T
-- and os₁' : Fair, such that os₁ = ft₁ ++ os₁'.
--
-- We proceed by induction on ft₁ : F*T using helper.

open Helper
lemma : ∀ {b i' is' os₁ os₂ as bs cs ds js} →
         Bit b →
         Fair os₁ →
         Fair os₂ →
         S b (i' ∷ is') os₁ os₂ as bs cs ds js →
         ∃[ js' ] js ≡ i' ∷ js'
lemma Bb Fos₁ Fos₂ s with Fair-out Fos₁
... | ft , os₁' , FTft , prf ,  Fos₁' = helper Bb Fos₂ s ft os₁' FTft Fos₁' prf

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc